---

Step * 1 of Lemma csm-singleton-type

.....subterm..... T:t
3:n
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. H : CubicalSet{j}
5. s : H j⟶ X
⊢ ((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
{ (InstLemmaIJ `csm-path-type`  [⌜X.A⌝;⌜H.(A)s⌝;⌜(s o p;q)⌝]⋅ THENA Auto) }

1
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 ⊢ _}

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  a  :  \{X  \mvdash{}  \_:A\}
4.  H  :  CubicalSet\{j\}
5.  s  :  H  j{}\mrightarrow{}  X
\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:
(InstLemmaIJ  `csm-path-type`    [\mkleeneopen{}X.A\mkleeneclose{};\mkleeneopen{}H.(A)s\mkleeneclose{};\mkleeneopen{}(s  o  p;q)\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index