---

Step * 1 1 of Lemma csm-singleton-type


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. H : CubicalSet{j}
5. s : H j⟶ X
6. ∀A@0:{X.A ⊢ _}. ∀a,b:{X.A ⊢ _:A@0}.
     (((Path_A@0 a b))(s o p;q) = (H.(A)s ⊢ Path_(A@0)(s o p;q) (a)(s o p;q) (b)(s o p;q)) ∈ {H.(A)s ⊢ _})
⊢ ((Path_(A)p (a)p q))(s o p;q) = (H.(A)s ⊢ Path_((A)s)p ((a)s)p q) ∈ {H.(A)s ⊢ _}
BY
{ ((RWO "-1" 0 THENM EqCDA) THEN Auto) }

1
.....wf..... 
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. H : CubicalSet{j}
5. s : H j⟶ X
6. ∀A@0:{X.A ⊢ _}. ∀a,b:{X.A ⊢ _:A@0}.
     (((Path_A@0 a b))(s o p;q) = (H.(A)s ⊢ Path_(A@0)(s o p;q) (a)(s o p;q) (b)(s o p;q)) ∈ {H.(A)s ⊢ _})
7. ((a)s)p ∈ {H.(A)s ⊢ _:((A)s)p}
⊢ cubical-type{[j' | i']:l}(H.(A)s)((A)p)(s o p;q)

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  H  :  CubicalSet\{j\}
5.  s  :  H  j{}\mrightarrow{}  X
6.  \mforall{}A@0:\{X.A  \mvdash{}  \_\}.  \mforall{}a,b:\{X.A  \mvdash{}  \_:A@0\}.
          (((Path\_A@0  a  b))(s  o  p;q)  =  (H.(A)s  \mvdash{}  Path\_(A@0)(s  o  p;q)  (a)(s  o  p;q)  (b)(s  o  p;q)))
\mvdash{}  ((Path\_(A)p  (a)p  q))(s  o  p;q)  =  (H.(A)s  \mvdash{}  Path\_((A)s)p  ((a)s)p  q)


By

---

Latex:
((RWO  "-1"  0  THENM  EqCDA)  THEN  Auto)

---

Home Index