---

Step * 2 1 of Lemma Kanfiller_wf


1. X : CubicalSet
2. A1 : {X ⊢ _}
3. A2 : I:(Cname List)
⟶ alpha:X(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(X;A1;I;alpha;J;x;i)
⟶ A1(alpha)
4. [%1] : Kan-A-filler(X;A1;A2) ∧ uniform-Kan-A-filler(X;A1;A2)
5. I : Cname List
6. alpha : X(I)
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. bx : A-open-box(X;A1;I;alpha;J;x;i)
⊢ fills-A-open-box(X;A1;I;alpha;bx;A2 I alpha J x i bx)
BY
{ Assert ⌜Kan-A-filler(X;A1;A2)⌝⋅ }

1
.....assertion..... 
1. X : CubicalSet
2. A1 : {X ⊢ _}
3. A2 : I:(Cname List)
⟶ alpha:X(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(X;A1;I;alpha;J;x;i)
⟶ A1(alpha)
4. [%1] : Kan-A-filler(X;A1;A2) ∧ uniform-Kan-A-filler(X;A1;A2)
5. I : Cname List
6. alpha : X(I)
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. bx : A-open-box(X;A1;I;alpha;J;x;i)
⊢ Kan-A-filler(X;A1;A2)

2
1. X : CubicalSet
2. A1 : {X ⊢ _}
3. A2 : I:(Cname List)
⟶ alpha:X(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(X;A1;I;alpha;J;x;i)
⟶ A1(alpha)
4. [%1] : Kan-A-filler(X;A1;A2) ∧ uniform-Kan-A-filler(X;A1;A2)
5. I : Cname List
6. alpha : X(I)
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. bx : A-open-box(X;A1;I;alpha;J;x;i)
11. Kan-A-filler(X;A1;A2)
⊢ fills-A-open-box(X;A1;I;alpha;bx;A2 I alpha J x i bx)

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A1  :  \{X  \mvdash{}  \_\}
3.  A2  :  I:(Cname  List)
{}\mrightarrow{}  alpha:X(I)
{}\mrightarrow{}  J:(nameset(I)  List)
{}\mrightarrow{}  x:nameset(I)
{}\mrightarrow{}  i:\mBbbN{}2
{}\mrightarrow{}  A-open-box(X;A1;I;alpha;J;x;i)
{}\mrightarrow{}  A1(alpha)
4.  [\%1]  :  Kan-A-filler(X;A1;A2)  \mwedge{}  uniform-Kan-A-filler(X;A1;A2)
5.  I  :  Cname  List
6.  alpha  :  X(I)
7.  J  :  nameset(I)  List
8.  x  :  nameset(I)
9.  i  :  \mBbbN{}2
10.  bx  :  A-open-box(X;A1;I;alpha;J;x;i)
\mvdash{}  fills-A-open-box(X;A1;I;alpha;bx;A2  I  alpha  J  x  i  bx)


By

---

Latex:
Assert  \mkleeneopen{}Kan-A-filler(X;A1;A2)\mkleeneclose{}\mcdot{}

---

Home Index