---

Step * 2 1 2 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. filler(x;i;sigma-box-snd(bx)) ∈ Kan-type(B)((alpha;filler(x;i;sigma-box-fst(bx))))
12. j : ℕ||bx||
13. cubeA : Kan-type(A)(alpha)
14. l_subset(Cname;J;I)
15. fills-A-open-box(X;Kan-type(A);I;alpha;sigma-box-fst(bx);cubeA)
16. cubeB : Kan-type(B)((alpha;cubeA))
17. fills-A-open-box(X.Kan-type(A);Kan-type(B);I;(alpha;cubeA);sigma-box-snd(bx);cubeB)
⊢ is-A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha;<cubeA, cubeB>;bx[j])
BY
{ (All (RepUR ``fills-A-open-box fills-A-faces l_all sigma-box-fst sigma-box-snd``)
   THEN (All (RWO "length-map") THENA Auto)
   THEN ∀h:hyp. ((InstHyp [⌜j⌝] h⋅ THENA Trivial) THEN (RWO "select-map" (-1) THENA Auto) THEN Reduce (-1)) 
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConclTerm ⌜bx[j]⌝⋅ THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN (RWO "cubical-sigma-at" (-2) THENA Auto)
   THEN D -2
   THEN RepUR ``is-A-face`` 0) }

1
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)
⊢ ((cubeB (alpha;cubeA) (x1:=i1)) = v3 ∈ Kan-type(B)((x1:=i1)((alpha;cubeA))))
⇒ ((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)))

---

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.  filler(x;i;sigma-box-snd(bx))  \mmember{}  Kan-type(B)((alpha;filler(x;i;sigma-box-fst(bx))))
12.  j  :  \mBbbN{}||bx||
13.  cubeA  :  Kan-type(A)(alpha)
14.  l\_subset(Cname;J;I)
15.  fills-A-open-box(X;Kan-type(A);I;alpha;sigma-box-fst(bx);cubeA)
16.  cubeB  :  Kan-type(B)((alpha;cubeA))
17.  fills-A-open-box(X.Kan-type(A);Kan-type(B);I;(alpha;cubeA);sigma-box-snd(bx);cubeB)
\mvdash{}  is-A-face(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha;<cubeA,  cubeB>bx[j])


By

---

Latex:
(All  (RepUR  ``fills-A-open-box  fills-A-faces  l\_all  sigma-box-fst  sigma-box-snd``)
  THEN  (All  (RWO  "length-map")  THENA  Auto)
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}j\mkleeneclose{}]  h\mcdot{}  THENA  Trivial)
                              THEN  (RWO  "select-map"  (-1)  THENA  Auto)
                              THEN  Reduce  (-1)) 
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConclTerm  \mkleeneopen{}bx[j]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  (RWO  "cubical-sigma-at"  (-2)  THENA  Auto)
  THEN  D  -2
  THEN  RepUR  ``is-A-face``  0)

---

Home Index