---

Step * of Lemma contraction-to-extend_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ Compositon(A)]. ∀[ctr:{Gamma ⊢ _:Contractible(A)}].
  (contraction-to-extend(Gamma;A;cA;ctr) ∈ Gamma ⊢ Extension(A))
BY
{ (Auto
   THEN (Assert contraction-to-extend(Gamma;A;cA;ctr) ∈ extension-fun{j:l}(Gamma; A) BY
               (RepUR ``contraction-to-extend extension-fun`` 0 THEN Auto))
   THEN Try (((MemTypeCD THEN Auto) THEN (D 0 THENA Auto) THEN Intros))
   THEN (InstLemma `contr-center_wf` [⌜H⌝;⌜(A)sigma⌝;⌜(ctr)sigma⌝]⋅ THENA Auto)
   THEN (InstLemma `contr-path_wf` [⌜H, phi⌝;⌜(A)sigma⌝]⋅ THENA Auto)
   THEN (RWO "contractible-type-subset" (-1) THENA Auto)
   THEN (InstHyp [⌜(ctr)sigma⌝] (-1)⋅ THENA Auto)
   THEN (InstLemma `path-eta_wf` [⌜H, phi⌝;⌜(A)sigma⌝]⋅ THENA Auto)
   THEN (Assert ∀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})) BY
               (ParallelOp -2
                THEN (GenConclTerm ⌜contr-path((ctr)sigma;x)⌝⋅ THENA Auto)
                THEN (D 0
                      THENL [Auto
                            ; ((RWO "path-eta-1 path-eta-0" 0 THENA Auto) THEN Fold `cubical-path-app` 0 THEN Auto)]
                )))
   THEN (InstHyp [⌜u⌝] (-1)⋅ THENA Auto)
   THEN ExRepD
   THEN ((Assert ((cA)sigma)p ∈ H.𝕀 ⊢ Compositon(((A)sigma)p) BY
                ((GenConclTerm ⌜(cA)sigma⌝⋅ THENA Auto)
                 THEN Thin (-1)
                 THEN MoveToConcl (-1)
                 THEN (GenConclTerm ⌜(A)sigma⌝⋅ THENA Auto)
                 THEN All Thin
                 THEN Auto))
         THEN (InstLemma `csm-comp_term` [⌜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)⋅
         THENA ((Subst' [0(𝕀)] ~ [0(𝕀)] 0 THENA (CsmUnfolding THEN Auto)) THEN MemTypeCD THEN Auto)
         )) }

1
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]}

2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ Compositon(A)
4. ctr : {Gamma ⊢ _:Contractible(A)}
5. contraction-to-extend(Gamma;A;cA;ctr) ∈ extension-fun{j:l}(Gamma; A)
6. H : CubicalSet{j}
7. K : CubicalSet{j}
8. tau : K j⟶ H
9. sigma : H j⟶ Gamma
10. phi : {H ⊢ _:𝔽}
11. u : {H, phi ⊢ _:(A)sigma}
12. contr-center((ctr)sigma) ∈ {H ⊢ _:(A)sigma}
13. ∀[c:{H, phi ⊢ _:Contractible((A)sigma)}]. ∀[x:{H, phi ⊢ _:(A)sigma}].
      (contr-path(c;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center(c) x)})
14. ∀[x:{H, phi ⊢ _:(A)sigma}]. (contr-path((ctr)sigma;x) ∈ {H, phi ⊢ _:(Path_(A)sigma contr-center((ctr)sigma) x)})
15. ∀[pth:{H, phi ⊢ _:Path((A)sigma)}]. (path-eta(pth) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p})
16. ∀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}))
17. path-eta(contr-path((ctr)sigma;u)) ∈ {H, phi.𝕀 ⊢ _:((A)sigma)p}
18. (path-eta(contr-path((ctr)sigma;u)))[0(𝕀)] = contr-center((ctr)sigma) ∈ {H, phi ⊢ _:(A)sigma}
19. (path-eta(contr-path((ctr)sigma;u)))[1(𝕀)] = u ∈ {H, phi ⊢ _:(A)sigma}
20. ((cA)sigma)p ∈ H.𝕀 ⊢ Compositon(((A)sigma)p)
21. ∀[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(𝕀)]]})
22. ∀[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(𝕀)]]})
⊢ (contraction-to-extend(Gamma;A;cA;ctr) H sigma phi u)tau
= (contraction-to-extend(Gamma;A;cA;ctr) K sigma o tau (phi)tau (u)tau)
∈ {K ⊢ _:((A)sigma)tau[(phi)tau |⟶ (u)tau]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  Compositon(A)].  \mforall{}[ctr:\{Gamma  \mvdash{}  \_:Contractible(A)\}].
    (contraction-to-extend(Gamma;A;cA;ctr)  \mmember{}  Gamma  \mvdash{}  Extension(A))


By

---

Latex:
(Auto
  THEN  (Assert  contraction-to-extend(Gamma;A;cA;ctr)  \mmember{}  extension-fun\{j:l\}(Gamma;  A)  BY
                          (RepUR  ``contraction-to-extend  extension-fun``  0  THEN  Auto))
  THEN  Try  (((MemTypeCD  THEN  Auto)  THEN  (D  0  THENA  Auto)  THEN  Intros))
  THEN  (InstLemma  `contr-center\_wf`  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}(A)sigma\mkleeneclose{};\mkleeneopen{}(ctr)sigma\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `contr-path\_wf`  [\mkleeneopen{}H,  phi\mkleeneclose{};\mkleeneopen{}(A)sigma\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "contractible-type-subset"  (-1)  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}(ctr)sigma\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `path-eta\_wf`  [\mkleeneopen{}H,  phi\mkleeneclose{};\mkleeneopen{}(A)sigma\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \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))  BY
                          (ParallelOp  -2
                            THEN  (GenConclTerm  \mkleeneopen{}contr-path((ctr)sigma;x)\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  (D  0
                                        THENL  [Auto
                                                    ;  ((RWO  "path-eta-1  path-eta-0"  0  THENA  Auto)
                                                          THEN  Fold  `cubical-path-app`  0
                                                          THEN  Auto)]
                            )))
  THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  ((Assert  ((cA)sigma)p  \mmember{}  H.\mBbbI{}  \mvdash{}  Compositon(((A)sigma)p)  BY
                            ((GenConclTerm  \mkleeneopen{}(cA)sigma\mkleeneclose{}\mcdot{}  THENA  Auto)
                              THEN  Thin  (-1)
                              THEN  MoveToConcl  (-1)
                              THEN  (GenConclTerm  \mkleeneopen{}(A)sigma\mkleeneclose{}\mcdot{}  THENA  Auto)
                              THEN  All  Thin
                              THEN  Auto))
              THEN  (InstLemma  `csm-comp\_term`  [\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{}
              THENA  ((Subst'  [0(\mBbbI{})]  \msim{}  [0(\mBbbI{})]  0  THENA  (CsmUnfolding  THEN  Auto))  THEN  MemTypeCD  THEN  Auto)
              ))

---

Home Index