---

Step * 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)
⊢ SqStable(∀I:Cname List. ∀alpha:X(I). ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:A-open-box(X;A;I;alpha;J;x;i).
             fills-A-open-box(X;A;I;alpha;bx;filler I alpha J x i bx))
BY
{ TACTIC:(Auto THEN ((Unfold `fills-A-open-box` 0 THEN Unfold `fills-A-faces` 0) ORELSE (D -1 THEN Unhide)) THEN 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)} 
⊢ SqStable(is-A-face(X;A;I;alpha;filler I alpha J x@0 i bx;f))

---

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)
\mvdash{}  SqStable(\mforall{}I:Cname  List.  \mforall{}alpha:X(I).  \mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.
                      \mforall{}bx:A-open-box(X;A;I;alpha;J;x;i).
                          fills-A-open-box(X;A;I;alpha;bx;filler  I  alpha  J  x  i  bx))


By

---

Latex:
TACTIC:(Auto
                THEN  ((Unfold  `fills-A-open-box`  0  THEN  Unfold  `fills-A-faces`  0)  ORELSE  (D  -1  THEN  Unhide))
                THEN  Auto)

---

Home Index