---

Step * 1 3 of Lemma cubical-nerve_wf

.....eq aux..... 
1. X : SmallCategory
2. X1 : L:(Cname List) ⟶ Type
⊢ I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  X  :  SmallCategory
2.  X1  :  L:(Cname  List)  {}\mrightarrow{}  Type
\mvdash{}  I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  name-morph(I;J)  {}\mrightarrow{}  (X1  I)  {}\mrightarrow{}  (X1  J)  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index