Proof of Nuprl Lemma : sigma-box-snd

Step * 1 1 1 2 1 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.
      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))))
BY
{ TACTIC:((D 0 THENA Auto)
          THEN ∀h:hyp. ((RWO "cubical-sigma-at" h THENA Auto) THEN (D h THENA Auto))
          THEN Reduce 0
          THEN (D -4 THENA Auto)
          THEN Reduce (-1)) }

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)))

 ((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. u1 : Kan-type(A)((x1:=i2)(alpha))@i
27. v7 : Kan-type(B)(((x1:=i2)(alpha);u1))@i
28. x2 : nameset(I)@i
29. i3 : ℕ2@i
30. u : Kan-type(A)((x2:=i3)(alpha))@i
31. v6 : Kan-type(B)(((x2:=i3)(alpha);u))@i
32. (cbA alpha (x1:=i2)) = (fst(<u1, v7>)) ∈ Kan-type(A)((x1:=i2)(alpha))
33. (cbA alpha (x2:=i3)) = (fst(<u, v6>)) ∈ Kan-type(A)((x2:=i3)(alpha))
34. ¬(x2 = x1 ∈ Cname)
35. (<u, v6> (x2:=i3)(alpha) (x1:=i2))
= (<u1, v7> (x1:=i2)(alpha) (x2:=i3))
∈ (u:Kan-type(A)(((x1:=i2) o (x2:=i3))(alpha)) × Kan-type(B)((((x1:=i2) o (x2:=i3))(alpha);u)))
⊢ (v6 (x2:=i3)((alpha;cbA)) (x1:=i2))
= (v7 (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. let y,b,w = bx[j] in let z,c,u = bx[i] in (\mneg{}(y = z)) {}\mRightarrow{} ((w (y:=b)(alpha) (z:=c)) = (u (z:=c)(alpha) (y:=b))) 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|| let y,b,w = map(\mlambda{}fc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>bx)[i] in (cbA alpha (y:=b)) = w 21. i1 : \mBbbN{}||bx||@i 22. \mforall{}j:\mBbbN{}i1 let y,b,w = bx[j] in let z,c,u = bx[i1] in (\mneg{}(y = z)) {}\mRightarrow{} ((w (y:=b)(alpha) (z:=c)) = (u (z:=c)(alpha) (y:=b))) 23. j : \mBbbN{}i1@i 24. x1 : nameset(I)@i 25. i2 : \mBbbN{}2@i 26. v3 : \mSigma{} Kan-type(A) Kan-type(B)((x1:=i2)(alpha))@i 27. x2 : nameset(I)@i 28. i3 : \mBbbN{}2@i 29. v5 : \mSigma{} Kan-type(A) Kan-type(B)((x2:=i3)(alpha))@i 30. (\mneg{}(x2 = x1)) {}\mRightarrow{} ((v5 (x2:=i3)(alpha) (x1:=i2)) = (v3 (x1:=i2)(alpha) (x2:=i3))) 31. (cbA alpha (x1:=i2)) = (fst(v3)) 32. (cbA alpha (x2:=i3)) = (fst(v5)) \mvdash{} (\mneg{}(x2 = x1)) {}\mRightarrow{} ((snd(v5) (x2:=i3)((alpha;cbA)) (x1:=i2)) = (snd(v3) (x1:=i2)((alpha;cbA)) (x2:=i3))) By Latex: TACTIC:((D 0 THENA Auto) THEN \mforall{}h:hyp. ((RWO "cubical-sigma-at" h THENA Auto) THEN (D h THENA Auto)) THEN Reduce 0 THEN (D -4 THENA Auto) THEN Reduce (-1)) Home Index