---

Step * of Lemma cubical-interval-filler_wf

cubical-interval-filler() ∈ I:(Cname List)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ open_box(cubical-interval();I;J;x;i)
⟶ cubical-interval()(I)
BY
{ (Unfold `cubical-interval-filler` 0
   THEN RepeatFor 5 ((MemCD THENA Auto))
   THEN RepUR ``cubical-interval I-cube functor-ob`` 0
   THEN (BoolCase ⌜null(J)⌝⋅ THENA Auto)) }

1
1. I : Cname List
2. J : nameset(I) List
3. x : nameset(I)
4. i : ℕ2
5. bx : open_box(cubical-interval();I;J;x;i)
6. J = [] ∈ (nameset(I) List)
⊢ cube(hd(bx)) ∈ name-morph(I;[]) ⟶ ℕ2

2
1. I : Cname List
2. J : nameset(I) List
3. ¬(J = [] ∈ (nameset(I) List))
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-interval();I;J;x;i)
⊢ λL.cube(get_face(hd(J);L hd(J);bx))(L) ∈ name-morph(I;[]) ⟶ ℕ2

---

Latex:

---

Latex:
cubical-interval-filler()  \mmember{}  I:(Cname  List)
{}\mrightarrow{}  J:(nameset(I)  List)
{}\mrightarrow{}  x:nameset(I)
{}\mrightarrow{}  i:\mBbbN{}2
{}\mrightarrow{}  open\_box(cubical-interval();I;J;x;i)
{}\mrightarrow{}  cubical-interval()(I)


By

---

Latex:
(Unfold  `cubical-interval-filler`  0
  THEN  RepeatFor  5  ((MemCD  THENA  Auto))
  THEN  RepUR  ``cubical-interval  I-cube  functor-ob``  0
  THEN  (BoolCase  \mkleeneopen{}null(J)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index