Step
*
1
1
1
2
of Lemma
sigma-box-snd_wf
.....set predicate.....
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. A-adjacent-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx)
∧ (¬(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. map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i)
12. cbA : Kan-type(A)(alpha)
13. fills-A-open-box(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx);cbA)
⊢ A-adjacent-compatible(X.Kan-type(A);Kan-type(B);I;(alpha;cbA);map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx))
∧ (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2.
(∃f∈map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx). A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
∧ (∃f∈map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx). A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx).¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx).(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx). ¬(A-face-name(f1)
= A-face-name(f2)
∈ (nameset(I) × ℕ2)))
BY
{ TACTIC:RepeatFor 5 (((ParallelOp -4 ORELSE ParallelLast) THEN (RWW "length-map" 0 THENA 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))
∧ 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);map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;
bx)[j];map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;
bx)[i1])
2
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. A-adjacent-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx)
11. ¬(x ∈ J)
12. l_subset(Cname;J;I)
13. (∀f∈bx.(fst(f) ∈ [x / J])) ∧ (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
14. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2)) ∧ (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
15. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
16. map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i)
17. cbA : Kan-type(A)(alpha)
18. fills-A-open-box(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx);cbA)
⊢ ∀y:nameset(J). ∀c:ℕ2.
(∃f∈map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx). A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
3
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. A-adjacent-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx)
11. ¬(x ∈ J)
12. l_subset(Cname;J;I)
13. (∀f∈bx.(fst(f) ∈ [x / J])) ∧ (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
14. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
15. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2)) ∧ (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i)
17. cbA : Kan-type(A)(alpha)
18. fills-A-open-box(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx);cbA)
⊢ (∃f∈map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx). A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx).¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
4
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. A-adjacent-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx)
11. ¬(x ∈ J)
12. l_subset(Cname;J;I)
13. (∀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)))
14. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
15. (∀f∈bx.(fst(f) ∈ [x / J]))
16. map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i)
17. cbA : Kan-type(A)(alpha)
18. fills-A-open-box(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx);cbA)
⊢ (∀f∈map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx).(fst(f) ∈ [x / J]))
5
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. A-adjacent-compatible(X;Σ Kan-type(A) Kan-type(B);I;alpha;bx)
11. ¬(x ∈ J)
12. l_subset(Cname;J;I)
13. (∀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)))
14. (∀f∈bx.(fst(f) ∈ [x / J]))
15. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
16. map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i)
17. cbA : Kan-type(A)(alpha)
18. fills-A-open-box(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx);cbA)
⊢ (∀f1,f2∈map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx). ¬(A-face-name(f1)
= A-face-name(f2)
∈ (nameset(I) × ℕ2)))
Latex:
Latex:
.....set predicate.....
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. A-adjacent-compatible(X;\mSigma{} Kan-type(A) Kan-type(B);I;alpha;bx)
\mwedge{} (\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. 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)
12. cbA : Kan-type(A)(alpha)
13. fills-A-open-box(X;Kan-type(A);I;alpha;map(\mlambda{}fc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>
bx);cbA)
\mvdash{} A-adjacent-compatible(X.Kan-type(A);Kan-type(B);I;(alpha;cbA);map(\mlambda{}fc.<fst(fc)
, fst(snd(fc))
, snd(snd(snd(fc)))>bx))
\mwedge{} (\mneg{}(x \mmember{} J))
\mwedge{} l\_subset(Cname;J;I)
\mwedge{} ((\mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2.
(\mexists{}f\mmember{}map(\mlambda{}fc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>bx). A-face-name(f) = <y, c>))
\mwedge{} (\mexists{}f\mmember{}map(\mlambda{}fc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>bx). A-face-name(f) = <x, i>)
\mwedge{} (\mforall{}f\mmember{}map(\mlambda{}fc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>bx).\mneg{}(A-face-name(f) = <x, 1 - i>)))
\mwedge{} (\mforall{}f\mmember{}map(\mlambda{}fc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>bx).(fst(f) \mmember{} [x / J]))
\mwedge{} (\mforall{}f1,f2\mmember{}map(\mlambda{}fc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>bx). \mneg{}(A-face-name(f1)
= A-face-name(f2)))
By
Latex:
TACTIC:RepeatFor 5 (((ParallelOp -4 ORELSE ParallelLast) THEN (RWW "length-map" 0 THENA Auto)))
Home
Index