---

Step * 1 1 1 1 of Lemma sq_stable_Kan-A-filler


1. X : CubicalSet
2. A : {X ⊢ _}
3. filler : I:(Cname List)
⟶ alpha:X(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(X;A;I;alpha;J;x;i)
⟶ A(alpha)
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x@0 : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;A;I;alpha;J;x@0;i)
10. x : nameset(I)
11. i1 : ℕ2
12. f2 : A((x:=i1)(alpha))
13. (<x, i1, f2> ∈ bx)
14. ↓(filler I alpha J x@0 i bx alpha (x:=i1)) = f2 ∈ A((x:=i1)(alpha))
⊢ Ax ∈ (filler I alpha J x@0 i bx alpha (x:=i1)) = f2 ∈ A((x:=i1)(alpha))
BY
{ (D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  filler  :  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;A;I;alpha;J;x;i)
{}\mrightarrow{}  A(alpha)
4.  I  :  Cname  List
5.  alpha  :  X(I)
6.  J  :  nameset(I)  List
7.  x@0  :  nameset(I)
8.  i  :  \mBbbN{}2
9.  bx  :  A-open-box(X;A;I;alpha;J;x@0;i)
10.  x  :  nameset(I)
11.  i1  :  \mBbbN{}2
12.  f2  :  A((x:=i1)(alpha))
13.  (<x,  i1,  f2>  \mmember{}  bx)
14.  \mdownarrow{}(filler  I  alpha  J  x@0  i  bx  alpha  (x:=i1))  =  f2
\mvdash{}  Ax  \mmember{}  (filler  I  alpha  J  x@0  i  bx  alpha  (x:=i1))  =  f2


By

---

Latex:
(D  -1  THEN  Auto)

---

Home Index