Step
*
1
of Lemma
sigma-box-fst_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-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)
⊢ map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i)
BY
{ (D -1 THEN MemTypeCD 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. 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))
14. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
15. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
⊢ A-adjacent-compatible(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx))
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. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
14. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
15. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
18. A-adjacent-compatible(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx))
19. ¬(x ∈ J)
20. l_subset(Cname;J;I)
21. y : nameset(J)
22. c : ℕ2
⊢ (∃f∈map(λfc.<fst(fc), fst(snd(fc)), fst(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. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
14. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
15. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
18. A-adjacent-compatible(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx))
19. ¬(x ∈ J)
20. l_subset(Cname;J;I)
21. ∀y:nameset(J). ∀c:ℕ2.
(∃f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx). A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
⊢ (∃f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx). A-face-name(f) = <x, 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))
14. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
15. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
18. A-adjacent-compatible(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx))
19. ¬(x ∈ J)
20. l_subset(Cname;J;I)
21. ∀y:nameset(J). ∀c:ℕ2.
(∃f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx). A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
22. (∃f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx). A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
⊢ (∀f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx).¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
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))
14. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
15. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
18. A-adjacent-compatible(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx))
19. ¬(x ∈ J)
20. l_subset(Cname;J;I)
21. ∀y:nameset(J). ∀c:ℕ2.
(∃f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx). A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
22. (∃f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx). A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
23. (∀f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx).¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
⊢ (∀f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx).(fst(f) ∈ [x / J]))
6
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))
14. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
15. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
18. A-adjacent-compatible(X;Kan-type(A);I;alpha;map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx))
19. ¬(x ∈ J)
20. l_subset(Cname;J;I)
21. ∀y:nameset(J). ∀c:ℕ2.
(∃f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx). A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
22. (∃f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx). A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
23. (∀f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx).¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
24. (∀f∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx).(fst(f) ∈ [x / J]))
⊢ (∀f1,f2∈map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx). ¬(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-open-box(X;\mSigma{} Kan-type(A) Kan-type(B);I;alpha;J;x;i)
\mvdash{} 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)
By
Latex:
(D -1 THEN MemTypeCD THEN Auto)
Home
Index