Step
*
1
of Lemma
contraction-to-extend_wf
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ Compositon(A)
4. ctr : {Gamma ⊢ _:Contractible(A)}
5. H : CubicalSet{j}
6. sigma : H j⟶ Gamma
7. phi : {H ⊢ _:𝔽}
8. u : {H, phi ⊢ _:(A)sigma}
9. contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma}
10. ∀[c:{H, phi ⊢ _:Contractible((A)sigma)}]. ∀[x:{H, phi ⊢ _:(A)sigma}].
      (contr-path(c;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center(c) x)})
11. ∀[x:{H, phi ⊢ _:(A)sigma}]. (contr-path((ctr)sigma;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center((ctr)sigma) x)})
12. ∀[pth:{H, phi ⊢ _:Path((A)sigma)}]. (path-eta(pth) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
13. ∀x:{H, phi ⊢ _:(A)sigma}
      ((path-eta(contr-path((ctr)sigma;x)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
      ∧ ((path-eta(contr-path((ctr)sigma;x)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma})
      ∧ ((path-eta(contr-path((ctr)sigma;x)))[1(𝕀)] = x ∈ {H, phi ⊢ _:(A)sigma}))
14. path-eta(contr-path((ctr)sigma;u)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p}
15. (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma}
16. (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)] = u ∈ {H, phi ⊢ _:(A)sigma}
17. ((cA)sigma)p ∈ H.𝕀 ⊢ Compositon(((A)sigma)p)
18. ∀[a0:{H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
      ((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] a0)s
      = comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (a0)s
      ∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
19. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
      ((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma))s
      = comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (contr-center((ctr)sigma))s
      ∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
⊢ comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma[phi |⟶ u]}
BY
{ ((InstLemma `comp_term_wf` [⌜H⌝;⌜phi⌝;⌜((A)sigma)p⌝;⌜((cA)sigma)p⌝;⌜path-eta(contr-path((ctr)sigma;u))⌝]⋅ THENA Auto)
   THEN Reduce -1
   THEN (Subst' ((A)sigma)1(H) ~ (A)sigma -1 THENA (CsmUnfolding THEN Auto))
   THEN InstHyp [⌜contr-center((ctr)sigma)⌝] (-1)⋅) }
1
.....wf..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ Compositon(A)
4. ctr : {Gamma ⊢ _:Contractible(A)}
5. H : CubicalSet{j}
6. sigma : H j⟶ Gamma
7. phi : {H ⊢ _:𝔽}
8. u : {H, phi ⊢ _:(A)sigma}
9. contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma}
10. ∀[c:{H, phi ⊢ _:Contractible((A)sigma)}]. ∀[x:{H, phi ⊢ _:(A)sigma}].
      (contr-path(c;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center(c) x)})
11. ∀[x:{H, phi ⊢ _:(A)sigma}]. (contr-path((ctr)sigma;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center((ctr)sigma) x)})
12. ∀[pth:{H, phi ⊢ _:Path((A)sigma)}]. (path-eta(pth) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
13. ∀x:{H, phi ⊢ _:(A)sigma}
      ((path-eta(contr-path((ctr)sigma;x)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
      ∧ ((path-eta(contr-path((ctr)sigma;x)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma})
      ∧ ((path-eta(contr-path((ctr)sigma;x)))[1(𝕀)] = x ∈ {H, phi ⊢ _:(A)sigma}))
14. path-eta(contr-path((ctr)sigma;u)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p}
15. (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma}
16. (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)] = u ∈ {H, phi ⊢ _:(A)sigma}
17. ((cA)sigma)p ∈ H.𝕀 ⊢ Compositon(((A)sigma)p)
18. ∀[a0:{H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
      ((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] a0)s
      = comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (a0)s
      ∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
19. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
      ((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma))s
      = comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (contr-center((ctr)sigma))s
      ∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
20. ∀[a0:{H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)]]}]
      (comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] a0
       ∈ {H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)]]})
⊢ contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)]]}
2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ Compositon(A)
4. ctr : {Gamma ⊢ _:Contractible(A)}
5. H : CubicalSet{j}
6. sigma : H j⟶ Gamma
7. phi : {H ⊢ _:𝔽}
8. u : {H, phi ⊢ _:(A)sigma}
9. contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma}
10. ∀[c:{H, phi ⊢ _:Contractible((A)sigma)}]. ∀[x:{H, phi ⊢ _:(A)sigma}].
      (contr-path(c;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center(c) x)})
11. ∀[x:{H, phi ⊢ _:(A)sigma}]. (contr-path((ctr)sigma;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center((ctr)sigma) x)})
12. ∀[pth:{H, phi ⊢ _:Path((A)sigma)}]. (path-eta(pth) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
13. ∀x:{H, phi ⊢ _:(A)sigma}
      ((path-eta(contr-path((ctr)sigma;x)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
      ∧ ((path-eta(contr-path((ctr)sigma;x)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma})
      ∧ ((path-eta(contr-path((ctr)sigma;x)))[1(𝕀)] = x ∈ {H, phi ⊢ _:(A)sigma}))
14. path-eta(contr-path((ctr)sigma;u)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p}
15. (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma}
16. (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)] = u ∈ {H, phi ⊢ _:(A)sigma}
17. ((cA)sigma)p ∈ H.𝕀 ⊢ Compositon(((A)sigma)p)
18. ∀[a0:{H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)]]}]. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
      ((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] a0)s
      = comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (a0)s
      ∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
