Step
*
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. 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)
⊢ map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx) ∈ A-open-box(X.Kan-type(A);Kan-type(B);I;(alpha;cbA);J;x;i)
BY
{ TACTIC:MemTypeCD }
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. 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)
⊢ map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx) ∈ A-face(X.Kan-type(A);Kan-type(B);I;(alpha;cbA)) List
2
.....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)))
3
.....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. 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)
14. L : A-face(X.Kan-type(A);Kan-type(B);I;(alpha;cbA)) List
⊢ istype(A-adjacent-compatible(X.Kan-type(A);Kan-type(B);I;(alpha;cbA);L)
∧ (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2. (∃f∈L. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
∧ (∃f∈L. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈L.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈L.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈L. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2))))
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. 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{} map(\mlambda{}fc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>bx)
\mmember{} A-open-box(X.Kan-type(A);Kan-type(B);I;(alpha;cbA);J;x;i)
By
Latex:
TACTIC:MemTypeCD
Home
Index