---

Step * 1 3 of Lemma cubical-universe_wf

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index