19. ∀[Delta:j⊢]. ∀[s:Delta j⟶ H].
      ((comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma))s
      = comp (((cA)sigma)p)s+ [(phi)s ⊢→ (path-eta(contr-path((ctr)sigma;u)))s+] (contr-center((ctr)sigma))s
      ∈ {Delta ⊢ _:((((A)sigma)p)s+)[1(𝕀)][(phi)s |⟶ ((path-eta(contr-path((ctr)sigma;u)))s+)[1(𝕀)]]})
20. ∀[a0:{H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)]]}]
      (comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] a0
       ∈ {H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)]]})
21. comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma)
    ∈ {H ⊢ _:(A)sigma[phi |⟶ (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)]]}
⊢ comp ((cA)sigma)p [phi ⊢→ path-eta(contr-path((ctr)sigma;u))] contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma[phi |⟶ u]}
Latex:
Latex:
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  Gamma  \mvdash{}  Compositon(A)
4.  ctr  :  \{Gamma  \mvdash{}  \_:Contractible(A)\}
5.  H  :  CubicalSet\{j\}
6.  sigma  :  H  j{}\mrightarrow{}  Gamma
7.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
8.  u  :  \{H,  phi  \mvdash{}  \_:(A)sigma\}
9.  contr-center((ctr)sigma)  \mmember{}  \{H  \mvdash{}  \_:(A)sigma\}
10.  \mforall{}[c:\{H,  phi  \mvdash{}  \_:Contractible((A)sigma)\}].  \mforall{}[x:\{H,  phi  \mvdash{}  \_:(A)sigma\}].
            (contr-path(c;x)  \mmember{}  \{H,  phi  \mvdash{}  \_:(Path\_(A)sigma  contr-center(c)  x)\})
11.  \mforall{}[x:\{H,  phi  \mvdash{}  \_:(A)sigma\}]
            (contr-path((ctr)sigma;x)  \mmember{}  \{H,  phi  \mvdash{}  \_:(Path\_(A)sigma  contr-center((ctr)sigma)  x)\})
12.  \mforall{}[pth:\{H,  phi  \mvdash{}  \_:Path((A)sigma)\}].  (path-eta(pth)  \mmember{}  \{H,  phi.\mBbbI{}  \mvdash{}  \_:((A)sigma)p\})
13.  \mforall{}x:\{H,  phi  \mvdash{}  \_:(A)sigma\}
            ((path-eta(contr-path((ctr)sigma;x))  \mmember{}  \{H,  phi.\mBbbI{}  \mvdash{}  \_:((A)sigma)p\})
            \mwedge{}  ((path-eta(contr-path((ctr)sigma;x)))[0(\mBbbI{})]  =  contr-center((ctr)sigma))
            \mwedge{}  ((path-eta(contr-path((ctr)sigma;x)))[1(\mBbbI{})]  =  x))
14.  path-eta(contr-path((ctr)sigma;u))  \mmember{}  \{H,  phi.\mBbbI{}  \mvdash{}  \_:((A)sigma)p\}
15.  (path-eta(contr-path((ctr)sigma;u)))[0(\mBbbI{})]  =  contr-center((ctr)sigma)
16.  (path-eta(contr-path((ctr)sigma;u)))[1(\mBbbI{})]  =  u
17.  ((cA)sigma)p  \mmember{}  H.\mBbbI{}  \mvdash{}  Compositon(((A)sigma)p)
18.  \mforall{}[a0:\{H  \mvdash{}  \_:(A)sigma[phi  |{}\mrightarrow{}  (path-eta(contr-path((ctr)sigma;u)))[0(\mBbbI{})]]\}].  \mforall{}[Delta:j\mvdash{}].
        \mforall{}[s:Delta  j{}\mrightarrow{}  H].
            ((comp  ((cA)sigma)p  [phi  \mvdash{}\mrightarrow{}  path-eta(contr-path((ctr)sigma;u))]  a0)s
            =  comp  (((cA)sigma)p)s+  [(phi)s  \mvdash{}\mrightarrow{}  (path-eta(contr-path((ctr)sigma;u)))s+]  (a0)s)
19.  \mforall{}[Delta:j\mvdash{}].  \mforall{}[s:Delta  j{}\mrightarrow{}  H].
            ((comp  ((cA)sigma)p  [phi  \mvdash{}\mrightarrow{}  path-eta(contr-path((ctr)sigma;u))]  contr-center((ctr)sigma))s
            =  comp  (((cA)sigma)p)s+  [(phi)s  \mvdash{}\mrightarrow{}  (path-eta(contr-path((ctr)sigma;u)))s+]
                        (contr-center((ctr)sigma))s)
\mvdash{}  comp  ((cA)sigma)p  [phi  \mvdash{}\mrightarrow{}  path-eta(contr-path((ctr)sigma;u))]  contr-center((ctr)sigma)
    \mmember{}  \{H  \mvdash{}  \_:(A)sigma[phi  |{}\mrightarrow{}  u]\}
By
Latex:
((InstLemma  `comp\_term\_wf`  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}((A)sigma)p\mkleeneclose{};\mkleeneopen{}((cA)sigma)p\mkleeneclose{};
    \mkleeneopen{}path-eta(contr-path((ctr)sigma;u))\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  Reduce  -1
  THEN  (Subst'  ((A)sigma)1(H)  \msim{}  (A)sigma  -1  THENA  (CsmUnfolding  THEN  Auto))
  THEN  InstHyp  [\mkleeneopen{}contr-center((ctr)sigma)\mkleeneclose{}]  (-1)\mcdot{})
Home
Index