Step
*
1
2
2
of Lemma
Kan_id_filler_uniform
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. a : {X ⊢ _:Kan-type(A)}
4. b : {X ⊢ _:Kan-type(A)}
5. I : Cname List
6. alpha : X(I)
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. bx : A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
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)
∧ (f x ∈ nameset(K))
∧ (nameset([x / J]) ⊆r name-morph-domain(f;I))
∧ l_subset(Cname;[fresh-cname(K) / map(f;J)];[fresh-cname(K) / K])
∧ ([fresh-cname(K) / map(f;J)] ∈ nameset([fresh-cname(K) / K]) List)
16. ∀z:Cname. ((z ∈ [fresh-cname(I) / J]) ⇒ (↑isname(f[fresh-cname(I):=fresh-cname(K)] z)))
⊢ (Kan_id_filler(X;A;a;b) I alpha J x i bx alpha f)
= (Kan_id_filler(X;A;a;b) K f(alpha) map(f;J) (f x) i A-open-box-image(X;(Id_Kan-type(A) a b);I;K;f;alpha;bx))
∈ (Id_Kan-type(A) a b)(f(alpha))
BY
{ Assert ⌜map(f[fresh-cname(I):=fresh-cname(K)];[fresh-cname(I) / J]) ~ [fresh-cname(K) / map(f;J)]⌝⋅ }
1
.....assertion.....
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. a : {X ⊢ _:Kan-type(A)}
4. b : {X ⊢ _:Kan-type(A)}
5. I : Cname List
6. alpha : X(I)
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. bx : A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
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)
∧ (f x ∈ nameset(K))
∧ (nameset([x / J]) ⊆r name-morph-domain(f;I))
∧ l_subset(Cname;[fresh-cname(K) / map(f;J)];[fresh-cname(K) / K])
∧ ([fresh-cname(K) / map(f;J)] ∈ nameset([fresh-cname(K) / K]) List)
16. ∀z:Cname. ((z ∈ [fresh-cname(I) / J]) ⇒ (↑isname(f[fresh-cname(I):=fresh-cname(K)] z)))
⊢ map(f[fresh-cname(I):=fresh-cname(K)];[fresh-cname(I) / J]) ~ [fresh-cname(K) / map(f;J)]
2
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. a : {X ⊢ _:Kan-type(A)}
4. b : {X ⊢ _:Kan-type(A)}
5. I : Cname List
6. alpha : X(I)
7. J : nameset(I) List
8. x : nameset(I)
9. i : ℕ2
10. bx : A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)
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)
∧ (f x ∈ nameset(K))
∧ (nameset([x / J]) ⊆r name-morph-domain(f;I))
∧ l_subset(Cname;[fresh-cname(K) / map(f;J)];[fresh-cname(K) / K])
∧ ([fresh-cname(K) / map(f;J)] ∈ nameset([fresh-cname(K) / K]) List)
16. ∀z:Cname. ((z ∈ [fresh-cname(I) / J]) ⇒ (↑isname(f[fresh-cname(I):=fresh-cname(K)] z)))
17. map(f[fresh-cname(I):=fresh-cname(K)];[fresh-cname(I) / J]) ~ [fresh-cname(K) / map(f;J)]
⊢ (Kan_id_filler(X;A;a;b) I alpha J x i bx alpha f)
= (Kan_id_filler(X;A;a;b) K f(alpha) map(f;J) (f x) i A-open-box-image(X;(Id_Kan-type(A) a b);I;K;f;alpha;bx))
∈ (Id_Kan-type(A) a b)(f(alpha))
Latex:
Latex:
1. X : CubicalSet
2. A : \{X \mvdash{} \_(Kan)\}
3. a : \{X \mvdash{} \_:Kan-type(A)\}
4. b : \{X \mvdash{} \_:Kan-type(A)\}
5. I : Cname List
6. alpha : X(I)
7. J : nameset(I) List
8. x : nameset(I)
9. i : \mBbbN{}2
10. bx : A-open-box(X;(Id\_Kan-type(A) a b);I;alpha;J;x;i)
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)
\mwedge{} (f x \mmember{} nameset(K))
\mwedge{} (nameset([x / J]) \msubseteq{}r name-morph-domain(f;I))
\mwedge{} l\_subset(Cname;[fresh-cname(K) / map(f;J)];[fresh-cname(K) / K])
\mwedge{} ([fresh-cname(K) / map(f;J)] \mmember{} nameset([fresh-cname(K) / K]) List)
16. \mforall{}z:Cname. ((z \mmember{} [fresh-cname(I) / J]) {}\mRightarrow{} (\muparrow{}isname(f[fresh-cname(I):=fresh-cname(K)] z)))
\mvdash{} (Kan\_id\_filler(X;A;a;b) I alpha J x i bx alpha f)
= (Kan\_id\_filler(X;A;a;b) K f(alpha) map(f;J) (f x) i
A-open-box-image(X;(Id\_Kan-type(A) a b);I;K;f;alpha;bx))
By
Latex:
Assert \mkleeneopen{}map(f[fresh-cname(I):=fresh-cname(K)];[fresh-cname(I) / J]) \msim{} [fresh-cname(K) / map(f;J)]\mkleeneclose{}\mcdot{}
Home
Index