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