---

Step * 1 2 of Lemma cubical-universe_wf

.....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)
BY
{ (Reduce 0 THEN RepeatFor 4 ((FunExt THENA Auto)) THEN Reduce 0) }

1
1. I : Cname List
2. J : Cname List
3. x : name-morph(I;J)
4. x1 : {unit-cube(I) ⊢ _(Kan)}
⊢ (x1)unit-cube-map(x) ∈ {unit-cube(J) ⊢ _(Kan)}

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
\mlambda{}I,J,f,AK.  (AK)unit-cube-map(f)  \mmember{}  I:(Cname  List)
{}\mrightarrow{}  J:(Cname  List)
{}\mrightarrow{}  name-morph(I;J)
{}\mrightarrow{}  ((\mlambda{}I.\{unit-cube(I)  \mvdash{}  \_(Kan)\})  I)
{}\mrightarrow{}  ((\mlambda{}I.\{unit-cube(I)  \mvdash{}  \_(Kan)\})  J)


By

---

Latex:
(Reduce  0  THEN  RepeatFor  4  ((FunExt  THENA  Auto))  THEN  Reduce  0)

---

Home Index