---

Step * of Lemma Kan-interval_wf

Kan-interval() ∈ KanCubicalSet
BY
{ TACTIC:(MemTypeCD THEN Auto THEN Unfold `Kan-interval` 0 THEN Reduce 0 THEN Auto THEN D 0 THEN Auto) }

1
1. Kan-filler(cubical-interval();cubical-interval-filler())
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-interval();I;J;x;i)
7. K : Cname List
8. f : name-morph(I;K)
9. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
10. ↑isname(f x)
⊢ f(cubical-interval-filler() I J x i bx)
= (cubical-interval-filler() K map(f;J) (f x) i open_box_image(cubical-interval();I;K;f;bx))
∈ cubical-interval()(K)

---

Latex:

---

Latex:
Kan-interval()  \mmember{}  KanCubicalSet


By

---

Latex:
TACTIC:(MemTypeCD  THEN  Auto  THEN  Unfold  `Kan-interval`  0  THEN  Reduce  0  THEN  Auto  THEN  D  0  THEN  Auto)

---

Home Index