---

Step * 2 of Lemma csm-contractible-type


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. Z : CubicalSet{j}
4. s : Z j⟶ X
5. (((A)s)p)p = (A)s o p o p ∈ {Z.(A)s.((A)s)p ⊢ _}
⊢ (Contractible(A))s = Z ⊢ Contractible((A)s) ∈ {Z ⊢ _}
BY
{ (Enough to prove Z.(A)s ⊢ Π((A)s)p (Path_(((A)s)p)p (q)p q)
   = Z.(A)s ⊢ Π((A)p)(s o p;q) ((Path_((A)p)p (q)p q))((s o p;q) o p;q)
   ∈ {Z.(A)s ⊢ _}
    Because (Unfold `contractible-type` 0
             THEN (RWO "csm-cubical-sigma" 0 THENA Auto)
             THEN EqCD
             THEN Auto
             THEN (InstLemmaIJ `csm-cubical-pi` [⌜X.A⌝;⌜Z.(A)s⌝;⌜(A)p⌝;⌜(Path_((A)p)p (q)p q)⌝;⌜(s o p;q)⌝]⋅ THENA Auto)
             THEN NthHypEqGen (-1)
             THEN EqCD
             THEN Try (Complete (Auto)))) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. Z : CubicalSet{j}
4. s : Z j⟶ X
5. (((A)s)p)p = (A)s o p o p ∈ {Z.(A)s.((A)s)p ⊢ _}
⊢ Z.(A)s ⊢ Π((A)s)p (Path_(((A)s)p)p (q)p q)
= Z.(A)s ⊢ Π((A)p)(s o p;q) ((Path_((A)p)p (q)p q))((s o p;q) o p;q)
∈ {Z.(A)s ⊢ _}

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  Z  :  CubicalSet\{j\}
4.  s  :  Z  j{}\mrightarrow{}  X
5.  (((A)s)p)p  =  (A)s  o  p  o  p
\mvdash{}  (Contractible(A))s  =  Z  \mvdash{}  Contractible((A)s)


By

---

Latex:
(Enough  to  prove  Z.(A)s  \mvdash{}  \mPi{}((A)s)p  (Path\_(((A)s)p)p  (q)p  q)
  =  Z.(A)s  \mvdash{}  \mPi{}((A)p)(s  o  p;q)  ((Path\_((A)p)p  (q)p  q))((s  o  p;q)  o  p;q)
    Because  (Unfold  `contractible-type`  0
                      THEN  (RWO  "csm-cubical-sigma"  0  THENA  Auto)
                      THEN  EqCD
                      THEN  Auto
                      THEN  (InstLemmaIJ  `csm-cubical-pi`  [\mkleeneopen{}X.A\mkleeneclose{};\mkleeneopen{}Z.(A)s\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(Path\_((A)p)p  (q)p  q)\mkleeneclose{};
                                  \mkleeneopen{}(s  o  p;q)\mkleeneclose{}]\mcdot{}
                                  THENA  Auto
                                  )
                      THEN  NthHypEqGen  (-1)
                      THEN  EqCD
                      THEN  Try  (Complete  (Auto))))

---

Home Index