---

Step * 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. Kan-filler(X1;X2)
4. uniform-Kan-filler(X1;X2)
5. Gamma : CubicalSet
⊢ Kan-A-filler(Gamma;(X1);λI,alpha. (X2 I))
BY
{ (Unfold `Kan-filler` -3
   THEN Unfold `Kan-A-filler` 0
   THEN ParallelOp -3
   THEN (D 0 THENA Auto)
   THEN (RWO "constant-A-open-box" 0 THENA Auto)
   THEN ParallelOp -2
   THEN RepeatFor 3 (ParallelLast)) }

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. 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)

---

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.  Kan-filler(X1;X2)
4.  uniform-Kan-filler(X1;X2)
5.  Gamma  :  CubicalSet
\mvdash{}  Kan-A-filler(Gamma;(X1);\mlambda{}I,alpha.  (X2  I))


By

---

Latex:
(Unfold  `Kan-filler`  -3
  THEN  Unfold  `Kan-A-filler`  0
  THEN  ParallelOp  -3
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "constant-A-open-box"  0  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  RepeatFor  3  (ParallelLast))

---

Home Index