---

Step * 2 1 2 1 1 2 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)
⊢ Kan-type(B)(((x1:=i1)(alpha);u)) ⊆r Kan-type(B)((x1:=i1)((alpha;cubeA)))
BY
{ (BLemma `subtype_rel-equal` THEN Auto) }

1
.....subterm..... T:t
2:n
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)
⊢ u = (cubeA alpha (x1:=i1)) ∈ Kan-type(A)((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;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>
\mvdash{}  Kan-type(B)(((x1:=i1)(alpha);u))  \msubseteq{}r  Kan-type(B)((x1:=i1)((alpha;cubeA)))


By

---

Latex:
(BLemma  `subtype\_rel-equal`  THEN  Auto)

---

Home Index