---

Step * 2 1 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 ⊢ _}
⊢ 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 ⊢ _}
BY
{ (EqCD THEN Try (Trivial) THEN Try (MemberAuto)) }

1
.....subterm..... T:t
2:n
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 ⊢ _}
⊢ ((A)s)p = ((A)p)(s o p;q) ∈ {Z.(A)s ⊢ _}

2
.....subterm..... T:t
3:n
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) = ((Path_((A)p)p (q)p q))((s o p;q) o p;q) ∈ {Z.(A)s.((A)s)p ⊢ _}

---

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{}  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)


By

---

Latex:
(EqCD  THEN  Try  (Trivial)  THEN  Try  (MemberAuto))

---

Home Index