Step * of Lemma cubical-interval-filler-fills

No Annotations
Kan-filler(cubical-interval();cubical-interval-filler())
BY
(D THEN Auto) }

1
1. Cname List
2. nameset(I) List
3. nameset(I)
4. : ℕ2
5. bx open_box(cubical-interval();I;J;x;i)
⊢ fills-open_box(cubical-interval();I;bx;cubical-interval-filler() bx)


Latex:


Latex:
No  Annotations
Kan-filler(cubical-interval();cubical-interval-filler())


By


Latex:
(D  0  THEN  Auto)




Home Index