---

Step * 1 1 1 2 1 1 1 of Lemma sigma-box-snd_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-face(X;Σ Kan-type(A) Kan-type(B);I;alpha) List
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
13. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
14. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
15. (∀f∈bx.(fst(f) ∈ [x / J]))
16. (∀f1,f2∈bx.  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
17. ∀i:ℕ||bx||. ∀j:ℕi.  A-face-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i])
18. map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i)
19. cbA : Kan-type(A)(alpha)
20. ∀i:ℕ||bx||. is-A-face(X;Kan-type(A);I;alpha;cbA;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx)[i])
21. i1 : ℕ||bx||@i
22. ∀j:ℕi1. A-face-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i1])
23. j : ℕi1@i
24. v : A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha)@i
25. v1 : A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha)@i
26. A-face-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;v1;v)
27. is-A-face(X;Kan-type(A);I;alpha;cbA;<fst(v), fst(snd(v)), fst(snd(snd(v)))>)
28. is-A-face(X;Kan-type(A);I;alpha;cbA;<fst(v1), fst(snd(v1)), fst(snd(snd(v1)))>)
⊢ A-face-compatible(X.Kan-type(A);Kan-type(B);I;(alpha;cbA);<fst(v1), fst(snd(v1)), snd(snd(snd(v1)))>;<fst(v), fst(snd(\000Cv)), snd(snd(snd(v)))>)
BY
{ TACTIC:(RepeatFor 2 (D -5) THEN RepeatFor 2 (D -4) THEN All (RepUR ``A-face-compatible is-A-face``)) }

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-face(X;Σ Kan-type(A) Kan-type(B);I;alpha) List
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
13. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
14. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
15. (∀f∈bx.(fst(f) ∈ [x / J]))
16. (∀f1,f2∈bx.  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
17. ∀i:ℕ||bx||. ∀j:ℕi.
      let y,b,w = bx[j] in 
      let z,c,u = bx[i] in 
      (¬(y = z ∈ Cname))
      ⇒ ((w (y:=b)(alpha) (z:=c)) = (u (z:=c)(alpha) (y:=b)) ∈ Σ Kan-type(A) Kan-type(B)(((z:=c) o (y:=b))(alpha)))
18. map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i)
19. cbA : Kan-type(A)(alpha)
20. ∀i:ℕ||bx||
      let y,b,w = map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx)[i] in 
      (cbA alpha (y:=b)) = w ∈ Kan-type(A)((y:=b)(alpha))
21. i1 : ℕ||bx||@i
22. ∀j:ℕi1
      let y,b,w = bx[j] in 
      let z,c,u = bx[i1] in 
      (¬(y = z ∈ Cname))
      ⇒ ((w (y:=b)(alpha) (z:=c)) = (u (z:=c)(alpha) (y:=b)) ∈ Σ Kan-type(A) Kan-type(B)(((z:=c) o (y:=b))(alpha)))
23. j : ℕi1@i
24. x1 : nameset(I)@i
25. i2 : ℕ2@i
26. v3 : Σ Kan-type(A) Kan-type(B)((x1:=i2)(alpha))@i
27. x2 : nameset(I)@i
28. i3 : ℕ2@i
29. v5 : Σ Kan-type(A) Kan-type(B)((x2:=i3)(alpha))@i
30. (¬(x2 = x1 ∈ Cname))
⇒ ((v5 (x2:=i3)(alpha) (x1:=i2))
   = (v3 (x1:=i2)(alpha) (x2:=i3))
   ∈ Σ Kan-type(A) Kan-type(B)(((x1:=i2) o (x2:=i3))(alpha)))
31. (cbA alpha (x1:=i2)) = (fst(v3)) ∈ Kan-type(A)((x1:=i2)(alpha))
32. (cbA alpha (x2:=i3)) = (fst(v5)) ∈ Kan-type(A)((x2:=i3)(alpha))
⊢ (¬(x2 = x1 ∈ Cname))
⇒ ((snd(v5) (x2:=i3)((alpha;cbA)) (x1:=i2))
   = (snd(v3) (x1:=i2)((alpha;cbA)) (x2:=i3))
   ∈ Kan-type(B)(((x1:=i2) o (x2:=i3))((alpha;cbA))))

---

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-face(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha)  List
10.  \mneg{}(x  \mmember{}  J)
11.  l\_subset(Cname;J;I)
12.  \mforall{}y:nameset(J).  \mforall{}c:\mBbbN{}2.    (\mexists{}f\mmember{}bx.  A-face-name(f)  =  <y,  c>)
13.  (\mexists{}f\mmember{}bx.  A-face-name(f)  =  <x,  i>)
14.  (\mforall{}f\mmember{}bx.\mneg{}(A-face-name(f)  =  <x,  1  -  i>))
15.  (\mforall{}f\mmember{}bx.(fst(f)  \mmember{}  [x  /  J]))
16.  (\mforall{}f1,f2\mmember{}bx.    \mneg{}(A-face-name(f1)  =  A-face-name(f2)))
17.  \mforall{}i:\mBbbN{}||bx||.  \mforall{}j:\mBbbN{}i.    A-face-compatible(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha;bx[j];bx[i])
18.  map(\mlambda{}fc.<fst(fc),  fst(snd(fc)),  fst(snd(snd(fc)))>bx)  \mmember{}  A-open-box(X;Kan-type(A);I;alpha;J;x;i)
19.  cbA  :  Kan-type(A)(alpha)
20.  \mforall{}i:\mBbbN{}||bx||
            is-A-face(X;Kan-type(A);I;alpha;cbA;map(\mlambda{}fc.<fst(fc),  fst(snd(fc)),  fst(snd(snd(fc)))>bx)[i])
21.  i1  :  \mBbbN{}||bx||@i
22.  \mforall{}j:\mBbbN{}i1.  A-face-compatible(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha;bx[j];bx[i1])
23.  j  :  \mBbbN{}i1@i
24.  v  :  A-face(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha)@i
25.  v1  :  A-face(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha)@i
26.  A-face-compatible(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha;v1;v)
27.  is-A-face(X;Kan-type(A);I;alpha;cbA;<fst(v),  fst(snd(v)),  fst(snd(snd(v)))>)
28.  is-A-face(X;Kan-type(A);I;alpha;cbA;<fst(v1),  fst(snd(v1)),  fst(snd(snd(v1)))>)
\mvdash{}  A-face-compatible(X.Kan-type(A);Kan-type(B);I;(alpha;cbA);<fst(v1)
                                                                                                                        ,  fst(snd(v1))
                                                                                                                        ,  snd(snd(snd(v1)))><fst(v),  fst(snd(v)\000C),  snd(snd(snd(v)))>)


By

---

Latex:
TACTIC:(RepeatFor  2  (D  -5)  THEN  RepeatFor  2  (D  -4)  THEN  All  (RepUR  ``A-face-compatible  is-A-face``))

---

Home Index