---

Step * 1 1 of Lemma constant-Kan-type_wf


1. X1 : CubicalSet
2. X2 : I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X1;I;J;x;i) ⟶ X1(I)
3. ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(X1;I;J;x;i).
     fills-open_box(X1;I;bx;X2 I J x i bx)
4. uniform-Kan-filler(X1;X2)
5. Gamma : CubicalSet
6. I : Cname List
7. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(X1;I;J;x;i).  fills-open_box(X1;I;bx;X2 I J x i bx)
8. alpha : Gamma(I)
9. J : nameset(I) List
10. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(X1;I;J;x;i).  fills-open_box(X1;I;bx;X2 I J x i bx)
11. x : nameset(I)
12. ∀i:ℕ2. ∀bx:open_box(X1;I;J;x;i).  fills-open_box(X1;I;bx;X2 I J x i bx)
13. i : ℕ2
14. ∀bx:open_box(X1;I;J;x;i). fills-open_box(X1;I;bx;X2 I J x i bx)
15. bx : open_box(X1;I;J;x;i)
16. fills-open_box(X1;I;bx;X2 I J x i bx)
⊢ fills-A-open-box(Gamma;(X1);I;alpha;bx;(λI,alpha. (X2 I)) I alpha J x i bx)
BY
{ (Unfold `fills-open_box` -1
   THEN Unfold `fills-A-open-box` 0
   THEN Unfold `fills-faces` -1
   THEN Unfold `fills-A-faces` 0) }

1
1. X1 : CubicalSet
2. X2 : I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X1;I;J;x;i) ⟶ X1(I)
3. ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(X1;I;J;x;i).
     fills-open_box(X1;I;bx;X2 I J x i bx)
4. uniform-Kan-filler(X1;X2)
5. Gamma : CubicalSet
6. I : Cname List
7. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(X1;I;J;x;i).  fills-open_box(X1;I;bx;X2 I J x i bx)
8. alpha : Gamma(I)
9. J : nameset(I) List
10. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(X1;I;J;x;i).  fills-open_box(X1;I;bx;X2 I J x i bx)
11. x : nameset(I)
12. ∀i:ℕ2. ∀bx:open_box(X1;I;J;x;i).  fills-open_box(X1;I;bx;X2 I J x i bx)
13. i : ℕ2
14. ∀bx:open_box(X1;I;J;x;i). fills-open_box(X1;I;bx;X2 I J x i bx)
15. bx : open_box(X1;I;J;x;i)
16. (∀f∈bx.is-face(X1;I;X2 I J x i bx;f))
⊢ (∀f∈bx.is-A-face(Gamma;(X1);I;alpha;(λI,alpha. (X2 I)) I alpha J x i bx;f))

---

Latex:

---

Latex:

1.  X1  :  CubicalSet
2.  X2  :  I:(Cname  List)
{}\mrightarrow{}  J:(nameset(I)  List)
{}\mrightarrow{}  x:nameset(I)
{}\mrightarrow{}  i:\mBbbN{}2
{}\mrightarrow{}  open\_box(X1;I;J;x;i)
{}\mrightarrow{}  X1(I)
3.  \mforall{}I:Cname  List.  \mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.  \mforall{}bx:open\_box(X1;I;J;x;i).
          fills-open\_box(X1;I;bx;X2  I  J  x  i  bx)
4.  uniform-Kan-filler(X1;X2)
5.  Gamma  :  CubicalSet
6.  I  :  Cname  List
7.  \mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.  \mforall{}bx:open\_box(X1;I;J;x;i).
          fills-open\_box(X1;I;bx;X2  I  J  x  i  bx)
8.  alpha  :  Gamma(I)
9.  J  :  nameset(I)  List
10.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.  \mforall{}bx:open\_box(X1;I;J;x;i).    fills-open\_box(X1;I;bx;X2  I  J  x  i  bx)
11.  x  :  nameset(I)
12.  \mforall{}i:\mBbbN{}2.  \mforall{}bx:open\_box(X1;I;J;x;i).    fills-open\_box(X1;I;bx;X2  I  J  x  i  bx)
13.  i  :  \mBbbN{}2
14.  \mforall{}bx:open\_box(X1;I;J;x;i).  fills-open\_box(X1;I;bx;X2  I  J  x  i  bx)
15.  bx  :  open\_box(X1;I;J;x;i)
16.  fills-open\_box(X1;I;bx;X2  I  J  x  i  bx)
\mvdash{}  fills-A-open-box(Gamma;(X1);I;alpha;bx;(\mlambda{}I,alpha.  (X2  I))  I  alpha  J  x  i  bx)


By

---

Latex:
(Unfold  `fills-open\_box`  -1
  THEN  Unfold  `fills-A-open-box`  0
  THEN  Unfold  `fills-faces`  -1
  THEN  Unfold  `fills-A-faces`  0)

---

Home Index