From 739ac71817d974848df28dea50ec71a83549a681 Mon Sep 17 00:00:00 2001 From: StiephenPradal Date: Tue, 24 Oct 2023 11:03:45 +0100 Subject: [PATCH 01/12] Corollary 8.20 + commented out stuff --- src/simplicial-hott/08-covariant.rzk.md | 696 ++++++++++++++++++++++++ 1 file changed, 696 insertions(+) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index c369dda1..65f36bb6 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -22,6 +22,7 @@ This is a literate `rzk` file: Some of the definitions in this file rely on extension extensionality: ```rzk +#assume funext : FunExt #assume extext : ExtExt #assume weakfunext : WeakFunExt #assume naiveextext : NaiveExtExt @@ -2277,3 +2278,698 @@ are discrete. ( is-covariant-representable-is-segal A is-segal-A x) ( y) ``` + +In particular, in discrete types identity types are discrete. + +```rzk title="RS17, Corollary 8.20" + +-- -- useless +-- #def map-inverse-is-equiv +-- ( A B : U) +-- ( f : A → B) +-- ( is-equiv-f : is-equiv A B f) +-- : B → A +-- := +-- π₁ (has-inverse-is-equiv A B f is-equiv-f) + +-- -- inverse map of idtoarr but probably useless now +-- #def inverse-hom-eq-id-type +-- ( A : U) +-- ( is-discrete-A : is-discrete A) +-- ( x y : A) +-- ( p q : x = y) +-- : (hom (x = y) p q) → (p = q) +-- := +-- comp +-- ( hom (x = y) p q) +-- ( (hom-eq A x y p) = (hom-eq A x y q)) +-- ( p = q) +-- ( ap-cancel-has-retraction ( x = y) ( hom A x y) +-- ( hom-eq A x y) +-- ( π₁ (is-discrete-A x y)) +-- ( p) +-- ( q)) +-- ( comp +-- ( hom (x = y) p q) +-- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y q)) +-- ( (hom-eq A x y p) = (hom-eq A x y q)) +-- ( map-inverse-is-equiv +-- ( (hom-eq A x y p) = (hom-eq A x y q)) +-- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y q)) +-- ( hom-eq (hom A x y) (hom-eq A x y p) (hom-eq A x y q)) +-- ( (is-discrete-hom-is-segal ( A) +-- ( is-segal-is-discrete extext A is-discrete-A) +-- ( x) +-- ( y)) +-- ( hom-eq A x y p) +-- ( hom-eq A x y q))) +-- ( ap-hom ( x = y) ( hom A x y) ( hom-eq A x y) ( p) ( q))) + +-- #def p₁ +-- ( A : U) +-- ( is-discrete-A : is-discrete A) +-- ( x y : A) +-- ( p : x = y) +-- : ( inverse-hom-eq-id-type A is-discrete-A x y p p) ( id-hom (x = y) p) +-- = +-- ( comp +-- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) +-- ( (hom-eq A x y p) = (hom-eq A x y p)) +-- ( p = p) +-- ( ap-cancel-has-retraction ( x = y) ( hom A x y) +-- ( hom-eq A x y) +-- ( π₁ (is-discrete-A x y)) +-- ( p) +-- ( p)) +-- ( map-inverse-is-equiv +-- ( (hom-eq A x y p) = (hom-eq A x y p)) +-- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) +-- ( hom-eq (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) +-- ( (is-discrete-hom-is-segal ( A) +-- ( is-segal-is-discrete extext A is-discrete-A) +-- ( x) +-- ( y)) +-- ( hom-eq A x y p) +-- ( hom-eq A x y p)))) ( id-hom (hom A x y) (hom-eq A x y p)) +-- := +-- ap +-- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) +-- ( p = p) +-- ( ap-hom ( x = y) ( hom A x y) +-- ( hom-eq A x y) +-- ( p) ( p) +-- ( id-hom ( x = y) p)) +-- ( id-hom ( hom A x y) ( hom-eq A x y p)) +-- ( comp +-- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) +-- ( (hom-eq A x y p) = (hom-eq A x y p)) +-- ( p = p) +-- ( ap-cancel-has-retraction ( x = y) ( hom A x y) +-- ( hom-eq A x y) +-- ( π₁ (is-discrete-A x y)) +-- ( p) +-- ( p)) +-- ( map-inverse-is-equiv +-- ( (hom-eq A x y p) = (hom-eq A x y p)) +-- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) +-- ( hom-eq ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) +-- ( ( is-discrete-hom-is-segal ( A) +-- ( is-segal-is-discrete extext A is-discrete-A) +-- ( x) +-- ( y)) +-- ( hom-eq A x y p) +-- ( hom-eq A x y p)))) +-- ( functors-pres-id extext ( x = y) ( hom A x y) +-- (hom-eq A x y) ( p)) + +-- #def p₂ +-- ( A : U) +-- ( is-discrete-A : is-discrete A) +-- ( x y : A) +-- ( p : x = y) +-- : ( comp +-- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) +-- ( (hom-eq A x y p) = (hom-eq A x y p)) +-- ( p = p) +-- ( ap-cancel-has-retraction ( x = y) ( hom A x y) +-- ( hom-eq A x y) +-- ( π₁ (is-discrete-A x y)) +-- ( p) +-- ( p)) +-- ( map-inverse-is-equiv +-- ( (hom-eq A x y p) = (hom-eq A x y p)) +-- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) +-- ( hom-eq (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) +-- ( (is-discrete-hom-is-segal ( A) +-- ( is-segal-is-discrete extext A is-discrete-A) +-- ( x) +-- ( y)) +-- ( hom-eq A x y p) +-- ( hom-eq A x y p)))) ( id-hom (hom A x y) (hom-eq A x y p)) +-- = +-- ( ( ap-cancel-has-retraction ( x = y) ( hom A x y) +-- ( hom-eq A x y) +-- ( π₁ (is-discrete-A x y)) +-- ( p) +-- ( p)) (refl_{hom-eq A x y p})) +-- := +-- ap +-- ( (hom-eq A x y p) = (hom-eq A x y p)) +-- ( p = p) +-- ( (map-inverse-is-equiv +-- ( (hom-eq A x y p) = (hom-eq A x y p)) +-- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) +-- ( hom-eq (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) +-- ( (is-discrete-hom-is-segal ( A) +-- ( is-segal-is-discrete extext A is-discrete-A) +-- ( x) +-- ( y)) +-- ( hom-eq A x y p) +-- ( hom-eq A x y p))) ( id-hom (hom A x y) (hom-eq A x y p))) +-- ( refl_{hom-eq A x y p}) +-- ( ap-cancel-has-retraction ( x = y) ( hom A x y) +-- ( hom-eq A x y) +-- ( π₁ (is-discrete-A x y)) +-- ( p) +-- ( p)) +-- ( (π₂ +-- (π₁ +-- ( +-- (is-discrete-hom-is-segal ( A) +-- ( is-segal-is-discrete extext A is-discrete-A) +-- ( x) +-- ( y) +-- ) +-- (hom-eq A x y p) +-- (hom-eq A x y p) +-- ) +-- ) +-- ) +-- (refl_{hom-eq A x y p}) +-- ) + +-- --inverse map of ap +-- #def inv-ap-is-equiv +-- ( A B : U) +-- ( f : A → B) +-- ( is-equiv-f : is-equiv A B f) +-- ( x y : A) +-- : (f x = f y) → (x = y) +-- := +-- \ p' → +-- triple-concat A x +-- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) x) +-- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) y) +-- ( y) +-- ( rev A ((comp A B A (π₁ (π₁ is-equiv-f)) f) x) x +-- ( (π₂ (π₁ is-equiv-f)) x)) +-- ( ap B A (f x) (f y) (π₁ (π₁ is-equiv-f)) p') +-- ( (π₂ (π₁ is-equiv-f)) y) + +-- -- finished but can do better with ind-path +-- #def has-retraction-ap-is-equiv +-- ( A B : U) +-- ( f : A → B) +-- ( is-equiv-f : is-equiv A B f) +-- ( x y : A) +-- : has-retraction (x = y) ((f x) = (f y)) (ap A B x y f) +-- := +-- ( inv-ap-is-equiv A B f is-equiv-f x y, +-- \ p' → +-- triple-concat (x = y) +-- ( inv-ap-is-equiv A B f is-equiv-f x y ( ap A B x y f p')) +-- ( triple-concat A x +-- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) x) +-- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) y) +-- ( y) +-- ( rev A ((comp A B A (π₁ (π₁ is-equiv-f)) f) x) x +-- ( (π₂ (π₁ is-equiv-f)) x)) +-- ( ap A A x y (comp A B A (π₁ (π₁ is-equiv-f)) f) p') +-- ( (π₂ (π₁ is-equiv-f)) y)) +-- ( ap A A x y (identity A) p') +-- ( p') +-- ( ap +-- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) x = (comp A B A (π₁ (π₁ is-equiv-f)) f) y) +-- ( x = y) +-- ( ap B A (f x) (f y) (π₁ (π₁ is-equiv-f)) (ap A B x y f p')) +-- ( ap A A x y (comp A B A (π₁ (π₁ is-equiv-f)) f) p') +-- ( \ q' → +-- triple-concat A x +-- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) x) +-- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) y) +-- ( y) +-- ( rev A ((comp A B A (π₁ (π₁ is-equiv-f)) f) x) x +-- ( (π₂ (π₁ is-equiv-f)) x)) +-- ( q') +-- ( (π₂ (π₁ is-equiv-f)) y)) +-- ( rev-ap-comp A B A x y f (π₁ (π₁ is-equiv-f)) p')) -- ap_{conj}(rev-ap-comp +-- ( triple-concat-nat-htpy A A +-- ( comp A B A (π₁ (π₁ is-equiv-f)) f) +-- ( identity A) +-- ( π₂ (π₁ is-equiv-f)) +-- ( x) +-- ( y) +-- ( p')) +-- ( ap-id A x y p')) + + +-- -- #def has-section-ap-is-equiv +-- -- ( A B : U) +-- -- ( f : A → B) +-- -- ( is-equiv-f : is-equiv A B f) +-- -- ( x y : A) +-- -- : has-section (x = y) ((f x) = (f y)) (ap A B x y f) +-- -- := TODO but horrible path algerba + + +-- -- #def η-ap +-- -- ( A B : U) +-- -- ( f : A → B) +-- -- ( is-equiv-f : is-equiv A B f) +-- -- ( x y : A) +-- -- : is-equiv (x = y) ((f x) = (f y)) (ap A B x y f) +-- -- := +-- -- ( (((second (first is-equiv-f)) x) . +-- -- ap +-- -- () +-- -- () +-- -- () +-- -- (map-inverse-is-equiv A B f is-equiv-f) . +-- -- rev ((second (first is-equiv-f)) y), +-- -- has-retract), +-- -- (map-inverse-is-equiv A B f is-equiv-f, +-- -- has-section)) + + + + +-- -- to finish, perhaps +-- #def has-retraction-inverse-hom-eq-id-type +-- ( A : U) +-- ( is-discrete-A : is-discrete A) +-- ( x y : A) +-- ( p q : x = y) +-- : has-retraction (p = q) (hom (x = y) p q) (hom-eq (x = y) p q) +-- := +-- ( inverse-hom-eq-id-type A is-discrete-A x y p q, +-- ( \ α → +-- ind-path ( x = y) ( p) +-- ( \ q' α' → +-- comp ( p = q') ( hom (x = y) p q') ( p = q') +-- ( inverse-hom-eq-id-type A is-discrete-A x y p q') +-- ( hom-eq (x = y) p q') +-- ( α') +-- = α') +-- ( ap +-- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) +-- ( p = p) +-- ( ap-hom ( x = y) ( hom A x y) +-- ( hom-eq A x y) +-- ( p) ( p) +-- ( id-hom ( x = y) p)) +-- ( id-hom ( hom A x y) ( hom-eq A x y p)) +-- ( comp +-- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) +-- ( (hom-eq A x y p) = (hom-eq A x y p)) +-- ( p = p) +-- ( ap-cancel-has-retraction ( x = y) ( hom A x y) +-- ( hom-eq A x y) +-- ( first (is-discrete-A x y)) +-- ( p) +-- ( p)) +-- ( map-inverse-is-equiv +-- ( (hom-eq A x y p) = (hom-eq A x y p)) +-- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) +-- ( hom-eq (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) +-- ( (is-discrete-hom-is-segal ( A) +-- ( is-segal-is-discrete extext A is-discrete-A) +-- ( x) +-- ( y)) +-- ( hom-eq A x y p) +-- ( hom-eq A x y p)))) +-- (functors-pres-id extext ( x = y) ( hom A x y) +-- ( hom-eq A x y) ( p))) -- concatenate p₁ p₂ and retraction ap φ is-equiv-φ +-- ( q) +-- ( α) +-- ) +-- ) + +-- #def has-section-inverse-hom-eq-id-type +-- ( A : U) +-- ( is-discrete-A : is-discrete A) +-- ( x y : A) +-- ( p q : x = y) +-- : has-section (p = q) (hom (x = y) p q) (hom-eq (x = y) p q) +-- := +-- ( inverse-hom-eq-id-type A is-discrete-A x y p q, +-- ( -- to fill +-- )) + +-- -- composition ap_{hom-eq}^{-1} o hom-eq^{-1} o ap-hom hom-eq with hom-eq is section and retraction +-- #def is-discrete-id-type-is-discrete +-- ( A : U) +-- ( is-discrete-A : is-discrete A) +-- ( x y : A) +-- : is-discrete (x = y) +-- := +-- \ p q → +-- is-equiv-has-inverse ( p = q) ( hom (x = y) p q) +-- ( hom-eq (x = y) p q) +-- ( inverse-hom-eq-id-type A is-discrete-A x y p q), +-- ( second has-retraction-inverse-hom-eq-id-type, +-- second has-section-inverse-hom-eq-id-type) +``` + +```rzk title="RS17, Corollary 8.19" + +-- #def precomp +-- ( A B : U) +-- ( P : B → U) +-- ( f : A → B) +-- : ((y : B) → P y) → ((x : A) → P (f x)) +-- := +-- \ α → (\ x → α (f x)) + +-- #def precomp-with-inv +-- ( A B : U) +-- ( P : B → U) +-- ( f : A → B) +-- ( is-equiv-f : is-equiv A B f) +-- : ((x : A) → P (f x)) → ((y : B) → P y) +-- := +-- \ β → +-- transport ( B → B) +-- ( \ f' → ((y : B) → P (f' y))) +-- ( comp B A B f (π₁ (π₂ is-equiv-f))) +-- ( identity B) +-- ( eq-htpy funext B (\ b' → B) +-- ( comp B A B f (π₁ (π₂ is-equiv-f))) +-- ( identity B) +-- (π₂ (π₂ is-equiv-f))) +-- ( precomp B A ( \ x' → P (f x')) +-- ( π₁ (π₂ is-equiv-f)) +-- ( β)) + +-- #def is-equiv-precomp-equiv +-- ( A B : U) +-- ( P : B → U) +-- ( f : A → B) +-- ( is-equiv-f : is-equiv A B f) +-- : Equiv ((y : B) → P y) ((x : A) → P (f x)) +-- := +-- ( precomp A B P f +-- , is-equiv-is-contr-map ((y : B) → P y) ((x : A) → P (f x)) (precomp A B P f) +-- ( \ β → +-- is-contr-equiv-is-contr' +-- ( fib +-- ( (y : B) → P y) +-- ( (x : A) → P (f x)) +-- ( precomp A B P f) +-- ( β)) +-- ( Σ (α : ((y : B) → P y)) , +-- ( α = precomp-with-inv A B P f is-equiv-f β)) +-- ( total-equiv-family-of-equiv +-- ( (y : B) → P y) +-- ( \ α → (precomp A B P f α) = β) +-- ( \ α → α = (precomp-with-inv A B P f is-equiv-f β))) +-- -- TODO: show that (α ∘ f = β) ≅ (α = tr (β ∘ f⁻¹) +-- ( is-contr-endpoint-based-paths +-- ( (y : B) → P y) +-- ( precomp-with-inv A B P f is-equiv-f β)))) + + + +#def hom-eq-ap-ap-hom-commute + ( A B : U) + ( f : A → B) + ( x y : A) + ( p : x = y) + : + comp (x = y) (hom A x y) (hom B (f x) (f y)) + ( ap-hom A B f x y) + ( hom-eq A x y) + ( p) + = + comp (x = y) ((f x) = (f y)) (hom B (f x) (f y)) + ( hom-eq B (f x) (f y)) + ( ap A B x y f) + ( p) + := + ind-path A x + ( \ y' p' → + comp (x = y') (hom A x y') (hom B (f x) (f y')) + ( ap-hom A B f x y') + ( hom-eq A x y') + ( p') + = + comp (x = y') ((f x) = (f y')) (hom B (f x) (f y')) + ( hom-eq B (f x) (f y')) + ( ap A B x y' f) + ( p')) + ( functors-pres-id extext A B f x) + ( y) + ( p) + +-- useless: hold judgmentaly +-- #def ap-hom-comp +-- ( A B C : U) +-- ( f : A → B) +-- ( g : B → C) +-- ( x y : A) +-- : comp (hom A x y) (hom B (f x) (f y)) (hom C (g (f x)) (g (f y))) +-- ( ap-hom B C g (f x) (f y)) +-- ( ap-hom A B f x y) +-- = +-- ap-hom A C (comp A B C g f) x y +-- := refl + +#def left-cancel-is-equiv + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + : (comp A B A (π₁ (π₁ is-equiv-f)) f) = (identity A) + := + eq-htpy funext A (\ x' → A) + ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( identity A) + ( π₂ (π₁ is-equiv-f)) + +#def right-cancel-is-equiv + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + : (comp B A B f (π₁ (π₂ is-equiv-f))) = (identity B) + := + eq-htpy funext B (\ x' → B) + ( comp B A B f (π₁ (π₂ is-equiv-f))) + ( identity B) + ( π₂ (π₂ is-equiv-f)) + +#def coherence-hae-is-equiv + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + : comp A B ((y' : B) → (comp B A B f (π₁ (π₁ is-equiv-f)) y') = y') + ( π₂ (π₂ is-equiv-f)) + ( f) + = + ap A B + (comp A B A (π₁ (π₁ is-equiv-f)) f) + (identity A) + ((π₂ (π₁ is-equiv-f))) + := + eq-htpy A (\ x' → triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f x') + ( comp A B ((y' : B) → (comp B A B f (π₁ (π₁ is-equiv-f)) y') = y') + ( π₂ (π₂ is-equiv-f)) + ( f)) + ( ap A B + (comp A B A (π₁ (π₁ is-equiv-f)) f) + (identity A) + ((π₂ (π₁ is-equiv-f)))) + ( coherence-is-half-adjoint-equiv A B f + ( is-half-adjoint-equiv-is-equiv A B f is-equiv-f)) + + +#def comp-homotopic-maps + ( A B C : U) + ( f g : A → B) + ( h k : B → C) + ( p : f = g) + ( q : h = k) + : comp A B C h f = comp A B C k g + := + ind-path (A → B) f (\ g' p' → comp A B C h f = comp A B C k g') + ( ind-path (B → C) h (\ k' q' → comp A B C h f = comp A B C k' f) + ( refl) + ( k) + ( q)) + ( g) + ( p) + +#def inv-ap-hom-equiv uses (funext) + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + ( x y : A) + : (hom B (f x) (f y)) → (hom A x y) + := + comp + ( hom B (f x) (f y)) + ( hom A ((π₁ (π₁ is-equiv-f)) (f x)) ((π₁ (π₁ is-equiv-f))(f y))) + ( hom A x y) + ( transport (A → A) (\ g' → (hom A (g' x) (g' y))) + ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( identity A) + ( left-cancel-is-equiv A B f is-equiv-f)) + ( ap-hom B A (π₁ (π₁ is-equiv-f)) (f x) (f y)) + + +#def has-retraction-ap-hom-equiv uses (funext) + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + ( x y : A) + : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) + := + ( inv-ap-hom-equiv A B f is-equiv-f x y + , \ α → + apd (A → A) (\ g' → (hom A (g' x) (g' y))) + ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( identity A) + ( \ g' → ap-hom A A g' x y α) + ( left-cancel-is-equiv A B f is-equiv-f)) + +#def ap-hom-naturality + ( A B C : U) + ( f g : A → B) + ( h k : B → C) + ( p : f = g) + ( q : h = k) + ( x y : A) + : comp (hom B (f x) (f y)) (hom B (g x) (g y)) (hom C (k (g x)) (k (g y))) + ( ap-hom B C k (g x) (g y)) + ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g p) + = + comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g x)) (k (g y))) + ( transport (A → C) (\ f' → hom C (f' x) (f' y)) + ( comp A B C h f) + ( comp A B C k g) + ( comp-homotopic-maps A B C f g h k p q)) + ( ap-hom B C h (f x) (f y)) + := + ind-path (A → B) f + ( \ g' p' → + comp (hom B (f x) (f y)) (hom B (g' x) (g' y)) (hom C (k (g' x)) (k (g' y))) + ( ap-hom B C k (g' x) (g' y)) + ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g' p') + = + comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g' x)) (k (g' y))) + ( transport (A → C) (\ f' → hom C (f' x) (f' y)) + ( comp A B C h f) + ( comp A B C k g') + ( comp-homotopic-maps A B C f g' h k p' q)) + ( ap-hom B C h (f x) (f y))) + ( ind-path (B → C) h + ( \ k' q' → + comp (hom B (f x) (f y)) (hom B (f x) (f y)) (hom C (k' (f x)) (k' (f y))) + ( ap-hom B C k' (f x) (f y)) + ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f f refl) + = + comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k' (f x)) (k' (f y))) + ( transport (A → C) (\ f' → hom C (f' x) (f' y)) + ( comp A B C h f) + ( comp A B C k' f) + ( comp-homotopic-maps A B C f f h k' refl q')) + ( ap-hom B C h (f x) (f y))) + ( refl) + ( k) + ( q)) + ( g) + ( p) + +#def has-section-ap-hom-equiv uses (funext) + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + ( x y : A) + : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) + := + ( inv-ap-hom-equiv A B f is-equiv-f x y + , \ α → + concat (hom B (f x) (f y)) + ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) + ( ap-hom A B f x y) + ( inv-ap-hom-equiv A B f is-equiv-f x y) + ( α)) + ( transport (A → A) (\ g' → hom A (g x) (g y)) + ( triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f) + ( f) + ( ap A B + ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( identity A) + ( f) + ( left-cancel-is-equiv A B f is-equiv-f)) + ( α)) + ( α) + ( ap-hom-naturality A A A B -- path 1 + ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( identity A) + ( f) + ( f) + ( left-cancel-is-equiv A B f is-equiv-f) + ( refl) + ( x) + ( y)) + + ) + + + -- triple-concat (hom B (f x) (f y)) + -- ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) + -- ( ap-hom A B f x y) + -- ( inv-ap-hom-equiv A B f is-equiv-f x y) + -- ( α)) + -- ( transport (A → A) (\ g' → hom A (g x) (g y)) + -- ( triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f) + -- ( f) + -- ( ap A B + -- ( comp A B A (π₁ (π₁ is-equiv-f)) f) + -- ( identity A) + -- ( f) + -- ( left-cancel-is-equiv A B f is-equiv-f)) + -- ( α)) + -- ( transport) + -- ( α) + + + + + + + + -- : ( α : hom A x y) → + -- ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) + -- ( ap-hom A B f x y) + -- ( inv-ap-hom-equiv A B f is-equiv-f x y) + -- ( α) + -- = α) + -- := + +#def equiv-preserve-discretness uses (extext funext) + ( A B : U) + ( (f, is-equiv-f) : Equiv A B) + ( is-discrete-B : is-discrete B) + : is-discrete A + := + \ x y → + is-equiv-right-cancel (x = y) (hom A x y) (hom B (f x) (f y)) + ( hom-eq A x y) + ( ap-hom A B f x y) + ( has-retraction-ap-hom-equiv A B f is-equiv-f x y) + ( is-equiv-homotopy (x = y) (hom B (f x) (f y)) + ( comp (x = y) (hom A x y) (hom B (f x) (f y)) + ( ap-hom A B f x y) + ( hom-eq A x y)) + ( comp (x = y) ((f x) = (f y)) (hom B (f x) (f y)) + ( hom-eq B (f x) (f y)) + ( ap A B x y f)) + ( hom-eq-ap-ap-hom-commute A B f x y) + ( is-equiv-comp (x = y) ((f x) = (f y)) (hom B (f x) (f y)) + ( ap A B x y f) + ( is-emb-is-equiv A B f is-equiv-f x y) + ( hom-eq B (f x) (f y)) + ( is-discrete-B (f x) (f y)))) + +#def is-discrete-id-path-is-discrete uses (extext funext) + ( A : U) + ( is-discrete-A : is-discrete A) + ( x y : A) + : is-discrete (x = y) + := + equiv-preserve-discretness (x = y) (hom A x y) + ( hom-eq A x y , is-discrete-A x y) + ( is-discrete-hom-is-segal A + ( is-segal-is-discrete extext A is-discrete-A) + ( x) ( y)) + +``` From 603ec2f0ab0e652cd298d7e517534c40165656a9 Mon Sep 17 00:00:00 2001 From: StiephenPradal Date: Thu, 26 Oct 2023 17:28:52 +0100 Subject: [PATCH 02/12] f_# is an equiv if f is an equiv --- src/hott/02-homotopies.rzk.md | 21 + src/hott/03-equivalences.rzk.md | 22 + src/simplicial-hott/03-extension-types.rzk.md | 19 + .../06-2cat-of-segal-types.rzk.md | 341 ++++++++++ src/simplicial-hott/08-covariant.rzk.md | 626 +----------------- 5 files changed, 406 insertions(+), 623 deletions(-) diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md index 70132dd9..9b4f8a6b 100644 --- a/src/hott/02-homotopies.rzk.md +++ b/src/hott/02-homotopies.rzk.md @@ -90,6 +90,27 @@ unlike composition. g ``` +## Composition of equal maps + +```rzk + +#def comp-homotopic-maps + ( A B C : U) + ( f g : A → B) + ( h k : B → C) + ( p : f = g) + ( q : h = k) + : comp A B C h f = comp A B C k g + := + ind-path (A → B) f (\ g' p' → comp A B C h f = comp A B C k g') + ( ind-path (B → C) h (\ k' q' → comp A B C h f = comp A B C k' f) + ( refl) + ( k) + ( q)) + ( g) + ( p) +``` + ## Naturality ```rzk title="The naturality square associated to a homotopy and a path" diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md index 52291225..2469d979 100644 --- a/src/hott/03-equivalences.rzk.md +++ b/src/hott/03-equivalences.rzk.md @@ -791,6 +791,28 @@ identifications. This defines `#!rzk eq-htpy` to be the retraction to ( f g : (x : X) → A x) : ((x : X) → f x = g x) → (f = g) := first (first (funext X A f g)) + +#def left-cancel-is-equiv uses (funext) + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + : (comp A B A (π₁ (π₁ is-equiv-f)) f) = (identity A) + := + eq-htpy A (\ x' → A) + ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( identity A) + ( π₂ (π₁ is-equiv-f)) + +#def right-cancel-is-equiv uses (funext) + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + : (comp B A B f (π₁ (π₂ is-equiv-f))) = (identity B) + := + eq-htpy B (\ x' → B) + ( comp B A B f (π₁ (π₂ is-equiv-f))) + ( identity B) + ( π₂ (π₂ is-equiv-f)) ``` Using function extensionality, a fiberwise equivalence defines an equivalence of diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index 02747f4a..b93857ff 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -331,6 +331,25 @@ For each of these we provide a corresponding functorial instance ( ( \ g → (\ t → (first (g t)) , \ t → second (g t))) , ( ( \ (f , h) t → (f t , h t) , \ _ → refl) , ( \ (f , h) t → (f t , h t) , \ _ → refl))) + +#def inv-equiv-axiom-choice + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( X : ψ → U) + ( Y : (t : ψ) → (x : X t) → U) + ( a : (t : ϕ) → X t) + ( b : (t : ϕ) → Y t (a t)) + : Equiv + ( Σ ( f : ((t : ψ) → X t [ϕ t ↦ a t])) + , ( (t : ψ) → Y t (f t) [ϕ t ↦ b t])) + ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)]) + := + inv-equiv + ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)]) + ( Σ ( f : ((t : ψ) → X t [ϕ t ↦ a t])) + , ( (t : ψ) → Y t (f t) [ϕ t ↦ b t])) + ( axiom-choice I ψ ϕ X Y a b) ``` ## Composites and unions of cofibrations diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 5075d86b..0ac99657 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -21,6 +21,7 @@ extension extensionality: ```rzk #assume funext : FunExt #assume extext : ExtExt +#assume weakextext : WeakExtExt ``` ## Functors @@ -103,6 +104,59 @@ Preservation of composition requires the Segal hypothesis. ( witness-comp-is-segal A is-segal-A x y z f g)) ``` +The action on morphisms commute with transport. + +```rzk + +#def ap-hom-naturality + ( A B C : U) + ( f g : A → B) + ( h k : B → C) + ( p : f = g) + ( q : h = k) + ( x y : A) + : comp (hom B (f x) (f y)) (hom B (g x) (g y)) (hom C (k (g x)) (k (g y))) + ( ap-hom B C k (g x) (g y)) + ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g p) + = + comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g x)) (k (g y))) + ( transport (A → C) (\ f' → hom C (f' x) (f' y)) + ( comp A B C h f) + ( comp A B C k g) + ( comp-homotopic-maps A B C f g h k p q)) + ( ap-hom B C h (f x) (f y)) + := + ind-path (A → B) f + ( \ g' p' → + comp (hom B (f x) (f y)) (hom B (g' x) (g' y)) (hom C (k (g' x)) (k (g' y))) + ( ap-hom B C k (g' x) (g' y)) + ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g' p') + = + comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g' x)) (k (g' y))) + ( transport (A → C) (\ f' → hom C (f' x) (f' y)) + ( comp A B C h f) + ( comp A B C k g') + ( comp-homotopic-maps A B C f g' h k p' q)) + ( ap-hom B C h (f x) (f y))) + ( ind-path (B → C) h + ( \ k' q' → + comp (hom B (f x) (f y)) (hom B (f x) (f y)) (hom C (k' (f x)) (k' (f y))) + ( ap-hom B C k' (f x) (f y)) + ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f f refl) + = + comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k' (f x)) (k' (f y))) + ( transport (A → C) (\ f' → hom C (f' x) (f' y)) + ( comp A B C h f) + ( comp A B C k' f) + ( comp-homotopic-maps A B C f f h k' refl q')) + ( ap-hom B C h (f x) (f y))) + ( refl) + ( k) + ( q)) + ( g) + ( p) +``` + ## Natural transformations Given two simplicial maps `#!rzk f g : (x : A) → B x` , a **natural @@ -416,3 +470,290 @@ the "Gray interchanger" built from two commutative triangles. ( horizontal-comp-nat-trans A B C f g f' g' η η') := \ (t, s) a → η' t (η s a) ``` + +## Equivalences are fully faithful + +```rzk + +#def postcomp-Π-ext + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( a : (t : ϕ) → A t) + ( f : (t : ψ) → (A t → B t)) + : ((t : ψ) → A t [ϕ t ↦ a t]) → ((t : ψ) → B t [ϕ t ↦ f t (a t)]) + := ( \ α t → f t (α t)) + +#def fiber-postcomp-Π-ext -- already defined as relative extension type in 03-extension-types + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( a : (t : ϕ) → A t) + ( f : (t : ψ) → (A t → B t)) + ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) + : U + := + fib + ( (t : ψ) → A t [ϕ t ↦ a t]) + ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( postcomp-Π-ext I ψ ϕ A B a f) + ( β) + +#def fiber-family-ext + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( a : (t : ϕ) → A t) + ( f : (t : ψ) → (A t → B t)) + ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) + : U + := + (t : ψ) → fib (A t) (B t) (f t) (β t) [ϕ t ↦ (a t, refl)] + +#def is-contr-fiber-family-ext-contr-fib + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( a : (t : ϕ) → A t) + ( f : (t : ψ) → (A t → B t)) + ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) + : is-contr (fiber-family-ext I ψ ϕ A B a f β) + := + weakextext I ψ ϕ + ( \ t → fib (A t) (B t) (f t) (β t)) + ( \ t → is-contr-map-is-equiv (A t) (B t) (f t) (family-equiv-f t) (β t)) + ( \ t → (a t, refl)) + + + +#def equiv-fiber-postcomp-Π-ext-fiber-family-ext + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( a : (t : ϕ) → A t) + ( f : (t : ψ) → (A t → B t)) + ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) + : Equiv + ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) + ( fiber-family-ext I ψ ϕ A B a f β) + := + equiv-comp + ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) + ( relative-extension-type I ψ ϕ A B f a β) + ( fiber-family-ext I ψ ϕ A B a f β) + ( equiv-relative-extension-type-fib extext I ψ ϕ A B f a β) + ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = β t) a (\ t → refl)) + + +#def fiber-ap-hom + ( A B : U) + ( x y : A) + ( f : A → B) + ( β : hom B (f x) (f y)) + : U + := + fib + ( hom A x y) + ( hom B (f x) (f y)) + ( ap-hom A B f x y) + ( β) + +-- --useless +-- #def fiber-ap-hom-postcomp +-- ( A B : U) +-- ( x y : A) +-- ( f : A → B) +-- ( β : hom B (f x) (f y)) +-- : U +-- := +-- fiber-postcomp-Π-ext 2 Δ¹ ∂Δ¹ (\ t → A) (\ t → B) +-- ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) +-- ( \ t → f) +-- ( β) + +-- --useless +-- #def equiv-fib-ap-hom-fib-post-comp-hom +-- ( A B : U) +-- ( x y : A) +-- ( f : A → B) +-- ( β : hom B (f x) (f y)) +-- : Equiv +-- ( fiber-ap-hom A B x y f β) +-- ( fiber-ap-hom-postcomp A B x y f β) +-- := ( \ x' → x', +-- ( (\ x' → x', (\ x' → refl)), +-- (\ x' → x', (\ x' → refl)))) + + +#def is-contr-fiber-ap-hom-is-equiv uses (weakextext extext) + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + ( x y : A) + ( β : hom B (f x) (f y)) + : is-contr (fiber-ap-hom A B x y f β) + := + is-contr-equiv-is-contr' + ( fiber-ap-hom A B x y f β) + ( fiber-family-ext 2 Δ¹ ∂Δ¹ (\ t → A) (\ t → B) + ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) + ( \ t → f) + ( β)) + ( equiv-fiber-postcomp-Π-ext-fiber-family-ext 2 Δ¹ ∂Δ¹ (\ t → A) (\ t → B) + ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) + ( \ t → f) + ( β)) + ( is-contr-fiber-family-ext-contr-fib 2 Δ¹ ∂Δ¹ (\ t → A) (\ t → B) + ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) + ( \ t → f) + ( β) + ( \t → is-equiv-f)) + + +#def is-equiv-ap-hom-is-equiv uses (weakextext extext) + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + ( x y : A) + : is-equiv (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) + := + is-equiv-is-contr-map (hom A x y) (hom B (f x) (f y)) + (ap-hom A B f x y) + ( \ β → is-contr-fiber-ap-hom-is-equiv A B f is-equiv-f x y β) + + +-- #def coherence-hae-is-equiv +-- ( A B : U) +-- ( f : A → B) +-- ( is-equiv-f : is-equiv A B f) +-- : (\ (x' : A) → ( π₂ (π₂ is-equiv-f)) (f x')) +-- = +-- ap A B +-- ( comp A B A (π₁ (π₁ is-equiv-f)) f) +-- ( identity A) +-- ( \ x' → comp A A B f x') +-- ( left-cancel-is-equiv A B f is-equiv-f) +-- := +-- eq-htpy A (\ x' → triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f x') +-- ( comp A B ((y' : B) → (comp B A B f (π₁ (π₁ is-equiv-f)) y') = y') +-- ( π₂ (π₂ is-equiv-f)) +-- ( f)) +-- ( ap A B +-- (comp A B A (π₁ (π₁ is-equiv-f)) f) +-- (identity A) +-- ((π₂ (π₁ is-equiv-f)))) +-- ( coherence-is-half-adjoint-equiv A B f +-- ( is-half-adjoint-equiv-is-equiv A B f is-equiv-f)) + + + +#def inv-ap-hom-equiv uses (funext) + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + ( x y : A) + : (hom B (f x) (f y)) → (hom A x y) + := + comp + ( hom B (f x) (f y)) + ( hom A ((π₁ (π₁ is-equiv-f)) (f x)) ((π₁ (π₁ is-equiv-f))(f y))) + ( hom A x y) + ( transport (A → A) (\ g' → (hom A (g' x) (g' y))) + ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( identity A) + ( left-cancel-is-equiv funext A B f is-equiv-f)) + ( ap-hom B A (π₁ (π₁ is-equiv-f)) (f x) (f y)) + + +#def has-retraction-ap-hom-equiv uses (funext) + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + ( x y : A) + : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) + := + ( inv-ap-hom-equiv A B f is-equiv-f x y + , \ α → + apd (A → A) (\ g' → (hom A (g' x) (g' y))) + ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( identity A) + ( \ g' → ap-hom A A g' x y α) + ( left-cancel-is-equiv funext A B f is-equiv-f)) + + + +-- #def has-section-ap-hom-equiv uses (funext) +-- ( A B : U) +-- ( f : A → B) +-- ( is-equiv-f : is-equiv A B f) +-- ( x y : A) +-- : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) +-- := +-- ( inv-ap-hom-equiv A B f is-equiv-f x y +-- , \ α → +-- concat (hom B (f x) (f y)) +-- ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) +-- ( ap-hom A B f x y) +-- ( inv-ap-hom-equiv A B f is-equiv-f x y) +-- ( α)) +-- ( transport (A → A) (\ g' → hom A (g x) (g y)) +-- ( triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f) +-- ( f) +-- ( ap A B +-- ( comp A B A (π₁ (π₁ is-equiv-f)) f) +-- ( identity A) +-- ( f) +-- ( left-cancel-is-equiv A B f is-equiv-f)) +-- ( α)) +-- ( α) +-- ( ap-hom-naturality A A A B -- path 1 +-- ( comp A B A (π₁ (π₁ is-equiv-f)) f) +-- ( identity A) +-- ( f) +-- ( f) +-- ( left-cancel-is-equiv A B f is-equiv-f) +-- ( refl) +-- ( x) +-- ( y)) + +-- ) + + + -- triple-concat (hom B (f x) (f y)) + -- ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) + -- ( ap-hom A B f x y) + -- ( inv-ap-hom-equiv A B f is-equiv-f x y) + -- ( α)) + -- ( transport (A → A) (\ g' → hom A (g x) (g y)) + -- ( triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f) + -- ( f) + -- ( ap A B + -- ( comp A B A (π₁ (π₁ is-equiv-f)) f) + -- ( identity A) + -- ( f) + -- ( left-cancel-is-equiv A B f is-equiv-f)) + -- ( α)) + -- ( transport) + -- ( α) + + + + + + + + -- : ( α : hom A x y) → + -- ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) + -- ( ap-hom A B f x y) + -- ( inv-ap-hom-equiv A B f is-equiv-f x y) + -- ( α) + -- = α) + -- := + +``` diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index db1a366b..0a8b75bc 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -2220,403 +2220,7 @@ In particular, in discrete types identity types are discrete. ```rzk title="RS17, Corollary 8.20" --- -- useless --- #def map-inverse-is-equiv --- ( A B : U) --- ( f : A → B) --- ( is-equiv-f : is-equiv A B f) --- : B → A --- := --- π₁ (has-inverse-is-equiv A B f is-equiv-f) - --- -- inverse map of idtoarr but probably useless now --- #def inverse-hom-eq-id-type --- ( A : U) --- ( is-discrete-A : is-discrete A) --- ( x y : A) --- ( p q : x = y) --- : (hom (x = y) p q) → (p = q) --- := --- comp --- ( hom (x = y) p q) --- ( (hom-eq A x y p) = (hom-eq A x y q)) --- ( p = q) --- ( ap-cancel-has-retraction ( x = y) ( hom A x y) --- ( hom-eq A x y) --- ( π₁ (is-discrete-A x y)) --- ( p) --- ( q)) --- ( comp --- ( hom (x = y) p q) --- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y q)) --- ( (hom-eq A x y p) = (hom-eq A x y q)) --- ( map-inverse-is-equiv --- ( (hom-eq A x y p) = (hom-eq A x y q)) --- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y q)) --- ( hom-eq (hom A x y) (hom-eq A x y p) (hom-eq A x y q)) --- ( (is-discrete-hom-is-segal ( A) --- ( is-segal-is-discrete extext A is-discrete-A) --- ( x) --- ( y)) --- ( hom-eq A x y p) --- ( hom-eq A x y q))) --- ( ap-hom ( x = y) ( hom A x y) ( hom-eq A x y) ( p) ( q))) - --- #def p₁ --- ( A : U) --- ( is-discrete-A : is-discrete A) --- ( x y : A) --- ( p : x = y) --- : ( inverse-hom-eq-id-type A is-discrete-A x y p p) ( id-hom (x = y) p) --- = --- ( comp --- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) --- ( (hom-eq A x y p) = (hom-eq A x y p)) --- ( p = p) --- ( ap-cancel-has-retraction ( x = y) ( hom A x y) --- ( hom-eq A x y) --- ( π₁ (is-discrete-A x y)) --- ( p) --- ( p)) --- ( map-inverse-is-equiv --- ( (hom-eq A x y p) = (hom-eq A x y p)) --- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) --- ( hom-eq (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) --- ( (is-discrete-hom-is-segal ( A) --- ( is-segal-is-discrete extext A is-discrete-A) --- ( x) --- ( y)) --- ( hom-eq A x y p) --- ( hom-eq A x y p)))) ( id-hom (hom A x y) (hom-eq A x y p)) --- := --- ap --- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) --- ( p = p) --- ( ap-hom ( x = y) ( hom A x y) --- ( hom-eq A x y) --- ( p) ( p) --- ( id-hom ( x = y) p)) --- ( id-hom ( hom A x y) ( hom-eq A x y p)) --- ( comp --- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) --- ( (hom-eq A x y p) = (hom-eq A x y p)) --- ( p = p) --- ( ap-cancel-has-retraction ( x = y) ( hom A x y) --- ( hom-eq A x y) --- ( π₁ (is-discrete-A x y)) --- ( p) --- ( p)) --- ( map-inverse-is-equiv --- ( (hom-eq A x y p) = (hom-eq A x y p)) --- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) --- ( hom-eq ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) --- ( ( is-discrete-hom-is-segal ( A) --- ( is-segal-is-discrete extext A is-discrete-A) --- ( x) --- ( y)) --- ( hom-eq A x y p) --- ( hom-eq A x y p)))) --- ( functors-pres-id extext ( x = y) ( hom A x y) --- (hom-eq A x y) ( p)) - --- #def p₂ --- ( A : U) --- ( is-discrete-A : is-discrete A) --- ( x y : A) --- ( p : x = y) --- : ( comp --- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) --- ( (hom-eq A x y p) = (hom-eq A x y p)) --- ( p = p) --- ( ap-cancel-has-retraction ( x = y) ( hom A x y) --- ( hom-eq A x y) --- ( π₁ (is-discrete-A x y)) --- ( p) --- ( p)) --- ( map-inverse-is-equiv --- ( (hom-eq A x y p) = (hom-eq A x y p)) --- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) --- ( hom-eq (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) --- ( (is-discrete-hom-is-segal ( A) --- ( is-segal-is-discrete extext A is-discrete-A) --- ( x) --- ( y)) --- ( hom-eq A x y p) --- ( hom-eq A x y p)))) ( id-hom (hom A x y) (hom-eq A x y p)) --- = --- ( ( ap-cancel-has-retraction ( x = y) ( hom A x y) --- ( hom-eq A x y) --- ( π₁ (is-discrete-A x y)) --- ( p) --- ( p)) (refl_{hom-eq A x y p})) --- := --- ap --- ( (hom-eq A x y p) = (hom-eq A x y p)) --- ( p = p) --- ( (map-inverse-is-equiv --- ( (hom-eq A x y p) = (hom-eq A x y p)) --- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) --- ( hom-eq (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) --- ( (is-discrete-hom-is-segal ( A) --- ( is-segal-is-discrete extext A is-discrete-A) --- ( x) --- ( y)) --- ( hom-eq A x y p) --- ( hom-eq A x y p))) ( id-hom (hom A x y) (hom-eq A x y p))) --- ( refl_{hom-eq A x y p}) --- ( ap-cancel-has-retraction ( x = y) ( hom A x y) --- ( hom-eq A x y) --- ( π₁ (is-discrete-A x y)) --- ( p) --- ( p)) --- ( (π₂ --- (π₁ --- ( --- (is-discrete-hom-is-segal ( A) --- ( is-segal-is-discrete extext A is-discrete-A) --- ( x) --- ( y) --- ) --- (hom-eq A x y p) --- (hom-eq A x y p) --- ) --- ) --- ) --- (refl_{hom-eq A x y p}) --- ) - --- --inverse map of ap --- #def inv-ap-is-equiv --- ( A B : U) --- ( f : A → B) --- ( is-equiv-f : is-equiv A B f) --- ( x y : A) --- : (f x = f y) → (x = y) --- := --- \ p' → --- triple-concat A x --- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) x) --- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) y) --- ( y) --- ( rev A ((comp A B A (π₁ (π₁ is-equiv-f)) f) x) x --- ( (π₂ (π₁ is-equiv-f)) x)) --- ( ap B A (f x) (f y) (π₁ (π₁ is-equiv-f)) p') --- ( (π₂ (π₁ is-equiv-f)) y) - --- -- finished but can do better with ind-path --- #def has-retraction-ap-is-equiv --- ( A B : U) --- ( f : A → B) --- ( is-equiv-f : is-equiv A B f) --- ( x y : A) --- : has-retraction (x = y) ((f x) = (f y)) (ap A B x y f) --- := --- ( inv-ap-is-equiv A B f is-equiv-f x y, --- \ p' → --- triple-concat (x = y) --- ( inv-ap-is-equiv A B f is-equiv-f x y ( ap A B x y f p')) --- ( triple-concat A x --- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) x) --- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) y) --- ( y) --- ( rev A ((comp A B A (π₁ (π₁ is-equiv-f)) f) x) x --- ( (π₂ (π₁ is-equiv-f)) x)) --- ( ap A A x y (comp A B A (π₁ (π₁ is-equiv-f)) f) p') --- ( (π₂ (π₁ is-equiv-f)) y)) --- ( ap A A x y (identity A) p') --- ( p') --- ( ap --- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) x = (comp A B A (π₁ (π₁ is-equiv-f)) f) y) --- ( x = y) --- ( ap B A (f x) (f y) (π₁ (π₁ is-equiv-f)) (ap A B x y f p')) --- ( ap A A x y (comp A B A (π₁ (π₁ is-equiv-f)) f) p') --- ( \ q' → --- triple-concat A x --- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) x) --- ( (comp A B A (π₁ (π₁ is-equiv-f)) f) y) --- ( y) --- ( rev A ((comp A B A (π₁ (π₁ is-equiv-f)) f) x) x --- ( (π₂ (π₁ is-equiv-f)) x)) --- ( q') --- ( (π₂ (π₁ is-equiv-f)) y)) --- ( rev-ap-comp A B A x y f (π₁ (π₁ is-equiv-f)) p')) -- ap_{conj}(rev-ap-comp --- ( triple-concat-nat-htpy A A --- ( comp A B A (π₁ (π₁ is-equiv-f)) f) --- ( identity A) --- ( π₂ (π₁ is-equiv-f)) --- ( x) --- ( y) --- ( p')) --- ( ap-id A x y p')) - - --- -- #def has-section-ap-is-equiv --- -- ( A B : U) --- -- ( f : A → B) --- -- ( is-equiv-f : is-equiv A B f) --- -- ( x y : A) --- -- : has-section (x = y) ((f x) = (f y)) (ap A B x y f) --- -- := TODO but horrible path algerba - - --- -- #def η-ap --- -- ( A B : U) --- -- ( f : A → B) --- -- ( is-equiv-f : is-equiv A B f) --- -- ( x y : A) --- -- : is-equiv (x = y) ((f x) = (f y)) (ap A B x y f) --- -- := --- -- ( (((second (first is-equiv-f)) x) . --- -- ap --- -- () --- -- () --- -- () --- -- (map-inverse-is-equiv A B f is-equiv-f) . --- -- rev ((second (first is-equiv-f)) y), --- -- has-retract), --- -- (map-inverse-is-equiv A B f is-equiv-f, --- -- has-section)) - - - - --- -- to finish, perhaps --- #def has-retraction-inverse-hom-eq-id-type --- ( A : U) --- ( is-discrete-A : is-discrete A) --- ( x y : A) --- ( p q : x = y) --- : has-retraction (p = q) (hom (x = y) p q) (hom-eq (x = y) p q) --- := --- ( inverse-hom-eq-id-type A is-discrete-A x y p q, --- ( \ α → --- ind-path ( x = y) ( p) --- ( \ q' α' → --- comp ( p = q') ( hom (x = y) p q') ( p = q') --- ( inverse-hom-eq-id-type A is-discrete-A x y p q') --- ( hom-eq (x = y) p q') --- ( α') --- = α') --- ( ap --- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) --- ( p = p) --- ( ap-hom ( x = y) ( hom A x y) --- ( hom-eq A x y) --- ( p) ( p) --- ( id-hom ( x = y) p)) --- ( id-hom ( hom A x y) ( hom-eq A x y p)) --- ( comp --- ( hom ( hom A x y) ( hom-eq A x y p) ( hom-eq A x y p)) --- ( (hom-eq A x y p) = (hom-eq A x y p)) --- ( p = p) --- ( ap-cancel-has-retraction ( x = y) ( hom A x y) --- ( hom-eq A x y) --- ( first (is-discrete-A x y)) --- ( p) --- ( p)) --- ( map-inverse-is-equiv --- ( (hom-eq A x y p) = (hom-eq A x y p)) --- ( hom (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) --- ( hom-eq (hom A x y) (hom-eq A x y p) (hom-eq A x y p)) --- ( (is-discrete-hom-is-segal ( A) --- ( is-segal-is-discrete extext A is-discrete-A) --- ( x) --- ( y)) --- ( hom-eq A x y p) --- ( hom-eq A x y p)))) --- (functors-pres-id extext ( x = y) ( hom A x y) --- ( hom-eq A x y) ( p))) -- concatenate p₁ p₂ and retraction ap φ is-equiv-φ --- ( q) --- ( α) --- ) --- ) - --- #def has-section-inverse-hom-eq-id-type --- ( A : U) --- ( is-discrete-A : is-discrete A) --- ( x y : A) --- ( p q : x = y) --- : has-section (p = q) (hom (x = y) p q) (hom-eq (x = y) p q) --- := --- ( inverse-hom-eq-id-type A is-discrete-A x y p q, --- ( -- to fill --- )) - --- -- composition ap_{hom-eq}^{-1} o hom-eq^{-1} o ap-hom hom-eq with hom-eq is section and retraction --- #def is-discrete-id-type-is-discrete --- ( A : U) --- ( is-discrete-A : is-discrete A) --- ( x y : A) --- : is-discrete (x = y) --- := --- \ p q → --- is-equiv-has-inverse ( p = q) ( hom (x = y) p q) --- ( hom-eq (x = y) p q) --- ( inverse-hom-eq-id-type A is-discrete-A x y p q), --- ( second has-retraction-inverse-hom-eq-id-type, --- second has-section-inverse-hom-eq-id-type) -``` - -```rzk title="RS17, Corollary 8.19" - --- #def precomp --- ( A B : U) --- ( P : B → U) --- ( f : A → B) --- : ((y : B) → P y) → ((x : A) → P (f x)) --- := --- \ α → (\ x → α (f x)) - --- #def precomp-with-inv --- ( A B : U) --- ( P : B → U) --- ( f : A → B) --- ( is-equiv-f : is-equiv A B f) --- : ((x : A) → P (f x)) → ((y : B) → P y) --- := --- \ β → --- transport ( B → B) --- ( \ f' → ((y : B) → P (f' y))) --- ( comp B A B f (π₁ (π₂ is-equiv-f))) --- ( identity B) --- ( eq-htpy funext B (\ b' → B) --- ( comp B A B f (π₁ (π₂ is-equiv-f))) --- ( identity B) --- (π₂ (π₂ is-equiv-f))) --- ( precomp B A ( \ x' → P (f x')) --- ( π₁ (π₂ is-equiv-f)) --- ( β)) - --- #def is-equiv-precomp-equiv --- ( A B : U) --- ( P : B → U) --- ( f : A → B) --- ( is-equiv-f : is-equiv A B f) --- : Equiv ((y : B) → P y) ((x : A) → P (f x)) --- := --- ( precomp A B P f --- , is-equiv-is-contr-map ((y : B) → P y) ((x : A) → P (f x)) (precomp A B P f) --- ( \ β → --- is-contr-equiv-is-contr' --- ( fib --- ( (y : B) → P y) --- ( (x : A) → P (f x)) --- ( precomp A B P f) --- ( β)) --- ( Σ (α : ((y : B) → P y)) , --- ( α = precomp-with-inv A B P f is-equiv-f β)) --- ( total-equiv-family-of-equiv --- ( (y : B) → P y) --- ( \ α → (precomp A B P f α) = β) --- ( \ α → α = (precomp-with-inv A B P f is-equiv-f β))) --- -- TODO: show that (α ∘ f = β) ≅ (α = tr (β ∘ f⁻¹) --- ( is-contr-endpoint-based-paths --- ( (y : B) → P y) --- ( precomp-with-inv A B P f is-equiv-f β)))) - - - -#def hom-eq-ap-ap-hom-commute +#def hom-eq-naturality ( A B : U) ( f : A → B) ( x y : A) @@ -2647,230 +2251,6 @@ In particular, in discrete types identity types are discrete. ( y) ( p) --- useless: hold judgmentaly --- #def ap-hom-comp --- ( A B C : U) --- ( f : A → B) --- ( g : B → C) --- ( x y : A) --- : comp (hom A x y) (hom B (f x) (f y)) (hom C (g (f x)) (g (f y))) --- ( ap-hom B C g (f x) (f y)) --- ( ap-hom A B f x y) --- = --- ap-hom A C (comp A B C g f) x y --- := refl - -#def left-cancel-is-equiv - ( A B : U) - ( f : A → B) - ( is-equiv-f : is-equiv A B f) - : (comp A B A (π₁ (π₁ is-equiv-f)) f) = (identity A) - := - eq-htpy funext A (\ x' → A) - ( comp A B A (π₁ (π₁ is-equiv-f)) f) - ( identity A) - ( π₂ (π₁ is-equiv-f)) - -#def right-cancel-is-equiv - ( A B : U) - ( f : A → B) - ( is-equiv-f : is-equiv A B f) - : (comp B A B f (π₁ (π₂ is-equiv-f))) = (identity B) - := - eq-htpy funext B (\ x' → B) - ( comp B A B f (π₁ (π₂ is-equiv-f))) - ( identity B) - ( π₂ (π₂ is-equiv-f)) - -#def coherence-hae-is-equiv - ( A B : U) - ( f : A → B) - ( is-equiv-f : is-equiv A B f) - : comp A B ((y' : B) → (comp B A B f (π₁ (π₁ is-equiv-f)) y') = y') - ( π₂ (π₂ is-equiv-f)) - ( f) - = - ap A B - (comp A B A (π₁ (π₁ is-equiv-f)) f) - (identity A) - ((π₂ (π₁ is-equiv-f))) - := - eq-htpy A (\ x' → triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f x') - ( comp A B ((y' : B) → (comp B A B f (π₁ (π₁ is-equiv-f)) y') = y') - ( π₂ (π₂ is-equiv-f)) - ( f)) - ( ap A B - (comp A B A (π₁ (π₁ is-equiv-f)) f) - (identity A) - ((π₂ (π₁ is-equiv-f)))) - ( coherence-is-half-adjoint-equiv A B f - ( is-half-adjoint-equiv-is-equiv A B f is-equiv-f)) - - -#def comp-homotopic-maps - ( A B C : U) - ( f g : A → B) - ( h k : B → C) - ( p : f = g) - ( q : h = k) - : comp A B C h f = comp A B C k g - := - ind-path (A → B) f (\ g' p' → comp A B C h f = comp A B C k g') - ( ind-path (B → C) h (\ k' q' → comp A B C h f = comp A B C k' f) - ( refl) - ( k) - ( q)) - ( g) - ( p) - -#def inv-ap-hom-equiv uses (funext) - ( A B : U) - ( f : A → B) - ( is-equiv-f : is-equiv A B f) - ( x y : A) - : (hom B (f x) (f y)) → (hom A x y) - := - comp - ( hom B (f x) (f y)) - ( hom A ((π₁ (π₁ is-equiv-f)) (f x)) ((π₁ (π₁ is-equiv-f))(f y))) - ( hom A x y) - ( transport (A → A) (\ g' → (hom A (g' x) (g' y))) - ( comp A B A (π₁ (π₁ is-equiv-f)) f) - ( identity A) - ( left-cancel-is-equiv A B f is-equiv-f)) - ( ap-hom B A (π₁ (π₁ is-equiv-f)) (f x) (f y)) - - -#def has-retraction-ap-hom-equiv uses (funext) - ( A B : U) - ( f : A → B) - ( is-equiv-f : is-equiv A B f) - ( x y : A) - : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) - := - ( inv-ap-hom-equiv A B f is-equiv-f x y - , \ α → - apd (A → A) (\ g' → (hom A (g' x) (g' y))) - ( comp A B A (π₁ (π₁ is-equiv-f)) f) - ( identity A) - ( \ g' → ap-hom A A g' x y α) - ( left-cancel-is-equiv A B f is-equiv-f)) - -#def ap-hom-naturality - ( A B C : U) - ( f g : A → B) - ( h k : B → C) - ( p : f = g) - ( q : h = k) - ( x y : A) - : comp (hom B (f x) (f y)) (hom B (g x) (g y)) (hom C (k (g x)) (k (g y))) - ( ap-hom B C k (g x) (g y)) - ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g p) - = - comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g x)) (k (g y))) - ( transport (A → C) (\ f' → hom C (f' x) (f' y)) - ( comp A B C h f) - ( comp A B C k g) - ( comp-homotopic-maps A B C f g h k p q)) - ( ap-hom B C h (f x) (f y)) - := - ind-path (A → B) f - ( \ g' p' → - comp (hom B (f x) (f y)) (hom B (g' x) (g' y)) (hom C (k (g' x)) (k (g' y))) - ( ap-hom B C k (g' x) (g' y)) - ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g' p') - = - comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g' x)) (k (g' y))) - ( transport (A → C) (\ f' → hom C (f' x) (f' y)) - ( comp A B C h f) - ( comp A B C k g') - ( comp-homotopic-maps A B C f g' h k p' q)) - ( ap-hom B C h (f x) (f y))) - ( ind-path (B → C) h - ( \ k' q' → - comp (hom B (f x) (f y)) (hom B (f x) (f y)) (hom C (k' (f x)) (k' (f y))) - ( ap-hom B C k' (f x) (f y)) - ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f f refl) - = - comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k' (f x)) (k' (f y))) - ( transport (A → C) (\ f' → hom C (f' x) (f' y)) - ( comp A B C h f) - ( comp A B C k' f) - ( comp-homotopic-maps A B C f f h k' refl q')) - ( ap-hom B C h (f x) (f y))) - ( refl) - ( k) - ( q)) - ( g) - ( p) - -#def has-section-ap-hom-equiv uses (funext) - ( A B : U) - ( f : A → B) - ( is-equiv-f : is-equiv A B f) - ( x y : A) - : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) - := - ( inv-ap-hom-equiv A B f is-equiv-f x y - , \ α → - concat (hom B (f x) (f y)) - ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) - ( ap-hom A B f x y) - ( inv-ap-hom-equiv A B f is-equiv-f x y) - ( α)) - ( transport (A → A) (\ g' → hom A (g x) (g y)) - ( triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f) - ( f) - ( ap A B - ( comp A B A (π₁ (π₁ is-equiv-f)) f) - ( identity A) - ( f) - ( left-cancel-is-equiv A B f is-equiv-f)) - ( α)) - ( α) - ( ap-hom-naturality A A A B -- path 1 - ( comp A B A (π₁ (π₁ is-equiv-f)) f) - ( identity A) - ( f) - ( f) - ( left-cancel-is-equiv A B f is-equiv-f) - ( refl) - ( x) - ( y)) - - ) - - - -- triple-concat (hom B (f x) (f y)) - -- ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) - -- ( ap-hom A B f x y) - -- ( inv-ap-hom-equiv A B f is-equiv-f x y) - -- ( α)) - -- ( transport (A → A) (\ g' → hom A (g x) (g y)) - -- ( triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f) - -- ( f) - -- ( ap A B - -- ( comp A B A (π₁ (π₁ is-equiv-f)) f) - -- ( identity A) - -- ( f) - -- ( left-cancel-is-equiv A B f is-equiv-f)) - -- ( α)) - -- ( transport) - -- ( α) - - - - - - - - -- : ( α : hom A x y) → - -- ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) - -- ( ap-hom A B f x y) - -- ( inv-ap-hom-equiv A B f is-equiv-f x y) - -- ( α) - -- = α) - -- := #def equiv-preserve-discretness uses (extext funext) ( A B : U) @@ -2882,7 +2262,7 @@ In particular, in discrete types identity types are discrete. is-equiv-right-cancel (x = y) (hom A x y) (hom B (f x) (f y)) ( hom-eq A x y) ( ap-hom A B f x y) - ( has-retraction-ap-hom-equiv A B f is-equiv-f x y) + ( has-retraction-ap-hom-equiv funext A B f is-equiv-f x y) ( is-equiv-homotopy (x = y) (hom B (f x) (f y)) ( comp (x = y) (hom A x y) (hom B (f x) (f y)) ( ap-hom A B f x y) @@ -2890,7 +2270,7 @@ In particular, in discrete types identity types are discrete. ( comp (x = y) ((f x) = (f y)) (hom B (f x) (f y)) ( hom-eq B (f x) (f y)) ( ap A B x y f)) - ( hom-eq-ap-ap-hom-commute A B f x y) + ( hom-eq-naturality A B f x y) ( is-equiv-comp (x = y) ((f x) = (f y)) (hom B (f x) (f y)) ( ap A B x y f) ( is-emb-is-equiv A B f is-equiv-f x y) From 01757db136f4c2134152459e6dad65def7a54522 Mon Sep 17 00:00:00 2001 From: StiephenPradal Date: Fri, 27 Oct 2023 13:47:16 +0100 Subject: [PATCH 03/12] Weakening assumption from equiv to retrqction for ap-hom --- .../06-2cat-of-segal-types.rzk.md | 158 +++--------------- src/simplicial-hott/08-covariant.rzk.md | 2 +- 2 files changed, 23 insertions(+), 137 deletions(-) diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 0ac99657..790573a4 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -473,6 +473,8 @@ the "Gray interchanger" built from two commutative triangles. ## Equivalences are fully faithful +-- Or: Equivalences induce equivalences of hom + ```rzk #def postcomp-Π-ext @@ -564,32 +566,6 @@ the "Gray interchanger" built from two commutative triangles. ( ap-hom A B f x y) ( β) --- --useless --- #def fiber-ap-hom-postcomp --- ( A B : U) --- ( x y : A) --- ( f : A → B) --- ( β : hom B (f x) (f y)) --- : U --- := --- fiber-postcomp-Π-ext 2 Δ¹ ∂Δ¹ (\ t → A) (\ t → B) --- ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) --- ( \ t → f) --- ( β) - --- --useless --- #def equiv-fib-ap-hom-fib-post-comp-hom --- ( A B : U) --- ( x y : A) --- ( f : A → B) --- ( β : hom B (f x) (f y)) --- : Equiv --- ( fiber-ap-hom A B x y f β) --- ( fiber-ap-hom-postcomp A B x y f β) --- := ( \ x' → x', --- ( (\ x' → x', (\ x' → refl)), --- (\ x' → x', (\ x' → refl)))) - #def is-contr-fiber-ap-hom-is-equiv uses (weakextext extext) ( A B : U) @@ -601,21 +577,26 @@ the "Gray interchanger" built from two commutative triangles. := is-contr-equiv-is-contr' ( fiber-ap-hom A B x y f β) - ( fiber-family-ext 2 Δ¹ ∂Δ¹ (\ t → A) (\ t → B) + ( fiber-family-ext 2 Δ¹ ∂Δ¹ + ( \ t → A) + ( \ t → B) ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) ( \ t → f) ( β)) - ( equiv-fiber-postcomp-Π-ext-fiber-family-ext 2 Δ¹ ∂Δ¹ (\ t → A) (\ t → B) + ( equiv-fiber-postcomp-Π-ext-fiber-family-ext 2 Δ¹ ∂Δ¹ + ( \ t → A) + ( \ t → B) ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) ( \ t → f) ( β)) - ( is-contr-fiber-family-ext-contr-fib 2 Δ¹ ∂Δ¹ (\ t → A) (\ t → B) + ( is-contr-fiber-family-ext-contr-fib 2 Δ¹ ∂Δ¹ + ( \ t → A) + ( \ t → B) ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) ( \ t → f) ( β) ( \t → is-equiv-f)) - #def is-equiv-ap-hom-is-equiv uses (weakextext extext) ( A B : U) ( f : A → B) @@ -628,132 +609,37 @@ the "Gray interchanger" built from two commutative triangles. ( \ β → is-contr-fiber-ap-hom-is-equiv A B f is-equiv-f x y β) --- #def coherence-hae-is-equiv --- ( A B : U) --- ( f : A → B) --- ( is-equiv-f : is-equiv A B f) --- : (\ (x' : A) → ( π₂ (π₂ is-equiv-f)) (f x')) --- = --- ap A B --- ( comp A B A (π₁ (π₁ is-equiv-f)) f) --- ( identity A) --- ( \ x' → comp A A B f x') --- ( left-cancel-is-equiv A B f is-equiv-f) --- := --- eq-htpy A (\ x' → triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f x') --- ( comp A B ((y' : B) → (comp B A B f (π₁ (π₁ is-equiv-f)) y') = y') --- ( π₂ (π₂ is-equiv-f)) --- ( f)) --- ( ap A B --- (comp A B A (π₁ (π₁ is-equiv-f)) f) --- (identity A) --- ((π₂ (π₁ is-equiv-f)))) --- ( coherence-is-half-adjoint-equiv A B f --- ( is-half-adjoint-equiv-is-equiv A B f is-equiv-f)) - - - -#def inv-ap-hom-equiv uses (funext) +#def retraction-ap-hom-retraction uses (funext) -- change this into retraction of ap-hom if f has one ( A B : U) ( f : A → B) - ( is-equiv-f : is-equiv A B f) + ( (r, ρ) : has-retraction A B f) ( x y : A) : (hom B (f x) (f y)) → (hom A x y) := comp ( hom B (f x) (f y)) - ( hom A ((π₁ (π₁ is-equiv-f)) (f x)) ((π₁ (π₁ is-equiv-f))(f y))) + ( hom A (r (f x)) (r (f y))) ( hom A x y) ( transport (A → A) (\ g' → (hom A (g' x) (g' y))) - ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( comp A B A r f) ( identity A) - ( left-cancel-is-equiv funext A B f is-equiv-f)) - ( ap-hom B A (π₁ (π₁ is-equiv-f)) (f x) (f y)) + ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) -- proof retraction here + ( ap-hom B A r (f x) (f y)) -#def has-retraction-ap-hom-equiv uses (funext) +#def has-retraction-ap-hom-retraction uses (funext) --change into proof that ap-hom has a retraction is f has one ( A B : U) ( f : A → B) - ( is-equiv-f : is-equiv A B f) + ( (r, ρ) : has-retraction A B f) ( x y : A) : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) := - ( inv-ap-hom-equiv A B f is-equiv-f x y + ( retraction-ap-hom-retraction A B f (r, ρ) x y , \ α → apd (A → A) (\ g' → (hom A (g' x) (g' y))) - ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( comp A B A r f) ( identity A) ( \ g' → ap-hom A A g' x y α) - ( left-cancel-is-equiv funext A B f is-equiv-f)) - - - --- #def has-section-ap-hom-equiv uses (funext) --- ( A B : U) --- ( f : A → B) --- ( is-equiv-f : is-equiv A B f) --- ( x y : A) --- : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) --- := --- ( inv-ap-hom-equiv A B f is-equiv-f x y --- , \ α → --- concat (hom B (f x) (f y)) --- ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) --- ( ap-hom A B f x y) --- ( inv-ap-hom-equiv A B f is-equiv-f x y) --- ( α)) --- ( transport (A → A) (\ g' → hom A (g x) (g y)) --- ( triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f) --- ( f) --- ( ap A B --- ( comp A B A (π₁ (π₁ is-equiv-f)) f) --- ( identity A) --- ( f) --- ( left-cancel-is-equiv A B f is-equiv-f)) --- ( α)) --- ( α) --- ( ap-hom-naturality A A A B -- path 1 --- ( comp A B A (π₁ (π₁ is-equiv-f)) f) --- ( identity A) --- ( f) --- ( f) --- ( left-cancel-is-equiv A B f is-equiv-f) --- ( refl) --- ( x) --- ( y)) - --- ) - - - -- triple-concat (hom B (f x) (f y)) - -- ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) - -- ( ap-hom A B f x y) - -- ( inv-ap-hom-equiv A B f is-equiv-f x y) - -- ( α)) - -- ( transport (A → A) (\ g' → hom A (g x) (g y)) - -- ( triple-comp A B A B f (π₁ (π₁ is-equiv-f)) f) - -- ( f) - -- ( ap A B - -- ( comp A B A (π₁ (π₁ is-equiv-f)) f) - -- ( identity A) - -- ( f) - -- ( left-cancel-is-equiv A B f is-equiv-f)) - -- ( α)) - -- ( transport) - -- ( α) - - - - - - - - -- : ( α : hom A x y) → - -- ( comp (hom B (f x) (f y)) (hom A x y) (hom B (f x) (f y)) - -- ( ap-hom A B f x y) - -- ( inv-ap-hom-equiv A B f is-equiv-f x y) - -- ( α) - -- = α) - -- := + ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) -- proof retraction here ``` diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 0a8b75bc..48b7da51 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -2262,7 +2262,7 @@ In particular, in discrete types identity types are discrete. is-equiv-right-cancel (x = y) (hom A x y) (hom B (f x) (f y)) ( hom-eq A x y) ( ap-hom A B f x y) - ( has-retraction-ap-hom-equiv funext A B f is-equiv-f x y) + ( has-retraction-ap-hom-retraction funext A B f (π₁ is-equiv-f) x y) ( is-equiv-homotopy (x = y) (hom B (f x) (f y)) ( comp (x = y) (hom A x y) (hom B (f x) (f y)) ( ap-hom A B f x y) From efcb1e079af8becfe9453d2a3532f11ce1dfb746 Mon Sep 17 00:00:00 2001 From: StiephenPradal Date: Fri, 27 Oct 2023 15:27:11 +0100 Subject: [PATCH 04/12] Cleaning up + Adding comments --- .../06-2cat-of-segal-types.rzk.md | 137 +++++++++++------- src/simplicial-hott/08-covariant.rzk.md | 12 +- 2 files changed, 92 insertions(+), 57 deletions(-) diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 72446c12..b07c7ace 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -10,10 +10,10 @@ This is a literate `rzk` file: ## Prerequisites -- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and - their subshapes. -- `04-extension-types.rzk.md` — We use extension extensionality. -- `05-segal-types.rzk.md` - We use the notion of hom types. +- `3-simplicial-type-theory.md` — We rely on definitions of simplicies and their + subshapes. +- `4-extension-types.md` — We use extension extensionality. +- `5-segal-types.md` - We use the notion of hom types. Some of the definitions in this file rely on function extensionality and extension extensionality: @@ -104,10 +104,9 @@ Preservation of composition requires the Segal hypothesis. ( witness-comp-is-segal A is-segal-A x y z f g)) ``` -The action on morphisms commute with transport. +The action on morphisms commutes with transport. ```rzk - #def ap-hom-naturality ( A B C : U) ( f g : A → B) @@ -475,8 +474,10 @@ the "Gray interchanger" built from two commutative triangles. -- Or: Equivalences induce equivalences of hom -```rzk +The fiber of postcomposition by a map $f: \prod_{t : I|\psi} A (t) \to B (t)$ is +equivalent to the family of fibers of $f\_t$. +```rzk #def postcomp-Π-ext ( I : CUBE) ( ψ : I → TOPE) @@ -515,6 +516,30 @@ the "Gray interchanger" built from two commutative triangles. := (t : ψ) → fib (A t) (B t) (f t) (β t) [ϕ t ↦ (a t, refl)] +#def equiv-fiber-postcomp-Π-ext-fiber-family-ext + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( a : (t : ϕ) → A t) + ( f : (t : ψ) → (A t → B t)) + ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) + : Equiv + ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) + ( fiber-family-ext I ψ ϕ A B a f β) + := + equiv-comp + ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) + ( relative-extension-type I ψ ϕ A B f a β) + ( fiber-family-ext I ψ ϕ A B a f β) + ( equiv-relative-extension-type-fib extext I ψ ϕ A B f a β) + ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = β t) a (\ t → refl)) +``` + +In particular, if $f: \prod_{t : I|\psi} A (t) \to B (t)$ is a family of +equivalence then the fibers of postcomposition by f are contractible. + +```rzk #def is-contr-fiber-family-ext-contr-fib ( I : CUBE) ( ψ : I → TOPE) @@ -531,9 +556,7 @@ the "Gray interchanger" built from two commutative triangles. ( \ t → is-contr-map-is-equiv (A t) (B t) (f t) (family-equiv-f t) (β t)) ( \ t → (a t, refl)) - - -#def equiv-fiber-postcomp-Π-ext-fiber-family-ext +#def is-contr-fiber-postcomp-Π-ext-is-equiv-fam uses (weakextext extext) ( I : CUBE) ( ψ : I → TOPE) ( ϕ : ψ → TOPE) @@ -541,18 +564,57 @@ the "Gray interchanger" built from two commutative triangles. ( a : (t : ϕ) → A t) ( f : (t : ψ) → (A t → B t)) ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) - : Equiv - ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) - ( fiber-family-ext I ψ ϕ A B a f β) + ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) + : is-contr (fiber-postcomp-Π-ext I ψ ϕ A B a f β) := - equiv-comp + is-contr-equiv-is-contr' ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) - ( relative-extension-type I ψ ϕ A B f a β) ( fiber-family-ext I ψ ϕ A B a f β) - ( equiv-relative-extension-type-fib extext I ψ ϕ A B f a β) - ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = β t) a (\ t → refl)) + ( equiv-fiber-postcomp-Π-ext-fiber-family-ext I ψ ϕ A B a f β) + ( is-contr-fiber-family-ext-contr-fib I ψ ϕ A B a f β family-equiv-f) +#def is-equiv-postcomp-Π-ext-is-equiv uses (weakextext extext) + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( a : (t : ϕ) → A t) + ( f : (t : ψ) → (A t → B t)) + ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) + : is-equiv + ( (t : ψ) → A t [ϕ t ↦ a t]) + ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( postcomp-Π-ext I ψ ϕ A B a f) + := + is-equiv-is-contr-map + ( (t : ψ) → A t [ϕ t ↦ a t]) + ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( postcomp-Π-ext I ψ ϕ A B a f) + ( \ β → is-contr-fiber-postcomp-Π-ext-is-equiv-fam I ψ ϕ A B a f β family-equiv-f) +``` + +Using this result we can show that `#!rzk ap-hom` is an equivalence when f is an +equivalence. + +```rzk +#def is-equiv-ap-hom-is-equiv uses (weakextext extext) + ( A B : U) + ( f : A → B) + ( is-equiv-f : is-equiv A B f) + ( x y : A) + : is-equiv (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) + := + is-equiv-postcomp-Π-ext-is-equiv 2 Δ¹ ∂Δ¹ + ( \ t → A) + ( \ t → B) + ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) + ( \ t → f) + ( \ t → is-equiv-f) +``` + +More precicely: +```rzk #def fiber-ap-hom ( A B : U) ( x y : A) @@ -566,7 +628,6 @@ the "Gray interchanger" built from two commutative triangles. ( ap-hom A B f x y) ( β) - #def is-contr-fiber-ap-hom-is-equiv uses (weakextext extext) ( A B : U) ( f : A → B) @@ -575,41 +636,15 @@ the "Gray interchanger" built from two commutative triangles. ( β : hom B (f x) (f y)) : is-contr (fiber-ap-hom A B x y f β) := - is-contr-equiv-is-contr' - ( fiber-ap-hom A B x y f β) - ( fiber-family-ext 2 Δ¹ ∂Δ¹ - ( \ t → A) - ( \ t → B) - ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) - ( \ t → f) - ( β)) - ( equiv-fiber-postcomp-Π-ext-fiber-family-ext 2 Δ¹ ∂Δ¹ - ( \ t → A) - ( \ t → B) - ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) - ( \ t → f) - ( β)) - ( is-contr-fiber-family-ext-contr-fib 2 Δ¹ ∂Δ¹ + is-contr-fiber-postcomp-Π-ext-is-equiv-fam 2 Δ¹ ∂Δ¹ ( \ t → A) ( \ t → B) ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) ( \ t → f) ( β) - ( \t → is-equiv-f)) + ( \ t → is-equiv-f) -#def is-equiv-ap-hom-is-equiv uses (weakextext extext) - ( A B : U) - ( f : A → B) - ( is-equiv-f : is-equiv A B f) - ( x y : A) - : is-equiv (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) - := - is-equiv-is-contr-map (hom A x y) (hom B (f x) (f y)) - (ap-hom A B f x y) - ( \ β → is-contr-fiber-ap-hom-is-equiv A B f is-equiv-f x y β) - - -#def retraction-ap-hom-retraction uses (funext) -- change this into retraction of ap-hom if f has one +#def retraction-ap-hom-retraction uses (funext) ( A B : U) ( f : A → B) ( (r, ρ) : has-retraction A B f) @@ -623,11 +658,10 @@ the "Gray interchanger" built from two commutative triangles. ( transport (A → A) (\ g' → (hom A (g' x) (g' y))) ( comp A B A r f) ( identity A) - ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) -- proof retraction here + ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) ( ap-hom B A r (f x) (f y)) - -#def has-retraction-ap-hom-retraction uses (funext) --change into proof that ap-hom has a retraction is f has one +#def has-retraction-ap-hom-retraction uses (funext) ( A B : U) ( f : A → B) ( (r, ρ) : has-retraction A B f) @@ -640,6 +674,5 @@ the "Gray interchanger" built from two commutative triangles. ( comp A B A r f) ( identity A) ( \ g' → ap-hom A A g' x y α) - ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) -- proof retraction here - + ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) ``` diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 323a7ab1..c1cd81fe 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -2217,10 +2217,11 @@ are discrete. ( y) ``` -In particular, in discrete types identity types are discrete. - -```rzk title="RS17, Corollary 8.20" +In particular, in discrete types identity types are discrete. First we show that +equivalences preserve discretness. For that, we need that `#!rzk hom-eq` +commutes with actions on morphisms. +```rzk #def hom-eq-naturality ( A B : U) ( f : A → B) @@ -2252,7 +2253,6 @@ In particular, in discrete types identity types are discrete. ( y) ( p) - #def equiv-preserve-discretness uses (extext funext) ( A B : U) ( (f, is-equiv-f) : Equiv A B) @@ -2263,7 +2263,7 @@ In particular, in discrete types identity types are discrete. is-equiv-right-cancel (x = y) (hom A x y) (hom B (f x) (f y)) ( hom-eq A x y) ( ap-hom A B f x y) - ( has-retraction-ap-hom-retraction funext A B f (π₁ is-equiv-f) x y) + ( has-retraction-ap-hom-retraction funext A B f (π₁ is-equiv-f) x y) -- should I use retraction from contr map instead? ( is-equiv-homotopy (x = y) (hom B (f x) (f y)) ( comp (x = y) (hom A x y) (hom B (f x) (f y)) ( ap-hom A B f x y) @@ -2277,7 +2277,9 @@ In particular, in discrete types identity types are discrete. ( is-emb-is-equiv A B f is-equiv-f x y) ( hom-eq B (f x) (f y)) ( is-discrete-B (f x) (f y)))) +``` +```rzk title="RS17, Corollary 8.20" #def is-discrete-id-path-is-discrete uses (extext funext) ( A : U) ( is-discrete-A : is-discrete A) From bbcbbd0802228bb440451ad877d58c716fe2a114 Mon Sep 17 00:00:00 2001 From: StiephenPradal Date: Fri, 27 Oct 2023 15:31:32 +0100 Subject: [PATCH 05/12] Adding comments --- src/simplicial-hott/06-2cat-of-segal-types.rzk.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index b07c7ace..96d3c6e4 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -472,8 +472,6 @@ the "Gray interchanger" built from two commutative triangles. ## Equivalences are fully faithful --- Or: Equivalences induce equivalences of hom - The fiber of postcomposition by a map $f: \prod_{t : I|\psi} A (t) \to B (t)$ is equivalent to the family of fibers of $f\_t$. @@ -643,7 +641,11 @@ More precicely: ( \ t → f) ( β) ( \ t → is-equiv-f) +``` +We can also define a retraction of `#!rzk ap-hom` directly. + +``` #def retraction-ap-hom-retraction uses (funext) ( A B : U) ( f : A → B) From 63b2fca77d8f41e6ff53120c54f6b5648839ea18 Mon Sep 17 00:00:00 2001 From: StiephenPradal Date: Fri, 27 Oct 2023 15:33:16 +0100 Subject: [PATCH 06/12] Adding comments --- src/simplicial-hott/06-2cat-of-segal-types.rzk.md | 2 +- src/simplicial-hott/08-covariant.rzk.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 96d3c6e4..1b9f5f38 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -645,7 +645,7 @@ More precicely: We can also define a retraction of `#!rzk ap-hom` directly. -``` +```rzk #def retraction-ap-hom-retraction uses (funext) ( A B : U) ( f : A → B) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index c1cd81fe..3b7d6418 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -2263,7 +2263,7 @@ commutes with actions on morphisms. is-equiv-right-cancel (x = y) (hom A x y) (hom B (f x) (f y)) ( hom-eq A x y) ( ap-hom A B f x y) - ( has-retraction-ap-hom-retraction funext A B f (π₁ is-equiv-f) x y) -- should I use retraction from contr map instead? + ( has-retraction-ap-hom-retraction funext A B f (π₁ is-equiv-f) x y) ( is-equiv-homotopy (x = y) (hom B (f x) (f y)) ( comp (x = y) (hom A x y) (hom B (f x) (f y)) ( ap-hom A B f x y) From ff5a06616f057a3c1ef437fadfefd08c6955d45a Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Fri, 3 Nov 2023 20:22:16 -0400 Subject: [PATCH 07/12] condensed indentation --- .../06-2cat-of-segal-types.rzk.md | 199 +++++++++--------- 1 file changed, 100 insertions(+), 99 deletions(-) diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 0e542c07..88657544 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -138,46 +138,54 @@ The action on morphisms commutes with transport. ( p : f = g) ( q : h = k) ( x y : A) - : comp (hom B (f x) (f y)) (hom B (g x) (g y)) (hom C (k (g x)) (k (g y))) - ( ap-hom B C k (g x) (g y)) - ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g p) + : comp + ( hom B (f x) (f y)) + ( hom B (g x) (g y)) + ( hom C (k (g x)) (k (g y))) + ( ap-hom B C k (g x) (g y)) + ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g p) = - comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g x)) (k (g y))) + comp + ( hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g x)) (k (g y))) + ( transport (A → C) (\ f' → hom C (f' x) (f' y)) + ( comp A B C h f) + ( comp A B C k g) + ( comp-homotopic-maps A B C f g h k p q)) + ( ap-hom B C h (f x) (f y)) + := + ind-path (A → B) f + ( \ g' p' → + comp (hom B (f x) (f y)) (hom B (g' x) (g' y)) (hom C (k (g' x)) (k (g' y))) + ( ap-hom B C k (g' x) (g' y)) + ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g' p') + = + comp + ( hom B (f x) (f y))(hom C (h (f x)) (h (f y)))(hom C (k (g' x)) (k (g' y))) + ( transport (A → C) (\ f' → hom C (f' x) (f' y)) + ( comp A B C h f) + ( comp A B C k g') + ( comp-homotopic-maps A B C f g' h k p' q)) + ( ap-hom B C h (f x) (f y))) + ( ind-path (B → C) h + ( \ k' q' → + comp (hom B (f x) (f y)) (hom B (f x) (f y)) (hom C (k' (f x)) (k' (f y))) + ( ap-hom B C k' (f x) (f y)) + ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f f refl) + = + comp + ( hom B (f x) (f y)) + ( hom C (h (f x)) (h (f y))) + ( hom C (k' (f x)) (k' (f y))) ( transport (A → C) (\ f' → hom C (f' x) (f' y)) ( comp A B C h f) - ( comp A B C k g) - ( comp-homotopic-maps A B C f g h k p q)) - ( ap-hom B C h (f x) (f y)) - := - ind-path (A → B) f - ( \ g' p' → - comp (hom B (f x) (f y)) (hom B (g' x) (g' y)) (hom C (k (g' x)) (k (g' y))) - ( ap-hom B C k (g' x) (g' y)) - ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g' p') - = - comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g' x)) (k (g' y))) - ( transport (A → C) (\ f' → hom C (f' x) (f' y)) - ( comp A B C h f) - ( comp A B C k g') - ( comp-homotopic-maps A B C f g' h k p' q)) - ( ap-hom B C h (f x) (f y))) - ( ind-path (B → C) h - ( \ k' q' → - comp (hom B (f x) (f y)) (hom B (f x) (f y)) (hom C (k' (f x)) (k' (f y))) - ( ap-hom B C k' (f x) (f y)) - ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f f refl) - = - comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k' (f x)) (k' (f y))) - ( transport (A → C) (\ f' → hom C (f' x) (f' y)) - ( comp A B C h f) - ( comp A B C k' f) - ( comp-homotopic-maps A B C f f h k' refl q')) - ( ap-hom B C h (f x) (f y))) - ( refl) - ( k) - ( q)) - ( g) - ( p) + ( comp A B C k' f) + ( comp-homotopic-maps A B C f f h k' refl q')) + ( ap-hom B C h (f x) (f y))) + ( refl) + ( k) + ( q)) + ( g) + ( p) ``` ## Natural transformations @@ -520,11 +528,11 @@ equivalent to the family of fibers of $f\_t$. ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) : U := - fib - ( (t : ψ) → A t [ϕ t ↦ a t]) - ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) - ( postcomp-Π-ext I ψ ϕ A B a f) - ( β) + fib + ( (t : ψ) → A t [ϕ t ↦ a t]) + ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( postcomp-Π-ext I ψ ϕ A B a f) + ( β) #def fiber-family-ext ( I : CUBE) @@ -535,8 +543,7 @@ equivalent to the family of fibers of $f\_t$. ( f : (t : ψ) → (A t → B t)) ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) : U - := - (t : ψ) → fib (A t) (B t) (f t) (β t) [ϕ t ↦ (a t, refl)] + := (t : ψ) → fib (A t) (B t) (f t) (β t) [ϕ t ↦ (a t, refl)] #def equiv-fiber-postcomp-Π-ext-fiber-family-ext ( I : CUBE) @@ -550,12 +557,12 @@ equivalent to the family of fibers of $f\_t$. ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) ( fiber-family-ext I ψ ϕ A B a f β) := - equiv-comp - ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) - ( relative-extension-type I ψ ϕ A B f a β) - ( fiber-family-ext I ψ ϕ A B a f β) - ( equiv-relative-extension-type-fib extext I ψ ϕ A B f a β) - ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = β t) a (\ t → refl)) + equiv-comp + ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) + ( relative-extension-type I ψ ϕ A B f a β) + ( fiber-family-ext I ψ ϕ A B a f β) + ( equiv-relative-extension-type-fib extext I ψ ϕ A B f a β) + ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = β t) a (\ t → refl)) ``` In particular, if $f: \prod_{t : I|\psi} A (t) \to B (t)$ is a family of @@ -573,10 +580,10 @@ equivalence then the fibers of postcomposition by f are contractible. ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) : is-contr (fiber-family-ext I ψ ϕ A B a f β) := - weakextext I ψ ϕ - ( \ t → fib (A t) (B t) (f t) (β t)) - ( \ t → is-contr-map-is-equiv (A t) (B t) (f t) (family-equiv-f t) (β t)) - ( \ t → (a t, refl)) + weakextext I ψ ϕ + ( \ t → fib (A t) (B t) (f t) (β t)) + ( \ t → is-contr-map-is-equiv (A t) (B t) (f t) (family-equiv-f t) (β t)) + ( \ t → (a t, refl)) #def is-contr-fiber-postcomp-Π-ext-is-equiv-fam uses (weakextext extext) ( I : CUBE) @@ -589,11 +596,11 @@ equivalence then the fibers of postcomposition by f are contractible. ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) : is-contr (fiber-postcomp-Π-ext I ψ ϕ A B a f β) := - is-contr-equiv-is-contr' - ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) - ( fiber-family-ext I ψ ϕ A B a f β) - ( equiv-fiber-postcomp-Π-ext-fiber-family-ext I ψ ϕ A B a f β) - ( is-contr-fiber-family-ext-contr-fib I ψ ϕ A B a f β family-equiv-f) + is-contr-equiv-is-contr' + ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) + ( fiber-family-ext I ψ ϕ A B a f β) + ( equiv-fiber-postcomp-Π-ext-fiber-family-ext I ψ ϕ A B a f β) + ( is-contr-fiber-family-ext-contr-fib I ψ ϕ A B a f β family-equiv-f) #def is-equiv-postcomp-Π-ext-is-equiv uses (weakextext extext) ( I : CUBE) @@ -604,15 +611,16 @@ equivalence then the fibers of postcomposition by f are contractible. ( f : (t : ψ) → (A t → B t)) ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) : is-equiv - ( (t : ψ) → A t [ϕ t ↦ a t]) - ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) - ( postcomp-Π-ext I ψ ϕ A B a f) + ( (t : ψ) → A t [ϕ t ↦ a t]) + ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( postcomp-Π-ext I ψ ϕ A B a f) := - is-equiv-is-contr-map - ( (t : ψ) → A t [ϕ t ↦ a t]) - ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) - ( postcomp-Π-ext I ψ ϕ A B a f) - ( \ β → is-contr-fiber-postcomp-Π-ext-is-equiv-fam I ψ ϕ A B a f β family-equiv-f) + is-equiv-is-contr-map + ( (t : ψ) → A t [ϕ t ↦ a t]) + ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( postcomp-Π-ext I ψ ϕ A B a f) + ( \ β + → is-contr-fiber-postcomp-Π-ext-is-equiv-fam I ψ ϕ A B a f β family-equiv-f) ``` Using this result we can show that `#!rzk ap-hom` is an equivalence when f is an @@ -626,12 +634,10 @@ equivalence. ( x y : A) : is-equiv (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) := - is-equiv-postcomp-Π-ext-is-equiv 2 Δ¹ ∂Δ¹ - ( \ t → A) - ( \ t → B) - ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) - ( \ t → f) - ( \ t → is-equiv-f) + is-equiv-postcomp-Π-ext-is-equiv 2 Δ¹ ∂Δ¹ + ( \ _ → A) ( \ _ → B) + ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) + ( \ _ → f) ( \ _ → is-equiv-f) ``` More precicely: @@ -644,11 +650,7 @@ More precicely: ( β : hom B (f x) (f y)) : U := - fib - ( hom A x y) - ( hom B (f x) (f y)) - ( ap-hom A B f x y) - ( β) + fib (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) (β) #def is-contr-fiber-ap-hom-is-equiv uses (weakextext extext) ( A B : U) @@ -658,13 +660,12 @@ More precicely: ( β : hom B (f x) (f y)) : is-contr (fiber-ap-hom A B x y f β) := - is-contr-fiber-postcomp-Π-ext-is-equiv-fam 2 Δ¹ ∂Δ¹ - ( \ t → A) - ( \ t → B) - ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) - ( \ t → f) - ( β) - ( \ t → is-equiv-f) + is-contr-fiber-postcomp-Π-ext-is-equiv-fam 2 Δ¹ ∂Δ¹ + ( \ _ → A) ( \ _ → B) + ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) + ( \ _ → f) + ( β) + ( \ _ → is-equiv-f) ``` We can also define a retraction of `#!rzk ap-hom` directly. @@ -677,15 +678,15 @@ We can also define a retraction of `#!rzk ap-hom` directly. ( x y : A) : (hom B (f x) (f y)) → (hom A x y) := - comp - ( hom B (f x) (f y)) - ( hom A (r (f x)) (r (f y))) - ( hom A x y) - ( transport (A → A) (\ g' → (hom A (g' x) (g' y))) - ( comp A B A r f) - ( identity A) - ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) - ( ap-hom B A r (f x) (f y)) + comp + ( hom B (f x) (f y)) + ( hom A (r (f x)) (r (f y))) + ( hom A x y) + ( transport (A → A) (\ g' → (hom A (g' x) (g' y))) + ( comp A B A r f) + ( identity A) + ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) + ( ap-hom B A r (f x) (f y)) #def has-retraction-ap-hom-retraction uses (funext) ( A B : U) @@ -694,11 +695,11 @@ We can also define a retraction of `#!rzk ap-hom` directly. ( x y : A) : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) := - ( retraction-ap-hom-retraction A B f (r, ρ) x y + ( retraction-ap-hom-retraction A B f (r, ρ) x y , \ α → apd (A → A) (\ g' → (hom A (g' x) (g' y))) - ( comp A B A r f) - ( identity A) - ( \ g' → ap-hom A A g' x y α) - ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) + ( comp A B A r f) + ( identity A) + ( \ g' → ap-hom A A g' x y α) + ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) ``` From 01ad86f8bcbe8149596ba6c5728b3e82b9b77799 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Fri, 3 Nov 2023 20:23:53 -0400 Subject: [PATCH 08/12] spelling of discreteness --- src/simplicial-hott/08-covariant.rzk.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index db3cdddd..f92b650a 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -2237,7 +2237,7 @@ are discrete. ``` In particular, in discrete types identity types are discrete. First we show that -equivalences preserve discretness. For that, we need that `#!rzk hom-eq` +equivalences preserve discreteness. For that, we need that `#!rzk hom-eq` commutes with actions on morphisms. ```rzk @@ -2272,7 +2272,7 @@ commutes with actions on morphisms. ( y) ( p) -#def equiv-preserve-discretness uses (extext funext) +#def equiv-preserve-discreteness uses (extext funext) ( A B : U) ( (f, is-equiv-f) : Equiv A B) ( is-discrete-B : is-discrete B) @@ -2305,10 +2305,10 @@ commutes with actions on morphisms. ( x y : A) : is-discrete (x = y) := - equiv-preserve-discretness (x = y) (hom A x y) - ( hom-eq A x y , is-discrete-A x y) - ( is-discrete-hom-is-segal A - ( is-segal-is-discrete extext A is-discrete-A) - ( x) ( y)) + equiv-preserve-discreteness (x = y) (hom A x y) + ( hom-eq A x y , is-discrete-A x y) + ( is-discrete-hom-is-segal A + ( is-segal-is-discrete extext A is-discrete-A) + ( x) ( y)) ``` From cc8361e4fd1a0186b27010e9acddbebe4df23172 Mon Sep 17 00:00:00 2001 From: StiephenPradal Date: Mon, 13 Nov 2023 19:46:21 +0000 Subject: [PATCH 09/12] Improvement of equiv-preserve-discreteness and has-retraction-ap-hom-retraction + hom-eq-naturality into 07-discrete --- .../06-2cat-of-segal-types.rzk.md | 33 ++------- src/simplicial-hott/07-discrete.rzk.md | 37 ++++++++++ src/simplicial-hott/08-covariant.rzk.md | 68 +++---------------- 3 files changed, 55 insertions(+), 83 deletions(-) diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 88657544..1c7870db 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -671,35 +671,16 @@ More precicely: We can also define a retraction of `#!rzk ap-hom` directly. ```rzk -#def retraction-ap-hom-retraction uses (funext) +#def has-retraction-ap-hom-retraction uses (extext) ( A B : U) ( f : A → B) - ( (r, ρ) : has-retraction A B f) - ( x y : A) - : (hom B (f x) (f y)) → (hom A x y) - := - comp - ( hom B (f x) (f y)) - ( hom A (r (f x)) (r (f y))) - ( hom A x y) - ( transport (A → A) (\ g' → (hom A (g' x) (g' y))) - ( comp A B A r f) - ( identity A) - ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) - ( ap-hom B A r (f x) (f y)) - -#def has-retraction-ap-hom-retraction uses (funext) - ( A B : U) - ( f : A → B) - ( (r, ρ) : has-retraction A B f) + ( has-retraction-f : has-retraction A B f) ( x y : A) : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) := - ( retraction-ap-hom-retraction A B f (r, ρ) x y - , \ α → - apd (A → A) (\ g' → (hom A (g' x) (g' y))) - ( comp A B A r f) - ( identity A) - ( \ g' → ap-hom A A g' x y α) - ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ)) + has-retraction-extensions-has-retraction extext 2 Δ¹ ∂Δ¹ + ( \ _ → A) ( \ _ → B) + ( \ _ → f) + ( \ _ → has-retraction-f) + ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) ``` diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md index 67f0fe2d..eda083d5 100644 --- a/src/simplicial-hott/07-discrete.rzk.md +++ b/src/simplicial-hott/07-discrete.rzk.md @@ -967,3 +967,40 @@ Finally, we conclude: : is-segal A := is-contr-hom2-is-discrete A is-discrete-A ``` + +## Naturality for hom-eq + +`#!rzk hom-eq` commute with `#!rzk ap-hom`. + +```rzk +#def hom-eq-naturality + ( A B : U) + ( f : A → B) + ( x y : A) + ( p : x = y) + : + comp (x = y) (hom A x y) (hom B (f x) (f y)) + ( ap-hom A B f x y) + ( hom-eq A x y) + ( p) + = + comp (x = y) ((f x) = (f y)) (hom B (f x) (f y)) + ( hom-eq B (f x) (f y)) + ( ap A B x y f) + ( p) + := + ind-path A x + ( \ y' p' → + comp (x = y') (hom A x y') (hom B (f x) (f y')) + ( ap-hom A B f x y') + ( hom-eq A x y') + ( p') + = + comp (x = y') ((f x) = (f y')) (hom B (f x) (f y')) + ( hom-eq B (f x) (f y')) + ( ap A B x y' f) + ( p')) + ( functors-pres-id extext A B f x) + ( y) + ( p) +``` diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index f92b650a..94badf53 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -23,7 +23,6 @@ This is a literate `rzk` file: Some of the definitions in this file rely on extension extensionality: ```rzk -#assume funext : FunExt #assume extext : ExtExt #assume weakfunext : WeakFunExt #assume naiveextext : NaiveExtExt @@ -2236,70 +2235,26 @@ are discrete. ( y) ``` -In particular, in discrete types identity types are discrete. First we show that -equivalences preserve discreteness. For that, we need that `#!rzk hom-eq` -commutes with actions on morphisms. +In particular, the identity types of discrete types are also discrete. First, we +show that equivalences preserve discreteness, which is a special case of +preservation of local types by equivalences. ```rzk -#def hom-eq-naturality +#def equiv-preserve-discreteness uses (extext) ( A B : U) - ( f : A → B) - ( x y : A) - ( p : x = y) - : - comp (x = y) (hom A x y) (hom B (f x) (f y)) - ( ap-hom A B f x y) - ( hom-eq A x y) - ( p) - = - comp (x = y) ((f x) = (f y)) (hom B (f x) (f y)) - ( hom-eq B (f x) (f y)) - ( ap A B x y f) - ( p) - := - ind-path A x - ( \ y' p' → - comp (x = y') (hom A x y') (hom B (f x) (f y')) - ( ap-hom A B f x y') - ( hom-eq A x y') - ( p') - = - comp (x = y') ((f x) = (f y')) (hom B (f x) (f y')) - ( hom-eq B (f x) (f y')) - ( ap A B x y' f) - ( p')) - ( functors-pres-id extext A B f x) - ( y) - ( p) - -#def equiv-preserve-discreteness uses (extext funext) - ( A B : U) - ( (f, is-equiv-f) : Equiv A B) + ( A≅B : Equiv A B) ( is-discrete-B : is-discrete B) : is-discrete A := - \ x y → - is-equiv-right-cancel (x = y) (hom A x y) (hom B (f x) (f y)) - ( hom-eq A x y) - ( ap-hom A B f x y) - ( has-retraction-ap-hom-retraction funext A B f (π₁ is-equiv-f) x y) - ( is-equiv-homotopy (x = y) (hom B (f x) (f y)) - ( comp (x = y) (hom A x y) (hom B (f x) (f y)) - ( ap-hom A B f x y) - ( hom-eq A x y)) - ( comp (x = y) ((f x) = (f y)) (hom B (f x) (f y)) - ( hom-eq B (f x) (f y)) - ( ap A B x y f)) - ( hom-eq-naturality A B f x y) - ( is-equiv-comp (x = y) ((f x) = (f y)) (hom B (f x) (f y)) - ( ap A B x y f) - ( is-emb-is-equiv A B f is-equiv-f x y) - ( hom-eq B (f x) (f y)) - ( is-discrete-B (f x) (f y)))) + is-discrete-is-Δ¹-local A + (is-Δ¹-local-is-left-local A + ( is-local-type-equiv-is-local-type extext 2 Δ¹ (\ t → t ≡ 0₂) A B A≅B + ( is-left-local-is-Δ¹-local B + (is-Δ¹-local-is-discrete B is-discrete-B)))) ``` ```rzk title="RS17, Corollary 8.20" -#def is-discrete-id-path-is-discrete uses (extext funext) +#def is-discrete-id-path-is-discrete uses (extext) ( A : U) ( is-discrete-A : is-discrete A) ( x y : A) @@ -2310,5 +2265,4 @@ commutes with actions on morphisms. ( is-discrete-hom-is-segal A ( is-segal-is-discrete extext A is-discrete-A) ( x) ( y)) - ``` From 73578f8e9f5a9c4099d4bf4b8a16c55ba7c34138 Mon Sep 17 00:00:00 2001 From: StiephenPradal Date: Thu, 23 Nov 2023 12:35:56 +0000 Subject: [PATCH 10/12] Reorganisation of Functoriality of Extension Types --- src/simplicial-hott/03-extension-types.rzk.md | 226 ++++++++++-------- .../04-right-orthogonal.rzk.md | 6 +- src/simplicial-hott/05-segal-types.rzk.md | 5 +- .../06-2cat-of-segal-types.rzk.md | 138 +---------- src/simplicial-hott/07-discrete.rzk.md | 11 +- src/simplicial-hott/08-covariant.rzk.md | 6 +- 6 files changed, 145 insertions(+), 247 deletions(-) diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index 2efa36ab..3b2d9528 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -1131,39 +1131,70 @@ Given a map `α : A' → A`, there is also a notion of relative extension types. #variable I : CUBE #variable ψ : I → TOPE #variable ϕ : ψ → TOPE -#variables A' A : ψ → U -#variable α : (t : ψ) → A' t → A t -#variable σ' : (t : ϕ) → A' t -#variable τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)] +#variables A B : ψ → U +#variable f : (t : ψ) → A t → B t +#variable a : (t : ϕ) → A t +#variable τ : (t : ψ) → B t [ϕ t ↦ f t (a t)] #def relative-extension-type : U := - Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) - , ( ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]) + Σ ( τ' : (t : ψ) → A t [ϕ t ↦ a t]) + , ( ( t : ψ) → (f t (τ' t) = τ t) [ϕ t ↦ refl]) +``` -#def relative-extension-type' +This is equivalently expressed as the fibers of postcomposition by $f$. + +```rzk +#def postcomp-Π-ext + : ((t : ψ) → A t [ϕ t ↦ a t]) → + ((t : ψ) → B t [ϕ t ↦ f t (a t)]) + := ( \ τ' t → f t (τ' t)) + +#def fiber-postcomp-Π-ext : U := fib - ( (t : ψ) → A' t [ϕ t ↦ σ' t]) - ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) - ( \ τ' t → α t (τ' t)) + ( (t : ψ) → A t [ϕ t ↦ a t]) + ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( postcomp-Π-ext) ( τ) #def equiv-relative-extension-type-fib uses (extext) : Equiv - ( relative-extension-type') + ( fiber-postcomp-Π-ext) ( relative-extension-type) := total-equiv-family-of-equiv - ( (t : ψ) → A' t [ϕ t ↦ σ' t]) - ( \ τ' → (\ t → α t (τ' t)) =_{ (t : ψ) → A t [ϕ t ↦ α t (σ' t)]} τ) - ( \ τ' → (t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]) + ( (t : ψ) → A t [ϕ t ↦ a t]) + ( \ τ' → (\ t → f t (τ' t)) =_{ (t : ψ) → B t [ϕ t ↦ f t (a t)]} τ) + ( \ τ' → (t : ψ) → (f t (τ' t) = τ t) [ϕ t ↦ refl]) ( \ τ' → - equiv-ExtExt extext I ψ ϕ A - ( \ t → α t (σ' t)) - ( \ t → α t (τ' t)) ( τ)) + equiv-ExtExt extext I ψ ϕ B + ( \ t → f t (a t)) + ( \ t → f t (τ' t)) ( τ)) +``` + +The fiber of postcomposition by a map $f: \prod_{t : I|\psi} A (t) \to B (t)$ is +equivalent to the family of fibers of $f\_t$. + +```rzk +#def fiber-family-ext + : U + := (t : ψ) → fib (A t) (B t) (f t) (τ t) [ϕ t ↦ (a t, refl)] + +#def equiv-fiber-postcomp-Π-ext-fiber-family-ext uses (extext) + : Equiv + ( fiber-postcomp-Π-ext) + ( fiber-family-ext) + := + equiv-comp + ( fiber-postcomp-Π-ext) + ( relative-extension-type) + ( fiber-family-ext) + ( equiv-relative-extension-type-fib) + ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = τ t) a (\ t → refl)) + #end relative-extension-types ``` @@ -1312,100 +1343,68 @@ We can view it as a map of maps either vertically or horizontally. ### Equivalences induce equivalences of extension types -We start by treating the case of extensions from the empty shape `BOT`. - -It follows from extension extensionality that if `f : A → B` is an equivalence, -then so is the map of maps `map-of-restriction-maps`. +If $f: \prod_{t : I|\psi} A (t) \to B (t)$ is a family of equivalence then the +fibers of postcomposition by $f$ are contractible. ```rzk -#def is-equiv-extensions-BOT-is-equiv uses (extext) - ( I : CUBE) - ( ψ : I → TOPE) - ( A B : ψ → U) - ( f : (t : ψ) → (A t) → (B t)) - ( is-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) - : is-equiv ((t : ψ) → A t) ((t : ψ) → B t) ( \ a t → f t (a t)) - := ( ( ( \ b t → (first (first (is-equiv-f t))) (b t)) - , ( \ a → - naiveextext-extext extext I ψ ( \ t → BOT) - ( A) - ( \ u → recBOT) - ( \ t → first (first (is-equiv-f t)) (f t (a t))) - ( a) - ( \ t → second (first (is-equiv-f t)) (a t)))) - , ( ( \ b t → first (second (is-equiv-f t)) (b t)) - , ( \ b → - naiveextext-extext extext I ψ ( \ t → BOT) - ( B) - ( \ u → recBOT) - ( \ t → f t (first (second (is-equiv-f t)) (b t))) - ( b) - ( \ t → second (second (is-equiv-f t)) (b t))))) - -#def equiv-extensions-BOT-equiv uses (extext) - ( I : CUBE) - ( ψ : I → TOPE) - ( A B : ψ → U) - ( famequiv : (t : ψ) → (Equiv (A t) (B t))) - : Equiv ((t : ψ) → A t) ((t : ψ) → B t) - := - ( ( \ a t → first ( famequiv t) (a t)) - , is-equiv-extensions-BOT-is-equiv I ψ A B - ( \ t → first (famequiv t)) - ( \ t → second (famequiv t))) -#def equiv-of-restriction-maps-equiv uses (extext) - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) - ( A B : ψ → U) - ( famequiv : (t : ψ) → (Equiv (A t) (B t))) - : Equiv-of-maps - ( (t : ψ) → A t) ( (t : ϕ) → A t) (\ a t → a t) - ( (t : ψ) → B t) ( (t : ϕ) → B t) (\ b t → b t) +#def is-contr-fiber-family-ext-contr-fib + (I : CUBE) + (ψ : I → TOPE) + (ϕ : ψ → TOPE) + (A B : ψ → U) + (f : (t : ψ) → A t → B t) + (a : (t : ϕ) → A t) + (τ : (t : ψ) → B t [ϕ t ↦ f t (a t)]) + (family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) + : is-contr (fiber-family-ext I ψ ϕ A B f a τ) := - ( map-of-restriction-maps I ψ ϕ A B (\ t → first (famequiv t)) - , ( second (equiv-extensions-BOT-equiv I ψ A B famequiv) - , second ( equiv-extensions-BOT-equiv I - (\ t → ϕ t) (\ t → A t) (\ t → B t) (\ t → famequiv t)))) + ((weakextext-extext extext) I ψ ϕ + ( \ t → fib (A t) (B t) (f t) (τ t)) + ( \ t → is-contr-map-is-equiv (A t) (B t) (f t) (family-equiv-f t) (τ t)) + ( \ t → (a t, refl))) + +#def is-contr-fiber-postcomp-Π-ext-is-equiv-fam uses (extext) + (I : CUBE) + (ψ : I → TOPE) + (ϕ : ψ → TOPE) + (A B : ψ → U) + (f : (t : ψ) → A t → B t) + (a : (t : ϕ) → A t) + (τ : (t : ψ) → B t [ϕ t ↦ f t (a t)]) + (family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) + : is-contr (fiber-postcomp-Π-ext I ψ ϕ A B f a τ) + := + is-contr-equiv-is-contr' + ( fiber-postcomp-Π-ext I ψ ϕ A B f a τ) + ( fiber-family-ext I ψ ϕ A B f a τ) + ( equiv-fiber-postcomp-Π-ext-fiber-family-ext I ψ ϕ A B f a τ) + ( is-contr-fiber-family-ext-contr-fib I ψ ϕ A B f a τ family-equiv-f) ``` -Now we use the result for extensions of `BOT` to bootstrap to arbitrary -extensions. We show that an equivalence `f : A → B` induces an equivalence of -all extension types, not just those extended from `BOT`. +Hence, postcomposing with an equivalence induces an equivalence of extension +types. ```rzk #def is-equiv-extensions-is-equiv uses (extext) - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) - ( A B : ψ → U) - ( f : (t : ψ) → A t → B t) - ( is-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) - : ( a : (t : ϕ) → A t) - → is-equiv + (I : CUBE) + (ψ : I → TOPE) + (ϕ : ψ → TOPE) + (A B : ψ → U) + (f : (t : ψ) → A t → B t) + (a : (t : ϕ) → A t) + (family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) + : is-equiv ( (t : ψ) → A t [ϕ t ↦ a t]) ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) - ( \ a' t → f t (a' t)) + ( postcomp-Π-ext I ψ ϕ A B f a) := - is-homotopy-cartesian-is-horizontal-equiv - ( (t : ϕ) → A t) - ( \ a → (t : ψ) → A t [ϕ t ↦ a t]) - ( (t : ϕ) → B t) - ( \ b → (t : ψ) → B t [ϕ t ↦ b t]) - ( \ a t → f t (a t)) - ( \ _ a' t → f t (a' t)) - ( is-equiv-extensions-BOT-is-equiv - ( I) (\ t → ϕ t) (\ t → A t) (\ t → B t) ( \ t → f t) - ( \ (t : ϕ) → is-equiv-f t)) - ( is-equiv-Equiv-is-equiv' - ( (t : ψ) → A t) ((t : ψ) → B t) (\ a' t → f t (a' t)) - ( Σ (a : (t : ϕ) → A t) , ((t : ψ) → A t [ϕ t ↦ a t])) - ( Σ (b : (t : ϕ) → B t) , ((t : ψ) → B t [ϕ t ↦ b t])) - ( \ (a , a') → ( \ t → f t (a t) , \ t → f t (a' t))) - ( cofibration-composition-functorial - I ψ ϕ (\ _ → BOT) A B f (\ _ → recBOT)) - ( is-equiv-extensions-BOT-is-equiv I ψ A B f is-equiv-f)) + is-equiv-is-contr-map + ( (t : ψ) → A t [ϕ t ↦ a t]) + ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( postcomp-Π-ext I ψ ϕ A B f a) + ( \ τ + → is-contr-fiber-postcomp-Π-ext-is-equiv-fam I ψ ϕ A B f a τ family-equiv-f) #def equiv-extensions-equiv uses (extext) ( I : CUBE) @@ -1418,11 +1417,31 @@ all extension types, not just those extended from `BOT`. ( (t : ψ) → A t [ϕ t ↦ a t]) ( (t : ψ) → B t [ϕ t ↦ first (equivs-A-B t) (a t)]) := - ( ( \ a' t → first (equivs-A-B t) (a' t)) + ( ( postcomp-Π-ext I ψ ϕ A B (\ t → (first (equivs-A-B t))) a) , ( is-equiv-extensions-is-equiv I ψ ϕ A B ( \ t → first (equivs-A-B t)) - ( \ t → second (equivs-A-B t)) - ( a))) + ( a) + ( \ t → second (equivs-A-B t)))) + +#def equiv-of-restriction-maps-equiv uses (extext) + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( famequiv : (t : ψ) → (Equiv (A t) (B t))) + : Equiv-of-maps + ( (t : ψ) → A t) ( (t : ϕ) → A t) (\ a t → a t) + ( (t : ψ) → B t) ( (t : ϕ) → B t) (\ b t → b t) + := + ( map-of-restriction-maps I ψ ϕ A B (\ t → first (famequiv t)) + , ( second (equiv-extensions-equiv I ψ ( \ _ → BOT) + ( A) ( B) + ( famequiv) + ( \ _ → recBOT)) + , second ( equiv-extensions-equiv I ( \ t → ϕ t) ( \ _ → BOT) + ( \ t → A t) ( \ t → B t) + ( \ t → famequiv t) + ( \ _ → recBOT)))) ``` ### Retracts induce retracts of extension types @@ -1454,8 +1473,9 @@ working with external retractions. := is-equiv-extensions-is-equiv I ψ ϕ A A ( \ t a₀ → r t (s t (a₀))) - ( \ t → is-equiv-retraction-section (A t) (B t) (s t) (r t) (η t)) ( a) + ( \ t → is-equiv-retraction-section (A t) (B t) (s t) (r t) (η t)) + #def has-retraction-extensions-has-retraction' uses (extext η) ( a : (t : ϕ) → A t) diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index c4460528..e8ac364b 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -504,8 +504,8 @@ Every equivalence `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`. ( is-equiv-α : is-equiv A' A α) : is-right-orthogonal-to-shape I ψ ϕ A' A α := - is-equiv-extensions-is-equiv extext I ψ ϕ - ( \ _ → A') ( \ _ → A) ( \ _ → α) ( \ _ → is-equiv-α) + ( \ a → is-equiv-extensions-is-equiv extext I ψ ϕ + ( \ _ → A') ( \ _ → A) ( \ _ → α) ( a) ( \ _ → is-equiv-α)) ``` Right orthogonality is closed under homotopy. @@ -664,7 +664,7 @@ follows for the former. = τhB) := ind-has-section-equiv - ( relative-extension-type' I ψ ϕ + ( fiber-postcomp-Π-ext I ψ ϕ ( \ _ → relative-product A A' α B f) ( \ _ → B) ( \ _ → second-relative-product A A' α B f) ( σB') ( τB)) diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md index dc45bedf..095468ce 100644 --- a/src/simplicial-hott/05-segal-types.rzk.md +++ b/src/simplicial-hott/05-segal-types.rzk.md @@ -676,10 +676,11 @@ then $(x : X) → A x$ is a Segal type. ( \ t s → A s) ( \ u → recBOT))) ( \ h s t → h s t) -- second equivalence - ( second (equiv-extensions-BOT-equiv extext I ψ + ( second (equiv-extensions-equiv extext I ψ (\ _ → BOT) ( \ s → Δ² → A s) ( \ s → Λ → A s) - ( \ s → (horn-restriction (A s) , fiberwise-is-segal-A s)))) + ( \ s → (horn-restriction (A s) , fiberwise-is-segal-A s)) + ( \ _ → recBOT))) ( \ h t s → (h s) t) -- third equivalence ( second ( fubini diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 1c7870db..1e9f41c0 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -21,7 +21,6 @@ extension extensionality: ```rzk #assume funext : FunExt #assume extext : ExtExt -#assume weakextext : WeakExtExt ``` ## Functors @@ -504,140 +503,23 @@ the "Gray interchanger" built from two commutative triangles. ## Equivalences are fully faithful -The fiber of postcomposition by a map $f: \prod_{t : I|\psi} A (t) \to B (t)$ is -equivalent to the family of fibers of $f\_t$. +Since `#!rzk hom` is defined as an extension type, `#!rzk ap-hom` correspond to +postcomposition. Hence, we can use `#!rzk is-equiv-extensions-is-equiv` to show +that `#!rzk ap-hom` is an equivalence when f is an equivalence. ```rzk -#def postcomp-Π-ext - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) - ( A B : ψ → U) - ( a : (t : ϕ) → A t) - ( f : (t : ψ) → (A t → B t)) - : ((t : ψ) → A t [ϕ t ↦ a t]) → ((t : ψ) → B t [ϕ t ↦ f t (a t)]) - := ( \ α t → f t (α t)) - -#def fiber-postcomp-Π-ext -- already defined as relative extension type in 03-extension-types - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) - ( A B : ψ → U) - ( a : (t : ϕ) → A t) - ( f : (t : ψ) → (A t → B t)) - ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) - : U - := - fib - ( (t : ψ) → A t [ϕ t ↦ a t]) - ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) - ( postcomp-Π-ext I ψ ϕ A B a f) - ( β) - -#def fiber-family-ext - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) - ( A B : ψ → U) - ( a : (t : ϕ) → A t) - ( f : (t : ψ) → (A t → B t)) - ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) - : U - := (t : ψ) → fib (A t) (B t) (f t) (β t) [ϕ t ↦ (a t, refl)] - -#def equiv-fiber-postcomp-Π-ext-fiber-family-ext - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) - ( A B : ψ → U) - ( a : (t : ϕ) → A t) - ( f : (t : ψ) → (A t → B t)) - ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) - : Equiv - ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) - ( fiber-family-ext I ψ ϕ A B a f β) - := - equiv-comp - ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) - ( relative-extension-type I ψ ϕ A B f a β) - ( fiber-family-ext I ψ ϕ A B a f β) - ( equiv-relative-extension-type-fib extext I ψ ϕ A B f a β) - ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = β t) a (\ t → refl)) -``` - -In particular, if $f: \prod_{t : I|\psi} A (t) \to B (t)$ is a family of -equivalence then the fibers of postcomposition by f are contractible. - -```rzk -#def is-contr-fiber-family-ext-contr-fib - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) - ( A B : ψ → U) - ( a : (t : ϕ) → A t) - ( f : (t : ψ) → (A t → B t)) - ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) - ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) - : is-contr (fiber-family-ext I ψ ϕ A B a f β) - := - weakextext I ψ ϕ - ( \ t → fib (A t) (B t) (f t) (β t)) - ( \ t → is-contr-map-is-equiv (A t) (B t) (f t) (family-equiv-f t) (β t)) - ( \ t → (a t, refl)) - -#def is-contr-fiber-postcomp-Π-ext-is-equiv-fam uses (weakextext extext) - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) - ( A B : ψ → U) - ( a : (t : ϕ) → A t) - ( f : (t : ψ) → (A t → B t)) - ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)]) - ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) - : is-contr (fiber-postcomp-Π-ext I ψ ϕ A B a f β) - := - is-contr-equiv-is-contr' - ( fiber-postcomp-Π-ext I ψ ϕ A B a f β) - ( fiber-family-ext I ψ ϕ A B a f β) - ( equiv-fiber-postcomp-Π-ext-fiber-family-ext I ψ ϕ A B a f β) - ( is-contr-fiber-family-ext-contr-fib I ψ ϕ A B a f β family-equiv-f) - -#def is-equiv-postcomp-Π-ext-is-equiv uses (weakextext extext) - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) - ( A B : ψ → U) - ( a : (t : ϕ) → A t) - ( f : (t : ψ) → (A t → B t)) - ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) - : is-equiv - ( (t : ψ) → A t [ϕ t ↦ a t]) - ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) - ( postcomp-Π-ext I ψ ϕ A B a f) - := - is-equiv-is-contr-map - ( (t : ψ) → A t [ϕ t ↦ a t]) - ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) - ( postcomp-Π-ext I ψ ϕ A B a f) - ( \ β - → is-contr-fiber-postcomp-Π-ext-is-equiv-fam I ψ ϕ A B a f β family-equiv-f) -``` - -Using this result we can show that `#!rzk ap-hom` is an equivalence when f is an -equivalence. - -```rzk -#def is-equiv-ap-hom-is-equiv uses (weakextext extext) +#def is-equiv-ap-hom-is-equiv uses (extext) ( A B : U) ( f : A → B) ( is-equiv-f : is-equiv A B f) ( x y : A) : is-equiv (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) := - is-equiv-postcomp-Π-ext-is-equiv 2 Δ¹ ∂Δ¹ + is-equiv-extensions-is-equiv extext 2 Δ¹ ∂Δ¹ ( \ _ → A) ( \ _ → B) + ( \ _ → f) ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) - ( \ _ → f) ( \ _ → is-equiv-f) + ( \ _ → is-equiv-f) ``` More precicely: @@ -652,7 +534,7 @@ More precicely: := fib (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) (β) -#def is-contr-fiber-ap-hom-is-equiv uses (weakextext extext) +#def is-contr-fiber-ap-hom-is-equiv uses (extext) ( A B : U) ( f : A → B) ( is-equiv-f : is-equiv A B f) @@ -660,10 +542,10 @@ More precicely: ( β : hom B (f x) (f y)) : is-contr (fiber-ap-hom A B x y f β) := - is-contr-fiber-postcomp-Π-ext-is-equiv-fam 2 Δ¹ ∂Δ¹ + is-contr-fiber-postcomp-Π-ext-is-equiv-fam extext 2 Δ¹ ∂Δ¹ ( \ _ → A) ( \ _ → B) + ( \ _ → f) ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) - ( \ _ → f) ( β) ( \ _ → is-equiv-f) ``` diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md index eda083d5..95cd9208 100644 --- a/src/simplicial-hott/07-discrete.rzk.md +++ b/src/simplicial-hott/07-discrete.rzk.md @@ -252,8 +252,7 @@ of discrete types is discrete. ``` By extension extensionality, an extension type into a family of discrete types -is discrete. Since `#!rzk equiv-extensions-BOT-equiv` considers total extension -types only, extending from `#!rzk BOT`, that's all we prove here for now. +is discrete. ```rzk #def equiv-hom-eq-extension-type-is-discrete uses (extext) @@ -270,13 +269,11 @@ types only, extending from `#!rzk BOT`, that's all we prove here for now. ( (t : ψ) → hom (A t) (f t) (g t)) ( hom ((t : ψ) → A t) f g) ( equiv-ExtExt extext I ψ (\ _ → BOT) A (\ _ → recBOT) f g) - ( equiv-extensions-BOT-equiv - ( extext) - ( I) - ( ψ) + ( equiv-extensions-equiv extext I ψ (\ _ → BOT) ( \ t → f t = g t) ( \ t → hom (A t) (f t) (g t)) - ( \ t → (hom-eq (A t) (f t) (g t) , (is-discrete-A t (f t) (g t))))) + ( \ t → (hom-eq (A t) (f t) (g t) , (is-discrete-A t (f t) (g t)))) + ( \ _ → recBOT)) ( fubini ( I) ( 2) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 94badf53..edd1a022 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -1454,13 +1454,11 @@ domain are equivalent: #def equiv-total-dhom-equiv uses (A x y) : Equiv ( (t : Δ¹) → B (f t)) ((t : Δ¹) → C (f t)) := - equiv-extensions-BOT-equiv - ( extext) - ( 2) - ( Δ¹) + equiv-extensions-equiv extext 2 Δ¹ (\ _ → BOT) ( \ t → B (f t)) ( \ t → C (f t)) ( \ t → equiv-BC (f t)) + ( \ _ → recBOT) #def equiv-total-covariant-dhom-equiv uses (extext equiv-BC) : Equiv From bff355514231cffb16bf4ae3ff328bfd0ee6bf67 Mon Sep 17 00:00:00 2001 From: StiephenPradal Date: Thu, 23 Nov 2023 12:57:11 +0000 Subject: [PATCH 11/12] Fixing spacing --- src/simplicial-hott/03-extension-types.rzk.md | 102 +++++++++--------- .../06-2cat-of-segal-types.rzk.md | 24 ++--- 2 files changed, 61 insertions(+), 65 deletions(-) diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index a4125e2e..67230927 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -1261,12 +1261,12 @@ equivalent to the family of fibers of $f\_t$. ( fiber-postcomp-Π-ext) ( fiber-family-ext) := - equiv-comp - ( fiber-postcomp-Π-ext) - ( relative-extension-type) - ( fiber-family-ext) - ( equiv-relative-extension-type-fib) - ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = τ t) a (\ t → refl)) + equiv-comp + ( fiber-postcomp-Π-ext) + ( relative-extension-type) + ( fiber-family-ext) + ( equiv-relative-extension-type-fib) + ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = τ t) a (\ t → refl)) #end relative-extension-types ``` @@ -1395,9 +1395,7 @@ We can view it as a map of maps either vertically or horizontally. ( (t : ψ) → A t) ( (t : ϕ) → A t) (\ a t → a t) ( (t : ψ) → B t) ( (t : ϕ) → B t) (\ b t → b t) := - ( ( ( \ a t → f t (a t)) - , ( \ a t → f t (a t))) - , \ _ → refl) + ( ( (\ a t → f t (a t)), (\ a t → f t (a t))), \ _ → refl) #def map-of-map-extension-type ( I : CUBE) @@ -1409,9 +1407,7 @@ We can view it as a map of maps either vertically or horizontally. ( (t : ψ) → A t) ( (t : ψ) → B t) (\ a t → f t (a t)) ( (t : ϕ) → A t) ( (t : ϕ) → B t) (\ a t → f t (a t)) := - ( ( ( \ a t → a t) - , ( \ b t → b t)) - , \ _ → refl) + ( ( (\ a t → a t), (\ b t → b t)), \ _ → refl) ``` ### Equivalences induce equivalences of extension types @@ -1422,37 +1418,37 @@ fibers of postcomposition by $f$ are contractible. ```rzk #def is-contr-fiber-family-ext-contr-fib - (I : CUBE) - (ψ : I → TOPE) - (ϕ : ψ → TOPE) - (A B : ψ → U) - (f : (t : ψ) → A t → B t) - (a : (t : ϕ) → A t) - (τ : (t : ψ) → B t [ϕ t ↦ f t (a t)]) - (family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( f : (t : ψ) → A t → B t) + ( a : (t : ϕ) → A t) + ( τ : (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) : is-contr (fiber-family-ext I ψ ϕ A B f a τ) := - ((weakextext-extext extext) I ψ ϕ - ( \ t → fib (A t) (B t) (f t) (τ t)) - ( \ t → is-contr-map-is-equiv (A t) (B t) (f t) (family-equiv-f t) (τ t)) - ( \ t → (a t, refl))) + (weakextext-extext extext) I ψ ϕ + ( \ t → fib (A t) (B t) (f t) (τ t)) + ( \ t → is-contr-map-is-equiv (A t) (B t) (f t) (family-equiv-f t) (τ t)) + ( \ t → (a t, refl)) #def is-contr-fiber-postcomp-Π-ext-is-equiv-fam uses (extext) - (I : CUBE) - (ψ : I → TOPE) - (ϕ : ψ → TOPE) - (A B : ψ → U) - (f : (t : ψ) → A t → B t) - (a : (t : ϕ) → A t) - (τ : (t : ψ) → B t [ϕ t ↦ f t (a t)]) - (family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( f : (t : ψ) → A t → B t) + ( a : (t : ϕ) → A t) + ( τ : (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) : is-contr (fiber-postcomp-Π-ext I ψ ϕ A B f a τ) := - is-contr-equiv-is-contr' - ( fiber-postcomp-Π-ext I ψ ϕ A B f a τ) - ( fiber-family-ext I ψ ϕ A B f a τ) - ( equiv-fiber-postcomp-Π-ext-fiber-family-ext I ψ ϕ A B f a τ) - ( is-contr-fiber-family-ext-contr-fib I ψ ϕ A B f a τ family-equiv-f) + is-contr-equiv-is-contr' + ( fiber-postcomp-Π-ext I ψ ϕ A B f a τ) + ( fiber-family-ext I ψ ϕ A B f a τ) + ( equiv-fiber-postcomp-Π-ext-fiber-family-ext I ψ ϕ A B f a τ) + ( is-contr-fiber-family-ext-contr-fib I ψ ϕ A B f a τ family-equiv-f) ``` Hence, postcomposing with an equivalence induces an equivalence of extension @@ -1460,24 +1456,24 @@ types. ```rzk #def is-equiv-extensions-is-equiv uses (extext) - (I : CUBE) - (ψ : I → TOPE) - (ϕ : ψ → TOPE) - (A B : ψ → U) - (f : (t : ψ) → A t → B t) - (a : (t : ϕ) → A t) - (family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( f : (t : ψ) → A t → B t) + ( a : (t : ϕ) → A t) + ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) : is-equiv ( (t : ψ) → A t [ϕ t ↦ a t]) ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) ( postcomp-Π-ext I ψ ϕ A B f a) := - is-equiv-is-contr-map - ( (t : ψ) → A t [ϕ t ↦ a t]) - ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) - ( postcomp-Π-ext I ψ ϕ A B f a) - ( \ τ - → is-contr-fiber-postcomp-Π-ext-is-equiv-fam I ψ ϕ A B f a τ family-equiv-f) + is-equiv-is-contr-map + ( (t : ψ) → A t [ϕ t ↦ a t]) + ( (t : ψ) → B t [ϕ t ↦ f t (a t)]) + ( postcomp-Π-ext I ψ ϕ A B f a) + ( \ τ → + is-contr-fiber-postcomp-Π-ext-is-equiv-fam I ψ ϕ A B f a τ family-equiv-f) #def equiv-extensions-equiv uses (extext) ( I : CUBE) @@ -1490,11 +1486,11 @@ types. ( (t : ψ) → A t [ϕ t ↦ a t]) ( (t : ψ) → B t [ϕ t ↦ first (equivs-A-B t) (a t)]) := - ( ( postcomp-Π-ext I ψ ϕ A B (\ t → (first (equivs-A-B t))) a) - , ( is-equiv-extensions-is-equiv I ψ ϕ A B + ( postcomp-Π-ext I ψ ϕ A B (\ t → (first (equivs-A-B t))) a + , is-equiv-extensions-is-equiv I ψ ϕ A B ( \ t → first (equivs-A-B t)) ( a) - ( \ t → second (equivs-A-B t)))) + ( \ t → second (equivs-A-B t))) #def equiv-of-restriction-maps-equiv uses (extext) ( I : CUBE) diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 1e9f41c0..677212a6 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -515,11 +515,11 @@ that `#!rzk ap-hom` is an equivalence when f is an equivalence. ( x y : A) : is-equiv (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) := - is-equiv-extensions-is-equiv extext 2 Δ¹ ∂Δ¹ - ( \ _ → A) ( \ _ → B) - ( \ _ → f) - ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) - ( \ _ → is-equiv-f) + is-equiv-extensions-is-equiv extext 2 Δ¹ ∂Δ¹ + ( \ _ → A) ( \ _ → B) + ( \ _ → f) + ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) + ( \ _ → is-equiv-f) ``` More precicely: @@ -532,7 +532,7 @@ More precicely: ( β : hom B (f x) (f y)) : U := - fib (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) (β) + fib (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) (β) #def is-contr-fiber-ap-hom-is-equiv uses (extext) ( A B : U) @@ -542,12 +542,12 @@ More precicely: ( β : hom B (f x) (f y)) : is-contr (fiber-ap-hom A B x y f β) := - is-contr-fiber-postcomp-Π-ext-is-equiv-fam extext 2 Δ¹ ∂Δ¹ - ( \ _ → A) ( \ _ → B) + is-contr-fiber-postcomp-Π-ext-is-equiv-fam extext 2 Δ¹ ∂Δ¹ + ( \ _ → A) ( \ _ → B) ( \ _ → f) - ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) - ( β) - ( \ _ → is-equiv-f) + ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y)) + ( β) + ( \ _ → is-equiv-f) ``` We can also define a retraction of `#!rzk ap-hom` directly. @@ -560,7 +560,7 @@ We can also define a retraction of `#!rzk ap-hom` directly. ( x y : A) : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) := - has-retraction-extensions-has-retraction extext 2 Δ¹ ∂Δ¹ + has-retraction-extensions-has-retraction extext 2 Δ¹ ∂Δ¹ ( \ _ → A) ( \ _ → B) ( \ _ → f) ( \ _ → has-retraction-f) From a1ee8ee906aba3254221e0325a199afae8f2b052 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Thu, 23 Nov 2023 14:36:18 -0500 Subject: [PATCH 12/12] cosmetic edits --- src/hott/02-homotopies.rzk.md | 12 ++++++------ src/hott/03-equivalences.rzk.md | 12 ++++++------ src/simplicial-hott/03-extension-types.rzk.md | 10 ++++------ src/simplicial-hott/06-2cat-of-segal-types.rzk.md | 8 ++++---- 4 files changed, 20 insertions(+), 22 deletions(-) diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md index a9c5ad23..1e55da48 100644 --- a/src/hott/02-homotopies.rzk.md +++ b/src/hott/02-homotopies.rzk.md @@ -145,12 +145,12 @@ $K^{-1} \cdot H \sim \text{refl-htpy}_{g}$ : comp A B C h f = comp A B C k g := ind-path (A → B) f (\ g' p' → comp A B C h f = comp A B C k g') - ( ind-path (B → C) h (\ k' q' → comp A B C h f = comp A B C k' f) - ( refl) - ( k) - ( q)) - ( g) - ( p) + ( ind-path (B → C) h (\ k' q' → comp A B C h f = comp A B C k' f) + ( refl) + ( k) + ( q)) + ( g) + ( p) ``` ## Naturality diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md index 12a150ed..c31a2198 100644 --- a/src/hott/03-equivalences.rzk.md +++ b/src/hott/03-equivalences.rzk.md @@ -821,9 +821,9 @@ identifications. This defines `#!rzk eq-htpy` to be the retraction to : (comp A B A (π₁ (π₁ is-equiv-f)) f) = (identity A) := eq-htpy A (\ x' → A) - ( comp A B A (π₁ (π₁ is-equiv-f)) f) - ( identity A) - ( π₂ (π₁ is-equiv-f)) + ( comp A B A (π₁ (π₁ is-equiv-f)) f) + ( identity A) + ( π₂ (π₁ is-equiv-f)) #def right-cancel-is-equiv uses (funext) ( A B : U) @@ -832,9 +832,9 @@ identifications. This defines `#!rzk eq-htpy` to be the retraction to : (comp B A B f (π₁ (π₂ is-equiv-f))) = (identity B) := eq-htpy B (\ x' → B) - ( comp B A B f (π₁ (π₂ is-equiv-f))) - ( identity B) - ( π₂ (π₂ is-equiv-f)) + ( comp B A B f (π₁ (π₂ is-equiv-f))) + ( identity B) + ( π₂ (π₂ is-equiv-f)) ``` Using function extensionality, a fiberwise equivalence defines an equivalence of diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index 67230927..d973037d 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -10,10 +10,8 @@ This is a literate `rzk` file: ## Prerequisites -- `hott/4-equivalences.rzk` — contains the definitions of `#!rzk Equiv` and +- `hott/03-equivalences.rzk.md` — contains the definitions of `#!rzk Equiv` and `#!rzk comp-equiv` -- the file `hott/4-equivalences.rzk` relies in turn on the previous files in - `hott/` ## Extension up to homotopy @@ -371,10 +369,10 @@ For each of these we provide a corresponding functorial instance ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)]) := inv-equiv - ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)]) - ( Σ ( f : ((t : ψ) → X t [ϕ t ↦ a t])) + ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)]) + ( Σ ( f : ((t : ψ) → X t [ϕ t ↦ a t])) , ( (t : ψ) → Y t (f t) [ϕ t ↦ b t])) - ( axiom-choice I ψ ϕ X Y a b) + ( axiom-choice I ψ ϕ X Y a b) ``` ## Composites and unions of cofibrations diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md index 677212a6..36301df0 100644 --- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md +++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md @@ -10,10 +10,10 @@ This is a literate `rzk` file: ## Prerequisites -- `3-simplicial-type-theory.md` — We rely on definitions of simplicies and their - subshapes. -- `4-extension-types.md` — We use extension extensionality. -- `5-segal-types.md` - We use the notion of hom types. +- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and + their subshapes. +- `03-extension-types.rzk.md` — We use extension extensionality. +- `05-segal-types.rzk.md` - We use the notion of hom types. Some of the definitions in this file rely on function extensionality and extension extensionality: