Proof of Nuprl Lemma : sigma-box-snd

Step * 1 1 1 2 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))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2.  (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
  ∧ (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
  ∧ (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈bx.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈bx.  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
11. ∀i:ℕ||bx||. ∀j:ℕi.  A-face-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i])
12. map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i)
13. cbA : Kan-type(A)(alpha)
14. fills-A-open-box(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx);cbA)
15. i1 : ℕ||bx||@i
16. ∀j:ℕi1. A-face-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i1])
17. j : ℕi1@i
18. A-face-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i1])

⊢ A-face-compatible(X.Kan-type(A);Kan-type(B);I;(alpha;cbA);<fst(bx[j]), fst(snd(bx[j])), snd(snd(snd(bx[j])))>;<fst(bx[\000Ci1]), fst(snd(bx[i1])), snd(snd(snd(bx[i1])))>)

BY
{ TACTIC:(RepUR ``fills-A-open-box fills-A-faces l_all`` -5
          THEN (RWO "length-map" (-5) THENA Auto)
          THEN (InstHyp [⌜i1⌝] (-5)⋅ THENA Auto)
          THEN ((RWO "select-map" (-1) THENA Auto) THEN Reduce (-1))
          THEN (InstHyp [⌜j⌝] (-6)⋅ THENA Auto)
          THEN (RWO "select-map" (-1) THENA Auto)
          THEN Reduce (-1)
          THEN RepeatFor 3 (MoveToConcl (-1))
          THEN ((GenConclTerm ⌜bx[i1]⌝⋅ THENA Auto) THEN Thin (-1))
          THEN (GenConclTerm ⌜bx[j]⌝⋅ THENA Auto)
          THEN Thin (-1)
          THEN Auto) }

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

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)) \mwedge{} l\_subset(Cname;J;I) \mwedge{} ((\mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}bx. A-face-name(f) = <y, c>)) \mwedge{} (\mexists{}f\mmember{}bx. A-face-name(f) = <x, i>) \mwedge{} (\mforall{}f\mmember{}bx.\mneg{}(A-face-name(f) = <x, 1 - i>))) \mwedge{} (\mforall{}f\mmember{}bx.(fst(f) \mmember{} [x / J])) \mwedge{} (\mforall{}f1,f2\mmember{}bx. \mneg{}(A-face-name(f1) = A-face-name(f2))) 11. \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]) 12. 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) 13. cbA : Kan-type(A)(alpha) 14. fills-A-open-box(X;Kan-type(A);I;alpha;map(\mlambda{}fc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))> bx);cbA) 15. i1 : \mBbbN{}||bx||@i 16. \mforall{}j:\mBbbN{}i1. A-face-compatible(X;\mSigma{} Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i1]) 17. j : \mBbbN{}i1@i 18. A-face-compatible(X;\mSigma{} Kan-type(A) Kan-type(B);I;alpha;bx[j];bx[i1]) \mvdash{} A-face-compatible(X.Kan-type(A);Kan-type(B);I;(alpha;cbA);<fst(bx[j]) , fst(snd(bx[j])) , snd(snd(snd(bx[j])))><fst(bx[i1]), fs\000Ct(snd(bx[i1])), snd(snd(snd(bx[i1])))>) By Latex: TACTIC:(RepUR ``fills-A-open-box fills-A-faces l\_all`` -5 THEN (RWO "length-map" (-5) THENA Auto) THEN (InstHyp [\mkleeneopen{}i1\mkleeneclose{}] (-5)\mcdot{} THENA Auto) THEN ((RWO "select-map" (-1) THENA Auto) THEN Reduce (-1)) THEN (InstHyp [\mkleeneopen{}j\mkleeneclose{}] (-6)\mcdot{} THENA Auto) THEN (RWO "select-map" (-1) THENA Auto) THEN Reduce (-1) THEN RepeatFor 3 (MoveToConcl (-1)) THEN ((GenConclTerm \mkleeneopen{}bx[i1]\mkleeneclose{}\mcdot{} THENA Auto) THEN Thin (-1)) THEN (GenConclTerm \mkleeneopen{}bx[j]\mkleeneclose{}\mcdot{} THENA Auto) THEN Thin (-1) THEN Auto) Home Index