---

Step * 1 of Lemma cubical-universe_wf


<λI.{unit-cube(I) ⊢ _(Kan)}, λI,J,f,AK. (AK)unit-cube-map(f)> ∈ X:L:(Cname List) ⟶ 𝕌' × (I:(Cname List)
                                                                                ⟶ J:(Cname List)
                                                                                ⟶ name-morph(I;J)
                                                                                ⟶ (X I)
                                                                                ⟶ (X J))
BY
{ MemCD }

1
.....subterm..... T:t
1:n
λI.{unit-cube(I) ⊢ _(Kan)} ∈ L:(Cname List) ⟶ 𝕌'

2
.....subterm..... T:t
2:n
λI,J,f,AK. (AK)unit-cube-map(f) ∈ I:(Cname List)
⟶ J:(Cname List)
⟶ name-morph(I;J)
⟶ ((λI.{unit-cube(I) ⊢ _(Kan)}) I)
⟶ ((λI.{unit-cube(I) ⊢ _(Kan)}) J)

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

---

Latex:

---

Latex:

<\mlambda{}I.\{unit-cube(I)  \mvdash{}  \_(Kan)\},  \mlambda{}I,J,f,AK.  (AK)unit-cube-map(f)>  \mmember{}  X:L:(Cname  List)  {}\mrightarrow{}  \mBbbU{}'  \mtimes{}  (I:(Cname  L\000Cist)
                                                                                                                                                                {}\mrightarrow{}  J:(Cname  List)
                                                                                                                                                                {}\mrightarrow{}  name-morph(I;J)
                                                                                                                                                                {}\mrightarrow{}  (X  I)
                                                                                                                                                                {}\mrightarrow{}  (X  J))


By

---

Latex:
MemCD

---

Home Index