Step
*
1
2
1
1
1
of Lemma
Kan_sigma_filler_uniform
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. K : Cname List
12. f : name-morph(I;K)
13. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
14. ↑isname(f x)
15. map(f;J) ∈ nameset(K) List
16. f x ∈ nameset(K)
17. l_subset(Cname;map(f;J);K)
18. nameset([x / J]) ⊆r name-morph-domain(f;I)
19. (filler(x;i;sigma-box-fst(bx)) alpha f)
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
⊢ sigma-box-fst(A-open-box-image(X;Σ Kan-type(A) Kan-type(B);I;K;f;alpha;bx))
= A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx))
∈ (A-face(X;Kan-type(A);K;f(alpha)) List)
BY
{ ((TACTIC:(RepUR ``sigma-box-fst A-open-box-image`` 0
THEN (RWO "map-map" 0 THENA Auto)
THEN RepUR ``compose`` 0
THEN GenConcl ⌜bx = L ∈ ({fc:A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha)| (fc ∈ bx)} List)⌝⋅)
THENA Auto
)
THEN RepeatFor 2 ((EqCD THEN Auto))
THEN TACTIC:((D -1 THEN RepeatFor 2 (D -2)) THEN RepUR ``A-face-image A-face`` 0)) }
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)))
18. K : Cname List
19. f : name-morph(I;K)
20. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
21. ↑isname(f x)
22. map(f;J) ∈ nameset(K) List
23. f x ∈ nameset(K)
24. l_subset(Cname;map(f;J);K)
25. nameset([x / J]) ⊆r name-morph-domain(f;I)
26. (filler(x;i;sigma-box-fst(bx)) alpha f)
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
∈ Kan-type(A)(f(alpha))
27. L : {fc:A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha)| (fc ∈ bx)} List
28. bx = L ∈ ({fc:A-face(X;Σ Kan-type(A) Kan-type(B);I;alpha)| (fc ∈ bx)} List)
29. x2 : nameset(I)
30. i1 : ℕ2
31. x4 : Σ Kan-type(A) Kan-type(B)((x2:=i1)(alpha))
32. (<x2, i1, x4> ∈ bx)
⊢ <f x2, i1, fst((x4 (x2:=i1)(alpha) f))>
= <f x2, i1, (fst(x4) (x2:=i1)(alpha) f)>
∈ (x:nameset(K) × i:ℕ2 × Kan-type(A)((x:=i)(f(alpha))))
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. K : Cname List
12. f : name-morph(I;K)
13. \mforall{}i:nameset(I). ((i \mmember{} J) {}\mRightarrow{} (\muparrow{}isname(f i)))
14. \muparrow{}isname(f x)
15. map(f;J) \mmember{} nameset(K) List
16. f x \mmember{} nameset(K)
17. l\_subset(Cname;map(f;J);K)
18. nameset([x / J]) \msubseteq{}r name-morph-domain(f;I)
19. (filler(x;i;sigma-box-fst(bx)) alpha f)
= filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx)))
\mvdash{} sigma-box-fst(A-open-box-image(X;\mSigma{} Kan-type(A) Kan-type(B);I;K;f;alpha;bx))
= A-open-box-image(X;Kan-type(A);I;K;f;alpha;sigma-box-fst(bx))
By
Latex:
((TACTIC:(RepUR ``sigma-box-fst A-open-box-image`` 0
THEN (RWO "map-map" 0 THENA Auto)
THEN RepUR ``compose`` 0
THEN GenConcl \mkleeneopen{}bx = L\mkleeneclose{}\mcdot{})
THENA Auto
)
THEN RepeatFor 2 ((EqCD THEN Auto))
THEN TACTIC:((D -1 THEN RepeatFor 2 (D -2)) THEN RepUR ``A-face-image A-face`` 0))
Home
Index