---

Step * 1 3 of Lemma csm-cubical-pi

.....eq aux..... 
1. X : CubicalSet
2. Delta : CubicalSet
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. s : Delta ⟶ X
6. A1 : I:(Cname List) ⟶ Delta(I) ⟶ Type
⊢ (I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:Delta(I) ⟶ (A1 I a) ⟶ (A1 J f(a)))
= (I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:Delta(I) ⟶ (A1 I a) ⟶ (A1 J f(a)))
∈ Type
BY
{ xxxAutoxxx }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  X  :  CubicalSet
2.  Delta  :  CubicalSet
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  s  :  Delta  {}\mrightarrow{}  X
6.  A1  :  I:(Cname  List)  {}\mrightarrow{}  Delta(I)  {}\mrightarrow{}  Type
\mvdash{}  (I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  f:name-morph(I;J)  {}\mrightarrow{}  a:Delta(I)  {}\mrightarrow{}  (A1  I  a)  {}\mrightarrow{}  (A1  J  f(a)))
=  (I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  f:name-morph(I;J)  {}\mrightarrow{}  a:Delta(I)  {}\mrightarrow{}  (A1  I  a)  {}\mrightarrow{}  (A1  J  f(a)))


By

---

Latex:
xxxAutoxxx

---

Home Index