---

Step * 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. [f] : {f:A-face(X;A;I;alpha)| (f ∈ bx)} 
⊢ SqStable(is-A-face(X;A;I;alpha;filler I alpha J x@0 i bx;f))
BY
{ (Unfold `is-A-face` 0 THEN (D 0 THENW Auto)) }

1
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. [f] : {f:A-face(X;A;I;alpha)| (f ∈ bx)} 
11. ↓let y,b,w = f in 
     (filler I alpha J x@0 i bx alpha (y:=b)) = w ∈ A((y:=b)(alpha))
⊢ let y,b,w = f in 
(filler I alpha J x@0 i bx alpha (y:=b)) = w ∈ A((y:=b)(alpha))

---

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.  [f]  :  \{f:A-face(X;A;I;alpha)|  (f  \mmember{}  bx)\} 
\mvdash{}  SqStable(is-A-face(X;A;I;alpha;filler  I  alpha  J  x@0  i  bx;f))


By

---

Latex:
(Unfold  `is-A-face`  0  THEN  (D  0  THENW  Auto))

---

Home Index