---

Step * 2 1 2 1 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;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx)) ∈ Kan-type(A)(alpha)
11. filler(x;i;map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx))
    ∈ Kan-type(B)((alpha;filler(x;i;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx))))
12. j : ℕ||bx||
13. cubeA : Kan-type(A)(alpha)
14. l_subset(Cname;J;I)
15. ∀i:ℕ||bx||. is-A-face(X;Kan-type(A);I;alpha;cubeA;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx)[i])
16. cubeB : Kan-type(B)((alpha;cubeA))
17. ∀i:ℕ||bx||
      is-A-face(X.Kan-type(A);Kan-type(B);I;(alpha;cubeA);cubeB;map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;
                                                                    bx)[i])
18. x1 : nameset(I)
19. i1 : ℕ2
20. u : Kan-type(A)((x1:=i1)(alpha))
21. v3 : Kan-type(B)(((x1:=i1)(alpha);u))
22. bx[j] = <x1, i1, u, v3> ∈ A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha)
23. (cubeB (alpha;cubeA) (x1:=i1)) = v3 ∈ Kan-type(B)((x1:=i1)((alpha;cubeA)))
24. (cubeA alpha (x1:=i1)) = u ∈ Kan-type(A)((x1:=i1)(alpha))
⊢ (<cubeA, cubeB> alpha (x1:=i1)) = <u, v3> ∈ Σ Kan-type(A) Kan-type(B)((x1:=i1)(alpha))
BY
{ TACTIC:((RWO "cubical-sigma-at" 0 THENA Auto)
          THEN RepUR ``cubical-type-ap-morph cubical-sigma`` 0
          THEN Fold `cubical-type-ap-morph` 0
          THEN EqCD
          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;map(\mlambda{}fc.<fst(fc),  fst(snd(fc)),  fst(snd(snd(fc)))>bx))  \mmember{}  Kan-type(A)(alpha)
11.  filler(x;i;map(\mlambda{}fc.<fst(fc),  fst(snd(fc)),  snd(snd(snd(fc)))>bx))
        \mmember{}  Kan-type(B)((alpha;filler(x;i;map(\mlambda{}fc.<fst(fc),  fst(snd(fc)),  fst(snd(snd(fc)))>bx))))
12.  j  :  \mBbbN{}||bx||
13.  cubeA  :  Kan-type(A)(alpha)
14.  l\_subset(Cname;J;I)
15.  \mforall{}i:\mBbbN{}||bx||
            is-A-face(X;Kan-type(A);I;alpha;cubeA;map(\mlambda{}fc.<fst(fc),  fst(snd(fc)),  fst(snd(snd(fc)))>
                                                                                                bx)[i])
16.  cubeB  :  Kan-type(B)((alpha;cubeA))
17.  \mforall{}i:\mBbbN{}||bx||
            is-A-face(X.Kan-type(A);Kan-type(B);I;(alpha;cubeA);cubeB;map(\mlambda{}fc.<fst(fc)
                                                                                                                                                ,  fst(snd(fc))
                                                                                                                                                ,  snd(snd(snd(fc)))>bx)[i])
18.  x1  :  nameset(I)
19.  i1  :  \mBbbN{}2
20.  u  :  Kan-type(A)((x1:=i1)(alpha))
21.  v3  :  Kan-type(B)(((x1:=i1)(alpha);u))
22.  bx[j]  =  <x1,  i1,  u,  v3>
23.  (cubeB  (alpha;cubeA)  (x1:=i1))  =  v3
24.  (cubeA  alpha  (x1:=i1))  =  u
\mvdash{}  (<cubeA,  cubeB>  alpha  (x1:=i1))  =  <u,  v3>


By

---

Latex:
TACTIC:((RWO  "cubical-sigma-at"  0  THENA  Auto)
                THEN  RepUR  ``cubical-type-ap-morph  cubical-sigma``  0
                THEN  Fold  `cubical-type-ap-morph`  0
                THEN  EqCD
                THEN  Auto)

---

Home Index