---

Step * 2 1 1 of Lemma Kan_sigma_filler_wf


1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. B : {X.Kan-type(A) ⊢ _(Kan)}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)
10. filler(x;i;sigma-box-fst(bx)) ∈ Kan-type(A)(alpha)
11. [%] : fills-A-open-box(X;Kan-type(A);I;alpha;sigma-box-fst(bx);filler(x;i;sigma-box-fst(bx)))
12. filler(x;i;sigma-box-snd(bx)) ∈ Kan-type(B)((alpha;filler(x;i;sigma-box-fst(bx))))
13. [%21] : fills-A-open-box(X.Kan-type(A);Kan-type(B);I;(alpha;
                                                          filler(x;i;sigma-box-fst(bx)));sigma-box-snd(bx);...)
14. j : ℕ||bx||
⊢ SqStable(is-A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha;(λI,alpha,J,x,i,bx. ...) 
                                                         I 
                                                         alpha 
                                                         J 
                                                         x 
                                                         i 
                                                         bx;bx[j]))
BY
{ TACTIC:((GenConclTerm ⌜bx[j]⌝⋅ THENA Auto)
          THEN RepeatFor 2 (D -2)
          THEN RepUR ``is-A-face let`` 0
          THEN Auto
          THEN RWO "cubical-sigma-at" 0⋅
          THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_(Kan)\}
3.  B  :  \{X.Kan-type(A)  \mvdash{}  \_(Kan)\}
4.  I  :  Cname  List
5.  alpha  :  X(I)
6.  J  :  nameset(I)  List
7.  x  :  nameset(I)
8.  i  :  \mBbbN{}2
9.  bx  :  A-open-box(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha;J;x;i)
10.  filler(x;i;sigma-box-fst(bx))  \mmember{}  Kan-type(A)(alpha)
11.  [\%]  :  fills-A-open-box(X;Kan-type(A);I;alpha;sigma-box-fst(bx);filler(x;i;sigma-box-fst(bx)))
12.  filler(x;i;sigma-box-snd(bx))  \mmember{}  Kan-type(B)((alpha;filler(x;i;sigma-box-fst(bx))))
13.  [\%21]  :  fills-A-open-box(X.Kan-type(A);Kan-type(B);I;(alpha;
                                                                                                                    filler(x;i;sigma-box-fst(bx)));...;...)
14.  j  :  \mBbbN{}||bx||
\mvdash{}  SqStable(is-A-face(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha;(\mlambda{}I,alpha,J,x,i,bx.
                                                                                                                                                        let  cubeA  =  ...  in
                                                                                                                                                          let  cubeB  =  ...  in
                                                                                                                                                          <cubeA,  cubeB>) 
                                                                                                                  I 
                                                                                                                  alpha 
                                                                                                                  J 
                                                                                                                  x 
                                                                                                                  i 
                                                                                                                  bx;bx[j]))


By

---

Latex:
TACTIC:((GenConclTerm  \mkleeneopen{}bx[j]\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  RepeatFor  2  (D  -2)
                THEN  RepUR  ``is-A-face  let``  0
                THEN  Auto
                THEN  RWO  "cubical-sigma-at"  0\mcdot{}
                THEN  Auto)

---

Home Index