From 42e82222687e8e2691684d04759ebb36c502bc15 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 8 Dec 2025 18:47:54 +0000 Subject: [PATCH 1/8] rename retracts of maps to retracts of arrows --- src/foundation-core/retractions.lagda.md | 4 +- .../retracts-of-types.lagda.md | 2 +- src/foundation.lagda.md | 1 - src/foundation/constant-maps.lagda.md | 2 +- src/foundation/decidable-embeddings.lagda.md | 22 +- src/foundation/decidable-maps.lagda.md | 14 +- src/foundation/embeddings.lagda.md | 2 +- ...toriality-cartesian-product-types.lagda.md | 4 +- .../functoriality-fibers-of-maps.lagda.md | 5 +- .../functoriality-morphisms-arrows.lagda.md | 2 +- src/foundation/path-cosplit-maps.lagda.md | 4 +- ...s.lagda.md => retracts-of-arrows.lagda.md} | 614 +++++++++--------- src/foundation/retracts-of-types.lagda.md | 2 +- src/foundation/small-maps.lagda.md | 10 +- src/logic/de-morgan-embeddings.lagda.md | 22 +- src/logic/de-morgan-maps.lagda.md | 16 +- .../double-negation-eliminating-maps.lagda.md | 14 +- ...double-negation-stable-embeddings.lagda.md | 22 +- .../anodyne-maps.lagda.md | 2 +- .../connected-maps-at-subuniverses.lagda.md | 16 +- .../connected-types-at-subuniverses.lagda.md | 6 +- ...alizations-at-global-subuniverses.lagda.md | 4 +- .../functoriality-pullback-hom.lagda.md | 2 +- ...ty-reflective-global-subuniverses.lagda.md | 2 +- .../maps-local-at-maps.lagda.md | 20 +- .../null-types.lagda.md | 6 +- .../types-colocal-at-maps.lagda.md | 18 +- .../types-local-at-maps.lagda.md | 20 +- .../weakly-anodyne-maps.lagda.md | 12 +- .../acyclic-maps.lagda.md | 8 +- .../retracts-of-sequential-diagrams.lagda.md | 2 +- .../truncated-acyclic-maps.lagda.md | 8 +- 32 files changed, 445 insertions(+), 443 deletions(-) rename src/foundation/{retracts-of-maps.lagda.md => retracts-of-arrows.lagda.md} (55%) diff --git a/src/foundation-core/retractions.lagda.md b/src/foundation-core/retractions.lagda.md index bbdeddf6a55..452c9e99b3a 100644 --- a/src/foundation-core/retractions.lagda.md +++ b/src/foundation-core/retractions.lagda.md @@ -266,5 +266,5 @@ module _ - Retracts of types are defined in [`foundation-core.retracts-of-types`](foundation-core.retracts-of-types.md). -- Retracts of maps are defined in - [`foundation.retracts-of-maps`](foundation.retracts-of-maps.md). +- Retracts of arrows are defined in + [`foundation.retracts-of-arrows`](foundation.retracts-of-arrows.md). diff --git a/src/foundation-core/retracts-of-types.lagda.md b/src/foundation-core/retracts-of-types.lagda.md index 1b18d5e0cef..4de46afa824 100644 --- a/src/foundation-core/retracts-of-types.lagda.md +++ b/src/foundation-core/retracts-of-types.lagda.md @@ -236,4 +236,4 @@ syntax step-retract-reasoning e Z f = e retract-of Z by f ## See also -- [Retracts of maps](foundation.retracts-of-maps.md) +- [Retracts of arrows](foundation.retracts-of-arrows.md) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 931de9244e3..cb38823d9b3 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -394,7 +394,6 @@ open import foundation.relaxed-sigma-decompositions public open import foundation.repetitions-of-values public open import foundation.replacement public open import foundation.retractions public -open import foundation.retracts-of-maps public open import foundation.retracts-of-types public open import foundation.sections public open import foundation.separated-types-subuniverses public diff --git a/src/foundation/constant-maps.lagda.md b/src/foundation/constant-maps.lagda.md index dd9b92514d8..ad4abe83c14 100644 --- a/src/foundation/constant-maps.lagda.md +++ b/src/foundation/constant-maps.lagda.md @@ -20,7 +20,7 @@ open import foundation.images open import foundation.morphisms-arrows open import foundation.postcomposition-functions open import foundation.propositional-truncations -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.retracts-of-types open import foundation.transposition-identifications-along-equivalences open import foundation.type-arithmetic-unit-type diff --git a/src/foundation/decidable-embeddings.lagda.md b/src/foundation/decidable-embeddings.lagda.md index 70856d62e23..d53374b3e2f 100644 --- a/src/foundation/decidable-embeddings.lagda.md +++ b/src/foundation/decidable-embeddings.lagda.md @@ -23,7 +23,7 @@ open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositional-maps open import foundation.propositions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.small-maps open import foundation.subtype-identity-principle open import foundation.type-arithmetic-dependent-pair-types @@ -583,7 +583,7 @@ module _ ( is-decidable-prop-map-is-decidable-emb F)) ``` -### Decidable embeddings are closed under retracts of maps +### Decidable embeddings are closed under retracts of arrows ```agda module _ @@ -591,18 +591,18 @@ module _ {f : A → B} {g : X → Y} where - is-decidable-prop-map-retract-map : - f retract-of-map g → is-decidable-prop-map g → is-decidable-prop-map f - is-decidable-prop-map-retract-map R G x = + is-decidable-prop-map-retract-arrow : + f retract-of-arrow g → is-decidable-prop-map g → is-decidable-prop-map f + is-decidable-prop-map-retract-arrow R G x = is-decidable-prop-retract-of - ( retract-fiber-retract-map f g R x) - ( G (map-codomain-inclusion-retract-map f g R x)) + ( retract-fiber-retract-arrow f g R x) + ( G (map-codomain-inclusion-retract-arrow f g R x)) - is-decidable-emb-retract-map : - f retract-of-map g → is-decidable-emb g → is-decidable-emb f - is-decidable-emb-retract-map R G = + is-decidable-emb-retract-arrow : + f retract-of-arrow g → is-decidable-emb g → is-decidable-emb f + is-decidable-emb-retract-arrow R G = is-decidable-emb-is-decidable-prop-map - ( is-decidable-prop-map-retract-map R + ( is-decidable-prop-map-retract-arrow R ( is-decidable-prop-map-is-decidable-emb G)) ``` diff --git a/src/foundation/decidable-maps.lagda.md b/src/foundation/decidable-maps.lagda.md index 89cb4cd7183..09ba8a8ec84 100644 --- a/src/foundation/decidable-maps.lagda.md +++ b/src/foundation/decidable-maps.lagda.md @@ -23,7 +23,7 @@ open import foundation.hilbert-epsilon-operators-maps open import foundation.identity-types open import foundation.iterating-functions open import foundation.propositional-truncations -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.transport-along-identifications open import foundation.universe-levels @@ -312,7 +312,7 @@ module _ ( F (map-codomain-cartesian-hom-arrow g f α d)) ``` -### Decidable maps are closed under retracts of maps +### Decidable maps are closed under retracts of arrows ```agda module _ @@ -320,12 +320,12 @@ module _ {f : A → B} {g : X → Y} where - is-decidable-retract-map : - f retract-of-map g → is-decidable-map g → is-decidable-map f - is-decidable-retract-map R G x = + is-decidable-retract-arrow : + f retract-of-arrow g → is-decidable-map g → is-decidable-map f + is-decidable-retract-arrow R G x = is-decidable-retract-of - ( retract-fiber-retract-map f g R x) - ( G (map-codomain-inclusion-retract-map f g R x)) + ( retract-fiber-retract-arrow f g R x) + ( G (map-codomain-inclusion-retract-arrow f g R x)) ``` ### Decidable maps have Hilbert ε-operators diff --git a/src/foundation/embeddings.lagda.md b/src/foundation/embeddings.lagda.md index 9d0c224af31..998e86d5f78 100644 --- a/src/foundation/embeddings.lagda.md +++ b/src/foundation/embeddings.lagda.md @@ -378,7 +378,7 @@ module _ ( is-prop-map-is-emb is-emb-f)) ``` -### In a commuting square of which the sides are embeddings, the top map is an embedding if and only if the bottom map is an embedding +### In a commuting square of which the sides are equivalences, the top map is an embedding if and only if the bottom map is an embedding ```agda module _ diff --git a/src/foundation/functoriality-cartesian-product-types.lagda.md b/src/foundation/functoriality-cartesian-product-types.lagda.md index 08be06910b8..6c4ad9ae0af 100644 --- a/src/foundation/functoriality-cartesian-product-types.lagda.md +++ b/src/foundation/functoriality-cartesian-product-types.lagda.md @@ -192,8 +192,8 @@ module _ ( map-retraction-map-product f g H K , retraction-map-retraction-map-product f g H K) - retract-map-product : A retract-of C → B retract-of D → A × B retract-of C × D - retract-map-product (f , retraction-f) (g , retraction-g) = + retract-product : A retract-of C → B retract-of D → A × B retract-of C × D + retract-product (f , retraction-f) (g , retraction-g) = ( map-product f g , retraction-map-product f g retraction-f retraction-g) ``` diff --git a/src/foundation/functoriality-fibers-of-maps.lagda.md b/src/foundation/functoriality-fibers-of-maps.lagda.md index 7ecce367511..f595fb3e94c 100644 --- a/src/foundation/functoriality-fibers-of-maps.lagda.md +++ b/src/foundation/functoriality-fibers-of-maps.lagda.md @@ -562,8 +562,9 @@ module _ ## See also -- In [retracts of maps](foundation.retracts-of-maps.md), we show that if `g` is - a retract of `g'`, then the fibers of `g` are retracts of the fibers of `g'`. +- In [retracts of arrows](foundation.retracts-of-arrows.md), we show that if `g` + is a retract of `g'`, then the fibers of `g` are retracts of the fibers of + `g'`. ## Table of files about fibers of maps diff --git a/src/foundation/functoriality-morphisms-arrows.lagda.md b/src/foundation/functoriality-morphisms-arrows.lagda.md index a8cdd6b3870..89d08abf0c5 100644 --- a/src/foundation/functoriality-morphisms-arrows.lagda.md +++ b/src/foundation/functoriality-morphisms-arrows.lagda.md @@ -31,7 +31,7 @@ open import foundation.precomposition-functions open import foundation.pullback-cones open import foundation.pullbacks open import foundation.retractions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.sections open import foundation.standard-pullbacks open import foundation.universe-levels diff --git a/src/foundation/path-cosplit-maps.lagda.md b/src/foundation/path-cosplit-maps.lagda.md index dbb0e02effc..3d9de9f6984 100644 --- a/src/foundation/path-cosplit-maps.lagda.md +++ b/src/foundation/path-cosplit-maps.lagda.md @@ -38,7 +38,7 @@ open import foundation.postcomposition-functions open import foundation.precomposition-functions open import foundation.propositional-truncations open import foundation.retractions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.truncated-maps open import foundation.truncation-levels open import foundation.universe-levels @@ -337,7 +337,7 @@ is-path-cosplit-is-path-cosplit-on-domain-hom-arrow : is-path-cosplit k f is-path-cosplit-is-path-cosplit-on-domain-hom-arrow {k = neg-two-𝕋} f g α I = - retraction-retract-map-retraction' f g + retraction-retract-arrow-retraction' f g ( map-domain-hom-arrow f g α , I) ( map-codomain-hom-arrow f g α) ( coh-hom-arrow f g α) diff --git a/src/foundation/retracts-of-maps.lagda.md b/src/foundation/retracts-of-arrows.lagda.md similarity index 55% rename from src/foundation/retracts-of-maps.lagda.md rename to src/foundation/retracts-of-arrows.lagda.md index bf904c18bc4..a38114bd862 100644 --- a/src/foundation/retracts-of-maps.lagda.md +++ b/src/foundation/retracts-of-arrows.lagda.md @@ -1,7 +1,7 @@ -# Retracts of maps +# Retracts of arrows ```agda -module foundation.retracts-of-maps where +module foundation.retracts-of-arrows where ```
Imports @@ -38,10 +38,12 @@ open import foundation-core.sections ## Idea -A map `f : A → B` is said to be a **retract** of a map `g : X → Y` if it is a -retract in the arrow category of types. In other words, `f` is a retract of `g` -if there are [morphisms of arrows](foundation.morphisms-arrows.md) `i : f → g` -and `r : g → f` equipped with a homotopy of morphisms of arrows `r ∘ i ~ id`. +A map `f : A → B` is said to be a +{{#concept "retract" Disambiguation="of arrows of types" Agda=retract-arrow}} of +a map `g : X → Y` if it is a retract in the arrow category of types. In other +words, `f` is a retract of `g` if there are +[morphisms of arrows](foundation.morphisms-arrows.md) `i : f → g` and +`r : g → f` equipped with a homotopy of morphisms of arrows `r ∘ i ~ id`. More explicitly, it consists of [retracts](foundation-core.retractions.md) `A` of `X` and `B` of `Y` that fit into a commutative diagram @@ -142,11 +144,11 @@ module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} where - retract-map : (g : X → Y) (f : A → B) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - retract-map g f = Σ (hom-arrow f g) (retraction-hom-arrow f g) + retract-arrow : (g : X → Y) (f : A → B) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + retract-arrow g f = Σ (hom-arrow f g) (retraction-hom-arrow f g) ``` -### The higher coherence in the definition of retracts of maps +### The higher coherence in the definition of retracts of arrows ```agda module _ @@ -159,12 +161,12 @@ module _ ( map-codomain-hom-arrow g f r)) where - coherence-retract-map : UU (l1 ⊔ l2) - coherence-retract-map = + coherence-retract-arrow : UU (l1 ⊔ l2) + coherence-retract-arrow = coherence-htpy-hom-arrow f f (comp-hom-arrow f g f r i) id-hom-arrow H H' ``` -### The binary relation `f g ↦ f retract-of-map g` asserting that `f` is a retract of the map `g` +### The binary relation `f g ↦ f retract-of-arrow g` asserting that `f` is a retract of the map `g` ```agda module _ @@ -175,117 +177,117 @@ module _ infix 6 _retract-of-map_ _retract-of-map_ : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - _retract-of-map_ = retract-map g f + _retract-of-map_ = retract-arrow g f module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (R : f retract-of-map g) + (f : A → B) (g : X → Y) (R : f retract-of-arrow g) where - inclusion-retract-map : hom-arrow f g - inclusion-retract-map = pr1 R + inclusion-retract-arrow : hom-arrow f g + inclusion-retract-arrow = pr1 R - map-domain-inclusion-retract-map : A → X - map-domain-inclusion-retract-map = - map-domain-hom-arrow f g inclusion-retract-map + map-domain-inclusion-retract-arrow : A → X + map-domain-inclusion-retract-arrow = + map-domain-hom-arrow f g inclusion-retract-arrow - map-codomain-inclusion-retract-map : B → Y - map-codomain-inclusion-retract-map = - map-codomain-hom-arrow f g inclusion-retract-map + map-codomain-inclusion-retract-arrow : B → Y + map-codomain-inclusion-retract-arrow = + map-codomain-hom-arrow f g inclusion-retract-arrow - coh-inclusion-retract-map : + coh-inclusion-retract-arrow : coherence-square-maps - ( map-domain-inclusion-retract-map) + ( map-domain-inclusion-retract-arrow) ( f) ( g) - ( map-codomain-inclusion-retract-map) - coh-inclusion-retract-map = - coh-hom-arrow f g inclusion-retract-map + ( map-codomain-inclusion-retract-arrow) + coh-inclusion-retract-arrow = + coh-hom-arrow f g inclusion-retract-arrow - retraction-retract-map : retraction-hom-arrow f g inclusion-retract-map - retraction-retract-map = pr2 R + retraction-retract-arrow : retraction-hom-arrow f g inclusion-retract-arrow + retraction-retract-arrow = pr2 R - hom-retraction-retract-map : hom-arrow g f - hom-retraction-retract-map = - hom-retraction-hom-arrow f g inclusion-retract-map retraction-retract-map + hom-retraction-retract-arrow : hom-arrow g f + hom-retraction-retract-arrow = + hom-retraction-hom-arrow f g inclusion-retract-arrow retraction-retract-arrow - map-domain-hom-retraction-retract-map : X → A - map-domain-hom-retraction-retract-map = - map-domain-hom-arrow g f hom-retraction-retract-map + map-domain-hom-retraction-retract-arrow : X → A + map-domain-hom-retraction-retract-arrow = + map-domain-hom-arrow g f hom-retraction-retract-arrow - map-codomain-hom-retraction-retract-map : Y → B - map-codomain-hom-retraction-retract-map = - map-codomain-hom-arrow g f hom-retraction-retract-map + map-codomain-hom-retraction-retract-arrow : Y → B + map-codomain-hom-retraction-retract-arrow = + map-codomain-hom-arrow g f hom-retraction-retract-arrow - coh-hom-retraction-retract-map : + coh-hom-retraction-retract-arrow : coherence-square-maps - ( map-domain-hom-retraction-retract-map) + ( map-domain-hom-retraction-retract-arrow) ( g) ( f) - ( map-codomain-hom-retraction-retract-map) - coh-hom-retraction-retract-map = - coh-hom-arrow g f hom-retraction-retract-map + ( map-codomain-hom-retraction-retract-arrow) + coh-hom-retraction-retract-arrow = + coh-hom-arrow g f hom-retraction-retract-arrow - is-retraction-hom-retraction-retract-map : - is-retraction-hom-arrow f g inclusion-retract-map hom-retraction-retract-map - is-retraction-hom-retraction-retract-map = + is-retraction-hom-retraction-retract-arrow : + is-retraction-hom-arrow f g inclusion-retract-arrow hom-retraction-retract-arrow + is-retraction-hom-retraction-retract-arrow = is-retraction-hom-retraction-hom-arrow f g - ( inclusion-retract-map) - ( retraction-retract-map) + ( inclusion-retract-arrow) + ( retraction-retract-arrow) - is-retraction-map-domain-hom-retraction-retract-map : + is-retraction-map-domain-hom-retraction-retract-arrow : is-retraction - ( map-domain-inclusion-retract-map) - ( map-domain-hom-retraction-retract-map) - is-retraction-map-domain-hom-retraction-retract-map = + ( map-domain-inclusion-retract-arrow) + ( map-domain-hom-retraction-retract-arrow) + is-retraction-map-domain-hom-retraction-retract-arrow = htpy-domain-htpy-hom-arrow f f - ( comp-hom-arrow f g f hom-retraction-retract-map inclusion-retract-map) + ( comp-hom-arrow f g f hom-retraction-retract-arrow inclusion-retract-arrow) ( id-hom-arrow) - ( is-retraction-hom-retraction-retract-map) + ( is-retraction-hom-retraction-retract-arrow) - retract-domain-retract-map : + retract-domain-retract-arrow : A retract-of X - pr1 retract-domain-retract-map = - map-domain-inclusion-retract-map - pr1 (pr2 retract-domain-retract-map) = - map-domain-hom-retraction-retract-map - pr2 (pr2 retract-domain-retract-map) = - is-retraction-map-domain-hom-retraction-retract-map - - is-retraction-map-codomain-hom-retraction-retract-map : + pr1 retract-domain-retract-arrow = + map-domain-inclusion-retract-arrow + pr1 (pr2 retract-domain-retract-arrow) = + map-domain-hom-retraction-retract-arrow + pr2 (pr2 retract-domain-retract-arrow) = + is-retraction-map-domain-hom-retraction-retract-arrow + + is-retraction-map-codomain-hom-retraction-retract-arrow : is-retraction - ( map-codomain-inclusion-retract-map) - ( map-codomain-hom-retraction-retract-map) - is-retraction-map-codomain-hom-retraction-retract-map = + ( map-codomain-inclusion-retract-arrow) + ( map-codomain-hom-retraction-retract-arrow) + is-retraction-map-codomain-hom-retraction-retract-arrow = htpy-codomain-htpy-hom-arrow f f - ( comp-hom-arrow f g f hom-retraction-retract-map inclusion-retract-map) + ( comp-hom-arrow f g f hom-retraction-retract-arrow inclusion-retract-arrow) ( id-hom-arrow) - ( is-retraction-hom-retraction-retract-map) - - retract-codomain-retract-map : B retract-of Y - pr1 retract-codomain-retract-map = - map-codomain-inclusion-retract-map - pr1 (pr2 retract-codomain-retract-map) = - map-codomain-hom-retraction-retract-map - pr2 (pr2 retract-codomain-retract-map) = - is-retraction-map-codomain-hom-retraction-retract-map - - coh-retract-map : - coherence-retract-map f g - ( inclusion-retract-map) - ( hom-retraction-retract-map) - ( is-retraction-map-domain-hom-retraction-retract-map) - ( is-retraction-map-codomain-hom-retraction-retract-map) - coh-retract-map = + ( is-retraction-hom-retraction-retract-arrow) + + retract-codomain-retract-arrow : B retract-of Y + pr1 retract-codomain-retract-arrow = + map-codomain-inclusion-retract-arrow + pr1 (pr2 retract-codomain-retract-arrow) = + map-codomain-hom-retraction-retract-arrow + pr2 (pr2 retract-codomain-retract-arrow) = + is-retraction-map-codomain-hom-retraction-retract-arrow + + coh-retract-arrow : + coherence-retract-arrow f g + ( inclusion-retract-arrow) + ( hom-retraction-retract-arrow) + ( is-retraction-map-domain-hom-retraction-retract-arrow) + ( is-retraction-map-codomain-hom-retraction-retract-arrow) + coh-retract-arrow = coh-htpy-hom-arrow f f - ( comp-hom-arrow f g f hom-retraction-retract-map inclusion-retract-map) + ( comp-hom-arrow f g f hom-retraction-retract-arrow inclusion-retract-arrow) ( id-hom-arrow) - ( is-retraction-hom-retraction-retract-map) + ( is-retraction-hom-retraction-retract-arrow) ``` ## Properties -### Retracts of maps with sections have sections +### Retracts of arrows with sections have sections In fact, we only need the following data to show this: @@ -323,8 +325,8 @@ module _ (s : section g) where - section-retract-map-section' : section f - section-retract-map-section' = + section-retract-arrow-section' : section f + section-retract-arrow-section' = section-right-map-triangle ( map-retraction-retract R₁ ∘ g) ( f) @@ -334,18 +336,18 @@ module _ module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (R : f retract-of-map g) + (f : A → B) (g : X → Y) (R : f retract-of-arrow g) where - section-retract-map-section : section g → section f - section-retract-map-section = - section-retract-map-section' f g - ( map-domain-hom-retraction-retract-map f g R) - ( retract-codomain-retract-map f g R) - ( coh-hom-retraction-retract-map f g R) + section-retract-arrow-section : section g → section f + section-retract-arrow-section = + section-retract-arrow-section' f g + ( map-domain-hom-retraction-retract-arrow f g R) + ( retract-codomain-retract-arrow f g R) + ( coh-hom-retraction-retract-arrow f g R) ``` -### Retracts of maps with retractions have retractions +### Retracts of arrows with retractions have retractions In fact, we only need the following data to show this: @@ -382,8 +384,8 @@ module _ (s : retraction g) where - retraction-retract-map-retraction' : retraction f - retraction-retract-map-retraction' = + retraction-retract-arrow-retraction' : retraction f + retraction-retract-arrow-retraction' = retraction-top-map-triangle' ( g ∘ inclusion-retract R₀) ( i₁) @@ -393,18 +395,18 @@ module _ module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (R : f retract-of-map g) + (f : A → B) (g : X → Y) (R : f retract-of-arrow g) where - retraction-retract-map-retraction : retraction g → retraction f - retraction-retract-map-retraction = - retraction-retract-map-retraction' f g - ( retract-domain-retract-map f g R) - ( map-codomain-inclusion-retract-map f g R) - ( coh-inclusion-retract-map f g R) + retraction-retract-arrow-retraction : retraction g → retraction f + retraction-retract-arrow-retraction = + retraction-retract-arrow-retraction' f g + ( retract-domain-retract-arrow f g R) + ( map-codomain-inclusion-retract-arrow f g R) + ( coh-inclusion-retract-arrow f g R) ``` -### Equivalences are closed under retracts of maps +### Equivalences are closed under retracts of arrows We may observe that the higher coherence of a retract of maps is not needed. @@ -422,15 +424,15 @@ module _ (H : is-equiv g) where - is-equiv-retract-map-is-equiv' : is-equiv f - pr1 is-equiv-retract-map-is-equiv' = - section-retract-map-section' f g + is-equiv-retract-arrow-is-equiv' : is-equiv f + pr1 is-equiv-retract-arrow-is-equiv' = + section-retract-arrow-section' f g ( map-retraction-retract R₀) ( R₁) ( r) ( section-is-equiv H) - pr2 is-equiv-retract-map-is-equiv' = - retraction-retract-map-retraction' f g + pr2 is-equiv-retract-arrow-is-equiv' = + retraction-retract-arrow-retraction' f g ( R₀) ( inclusion-retract R₁) ( i) @@ -438,20 +440,20 @@ module _ module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (R : f retract-of-map g) (H : is-equiv g) + (f : A → B) (g : X → Y) (R : f retract-of-arrow g) (H : is-equiv g) where - section-retract-map-is-equiv : section f - section-retract-map-is-equiv = - section-retract-map-section f g R (section-is-equiv H) + section-retract-arrow-is-equiv : section f + section-retract-arrow-is-equiv = + section-retract-arrow-section f g R (section-is-equiv H) - retraction-retract-map-is-equiv : retraction f - retraction-retract-map-is-equiv = - retraction-retract-map-retraction f g R (retraction-is-equiv H) + retraction-retract-arrow-is-equiv : retraction f + retraction-retract-arrow-is-equiv = + retraction-retract-arrow-retraction f g R (retraction-is-equiv H) - is-equiv-retract-map-is-equiv : is-equiv f - pr1 is-equiv-retract-map-is-equiv = section-retract-map-is-equiv - pr2 is-equiv-retract-map-is-equiv = retraction-retract-map-is-equiv + is-equiv-retract-arrow-is-equiv : is-equiv f + pr1 is-equiv-retract-arrow-is-equiv = section-retract-arrow-is-equiv + pr2 is-equiv-retract-arrow-is-equiv = retraction-retract-arrow-is-equiv ``` ### If `f` is a retract of `g`, then the fiber inclusions of `f` are retracts of the fiber inclusions of `g` @@ -506,38 +508,38 @@ involved take a lot of arguments and therefore the code is somewhat lengthy. ```agda module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (R : f retract-of-map g) (b : B) + (f : A → B) (g : X → Y) (R : f retract-of-arrow g) (b : B) where - inclusion-retract-map-inclusion-fiber-retract-map : + inclusion-retract-arrow-inclusion-fiber-retract-arrow : hom-arrow ( inclusion-fiber f {b}) - ( inclusion-fiber g {map-codomain-inclusion-retract-map f g R b}) - inclusion-retract-map-inclusion-fiber-retract-map = - hom-arrow-fiber f g (inclusion-retract-map f g R) b + ( inclusion-fiber g {map-codomain-inclusion-retract-arrow f g R b}) + inclusion-retract-arrow-inclusion-fiber-retract-arrow = + hom-arrow-fiber f g (inclusion-retract-arrow f g R) b - hom-retraction-retract-map-inclusion-fiber-retract-map : + hom-retraction-retract-arrow-inclusion-fiber-retract-arrow : hom-arrow - ( inclusion-fiber g {map-codomain-inclusion-retract-map f g R b}) + ( inclusion-fiber g {map-codomain-inclusion-retract-arrow f g R b}) ( inclusion-fiber f {b}) - hom-retraction-retract-map-inclusion-fiber-retract-map = + hom-retraction-retract-arrow-inclusion-fiber-retract-arrow = comp-hom-arrow ( inclusion-fiber g) ( inclusion-fiber f) ( inclusion-fiber f) ( tr-hom-arrow-inclusion-fiber f - ( is-retraction-map-codomain-hom-retraction-retract-map f g R b)) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R b)) ( hom-arrow-fiber g f - ( hom-retraction-retract-map f g R) - ( map-codomain-inclusion-retract-map f g R b)) + ( hom-retraction-retract-arrow f g R) + ( map-codomain-inclusion-retract-arrow f g R b)) - is-retraction-hom-retraction-retract-map-inclusion-fiber-retract-map : + is-retraction-hom-retraction-retract-arrow-inclusion-fiber-retract-arrow : is-retraction-hom-arrow ( inclusion-fiber f) ( inclusion-fiber g) - ( inclusion-retract-map-inclusion-fiber-retract-map) - ( hom-retraction-retract-map-inclusion-fiber-retract-map) - is-retraction-hom-retraction-retract-map-inclusion-fiber-retract-map = + ( inclusion-retract-arrow-inclusion-fiber-retract-arrow) + ( hom-retraction-retract-arrow-inclusion-fiber-retract-arrow) + is-retraction-hom-retraction-retract-arrow-inclusion-fiber-retract-arrow = concat-htpy-hom-arrow ( inclusion-fiber f) ( inclusion-fiber f) @@ -550,25 +552,25 @@ module _ ( inclusion-fiber f) ( inclusion-fiber f) ( tr-hom-arrow-inclusion-fiber f - ( is-retraction-map-codomain-hom-retraction-retract-map f g R b)) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R b)) ( hom-arrow-fiber g f - ( hom-retraction-retract-map f g R) - ( map-codomain-inclusion-retract-map f g R b))) - ( inclusion-retract-map-inclusion-fiber-retract-map)) + ( hom-retraction-retract-arrow f g R) + ( map-codomain-inclusion-retract-arrow f g R b))) + ( inclusion-retract-arrow-inclusion-fiber-retract-arrow)) ( comp-hom-arrow ( inclusion-fiber f) ( inclusion-fiber f) ( inclusion-fiber f) ( tr-hom-arrow-inclusion-fiber f - ( is-retraction-map-codomain-hom-retraction-retract-map f g R b)) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R b)) ( comp-hom-arrow ( inclusion-fiber f) ( inclusion-fiber g) ( inclusion-fiber f) ( hom-arrow-fiber g f - ( hom-retraction-retract-map f g R) - ( map-codomain-inclusion-retract-map f g R b)) - ( inclusion-retract-map-inclusion-fiber-retract-map))) + ( hom-retraction-retract-arrow f g R) + ( map-codomain-inclusion-retract-arrow f g R b)) + ( inclusion-retract-arrow-inclusion-fiber-retract-arrow))) ( id-hom-arrow) ( inv-assoc-comp-hom-arrow ( inclusion-fiber f) @@ -576,11 +578,11 @@ module _ ( inclusion-fiber f) ( inclusion-fiber f) ( tr-hom-arrow-inclusion-fiber f - ( is-retraction-map-codomain-hom-retraction-retract-map f g R b)) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R b)) ( hom-arrow-fiber g f - ( hom-retraction-retract-map f g R) - ( map-codomain-inclusion-retract-map f g R b)) - ( inclusion-retract-map-inclusion-fiber-retract-map)) + ( hom-retraction-retract-arrow f g R) + ( map-codomain-inclusion-retract-arrow f g R b)) + ( inclusion-retract-arrow-inclusion-fiber-retract-arrow)) ( concat-htpy-hom-arrow ( inclusion-fiber f) ( inclusion-fiber f) @@ -589,25 +591,25 @@ module _ ( inclusion-fiber f) ( inclusion-fiber f) ( tr-hom-arrow-inclusion-fiber f - ( is-retraction-map-codomain-hom-retraction-retract-map f g R b)) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R b)) ( comp-hom-arrow ( inclusion-fiber f) ( inclusion-fiber g) ( inclusion-fiber f) ( hom-arrow-fiber g f - ( hom-retraction-retract-map f g R) - ( map-codomain-inclusion-retract-map f g R b)) - ( inclusion-retract-map-inclusion-fiber-retract-map))) + ( hom-retraction-retract-arrow f g R) + ( map-codomain-inclusion-retract-arrow f g R b)) + ( inclusion-retract-arrow-inclusion-fiber-retract-arrow))) ( comp-hom-arrow ( inclusion-fiber f) ( inclusion-fiber f) ( inclusion-fiber f) ( tr-hom-arrow-inclusion-fiber f - ( is-retraction-map-codomain-hom-retraction-retract-map f g R b)) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R b)) ( hom-arrow-fiber f f ( comp-hom-arrow f g f - ( hom-retraction-retract-map f g R) - ( inclusion-retract-map f g R)) + ( hom-retraction-retract-arrow f g R) + ( inclusion-retract-arrow f g R)) ( b))) ( id-hom-arrow) ( left-whisker-comp-hom-arrow @@ -615,39 +617,39 @@ module _ ( inclusion-fiber f) ( inclusion-fiber f) ( tr-hom-arrow-inclusion-fiber f - ( is-retraction-map-codomain-hom-retraction-retract-map f g R b)) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R b)) ( comp-hom-arrow ( inclusion-fiber f) ( inclusion-fiber g) ( inclusion-fiber f) ( hom-arrow-fiber g f - ( hom-retraction-retract-map f g R) - ( map-codomain-inclusion-retract-map f g R b)) - ( hom-arrow-fiber f g (inclusion-retract-map f g R) b)) + ( hom-retraction-retract-arrow f g R) + ( map-codomain-inclusion-retract-arrow f g R b)) + ( hom-arrow-fiber f g (inclusion-retract-arrow f g R) b)) ( hom-arrow-fiber f f ( comp-hom-arrow f g f - ( hom-retraction-retract-map f g R) - ( inclusion-retract-map f g R)) + ( hom-retraction-retract-arrow f g R) + ( inclusion-retract-arrow f g R)) ( b)) ( inv-htpy-hom-arrow ( inclusion-fiber f) ( inclusion-fiber f) ( hom-arrow-fiber f f ( comp-hom-arrow f g f - ( hom-retraction-retract-map f g R) - ( inclusion-retract-map f g R)) + ( hom-retraction-retract-arrow f g R) + ( inclusion-retract-arrow f g R)) ( b)) ( comp-hom-arrow ( inclusion-fiber f) ( inclusion-fiber g) ( inclusion-fiber f) ( hom-arrow-fiber g f - ( hom-retraction-retract-map f g R) - ( map-codomain-inclusion-retract-map f g R b)) - ( hom-arrow-fiber f g (inclusion-retract-map f g R) b)) + ( hom-retraction-retract-arrow f g R) + ( map-codomain-inclusion-retract-arrow f g R b)) + ( hom-arrow-fiber f g (inclusion-retract-arrow f g R) b)) ( preserves-comp-hom-arrow-fiber f g f - ( hom-retraction-retract-map f g R) - ( inclusion-retract-map f g R) + ( hom-retraction-retract-arrow f g R) + ( inclusion-retract-arrow f g R) ( b)))) ( concat-htpy-hom-arrow ( inclusion-fiber f) @@ -657,33 +659,33 @@ module _ ( inclusion-fiber f) ( inclusion-fiber f) ( tr-hom-arrow-inclusion-fiber f - ( is-retraction-map-codomain-hom-retraction-retract-map f g R b)) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R b)) ( hom-arrow-fiber f f ( comp-hom-arrow f g f - ( hom-retraction-retract-map f g R) - ( inclusion-retract-map f g R)) + ( hom-retraction-retract-arrow f g R) + ( inclusion-retract-arrow f g R)) ( b))) ( hom-arrow-fiber f f id-hom-arrow b) ( id-hom-arrow) ( htpy-hom-arrow-fiber f f ( comp-hom-arrow f g f - ( hom-retraction-retract-map f g R) - ( inclusion-retract-map f g R)) + ( hom-retraction-retract-arrow f g R) + ( inclusion-retract-arrow f g R)) ( id-hom-arrow) - ( is-retraction-hom-retraction-retract-map f g R) + ( is-retraction-hom-retraction-retract-arrow f g R) ( b)) ( preserves-id-hom-arrow-fiber f b))) - retract-map-inclusion-fiber-retract-map : - retract-map - ( inclusion-fiber g {map-codomain-inclusion-retract-map f g R b}) + retract-arrow-inclusion-fiber-retract-arrow : + retract-arrow + ( inclusion-fiber g {map-codomain-inclusion-retract-arrow f g R b}) ( inclusion-fiber f {b}) - pr1 retract-map-inclusion-fiber-retract-map = - inclusion-retract-map-inclusion-fiber-retract-map - pr1 (pr2 retract-map-inclusion-fiber-retract-map) = - hom-retraction-retract-map-inclusion-fiber-retract-map - pr2 (pr2 retract-map-inclusion-fiber-retract-map) = - is-retraction-hom-retraction-retract-map-inclusion-fiber-retract-map + pr1 retract-arrow-inclusion-fiber-retract-arrow = + inclusion-retract-arrow-inclusion-fiber-retract-arrow + pr1 (pr2 retract-arrow-inclusion-fiber-retract-arrow) = + hom-retraction-retract-arrow-inclusion-fiber-retract-arrow + pr2 (pr2 retract-arrow-inclusion-fiber-retract-arrow) = + is-retraction-hom-retraction-retract-arrow-inclusion-fiber-retract-arrow ``` ### If `f` is a retract of `g`, then the fibers of `f` are retracts of the fibers of `g` @@ -691,18 +693,18 @@ module _ ```agda module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (R : f retract-of-map g) (b : B) + (f : A → B) (g : X → Y) (R : f retract-of-arrow g) (b : B) where - retract-fiber-retract-map : + retract-fiber-retract-arrow : retract - ( fiber g (map-codomain-inclusion-retract-map f g R b)) + ( fiber g (map-codomain-inclusion-retract-arrow f g R b)) ( fiber f b) - retract-fiber-retract-map = - retract-domain-retract-map + retract-fiber-retract-arrow = + retract-domain-retract-arrow ( inclusion-fiber f) ( inclusion-fiber g) - ( retract-map-inclusion-fiber-retract-map f g R b) + ( retract-arrow-inclusion-fiber-retract-arrow f g R b) ``` ### If `f` is a retract of `g`, then `- ∘ f` is a retract of `- ∘ g` @@ -710,99 +712,99 @@ module _ ```agda module _ {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (R : f retract-of-map g) (S : UU l5) + (f : A → B) (g : X → Y) (R : f retract-of-arrow g) (S : UU l5) where - inclusion-precomp-retract-map : hom-arrow (precomp f S) (precomp g S) - inclusion-precomp-retract-map = - precomp-hom-arrow g f (hom-retraction-retract-map f g R) S + inclusion-precomp-retract-arrow : hom-arrow (precomp f S) (precomp g S) + inclusion-precomp-retract-arrow = + precomp-hom-arrow g f (hom-retraction-retract-arrow f g R) S - hom-retraction-precomp-retract-map : hom-arrow (precomp g S) (precomp f S) - hom-retraction-precomp-retract-map = - precomp-hom-arrow f g (inclusion-retract-map f g R) S + hom-retraction-precomp-retract-arrow : hom-arrow (precomp g S) (precomp f S) + hom-retraction-precomp-retract-arrow = + precomp-hom-arrow f g (inclusion-retract-arrow f g R) S - is-retraction-map-domain-precomp-retract-map : + is-retraction-map-domain-precomp-retract-arrow : is-retraction ( map-domain-hom-arrow ( precomp f S) ( precomp g S) - ( inclusion-precomp-retract-map)) + ( inclusion-precomp-retract-arrow)) ( map-domain-hom-arrow ( precomp g S) ( precomp f S) - ( hom-retraction-precomp-retract-map)) - is-retraction-map-domain-precomp-retract-map = - htpy-precomp (is-retraction-map-codomain-hom-retraction-retract-map f g R) S + ( hom-retraction-precomp-retract-arrow)) + is-retraction-map-domain-precomp-retract-arrow = + htpy-precomp (is-retraction-map-codomain-hom-retraction-retract-arrow f g R) S - is-retraction-map-codomain-precomp-retract-map : + is-retraction-map-codomain-precomp-retract-arrow : is-retraction ( map-codomain-hom-arrow ( precomp f S) ( precomp g S) - ( inclusion-precomp-retract-map)) + ( inclusion-precomp-retract-arrow)) ( map-codomain-hom-arrow ( precomp g S) ( precomp f S) - ( hom-retraction-precomp-retract-map)) - is-retraction-map-codomain-precomp-retract-map = - htpy-precomp (is-retraction-map-domain-hom-retraction-retract-map f g R) S + ( hom-retraction-precomp-retract-arrow)) + is-retraction-map-codomain-precomp-retract-arrow = + htpy-precomp (is-retraction-map-domain-hom-retraction-retract-arrow f g R) S - coh-retract-precomp-retract-map : - coherence-retract-map + coh-retract-precomp-retract-arrow : + coherence-retract-arrow ( precomp f S) ( precomp g S) - ( inclusion-precomp-retract-map) - ( hom-retraction-precomp-retract-map) - ( is-retraction-map-domain-precomp-retract-map) - ( is-retraction-map-codomain-precomp-retract-map) - coh-retract-precomp-retract-map = + ( inclusion-precomp-retract-arrow) + ( hom-retraction-precomp-retract-arrow) + ( is-retraction-map-domain-precomp-retract-arrow) + ( is-retraction-map-codomain-precomp-retract-arrow) + coh-retract-precomp-retract-arrow = ( precomp-vertical-coherence-prism-inv-triangles-maps ( id) - ( map-domain-hom-retraction-retract-map f g R) - ( map-domain-inclusion-retract-map f g R) + ( map-domain-hom-retraction-retract-arrow f g R) + ( map-domain-inclusion-retract-arrow f g R) ( id) - ( map-codomain-hom-retraction-retract-map f g R) - ( map-codomain-inclusion-retract-map f g R) + ( map-codomain-hom-retraction-retract-arrow f g R) + ( map-codomain-inclusion-retract-arrow f g R) ( f) ( g) ( f) - ( is-retraction-map-domain-hom-retraction-retract-map f g R) + ( is-retraction-map-domain-hom-retraction-retract-arrow f g R) ( refl-htpy) - ( coh-hom-retraction-retract-map f g R) - ( coh-inclusion-retract-map f g R) - ( is-retraction-map-codomain-hom-retraction-retract-map f g R) - ( coh-retract-map f g R) + ( coh-hom-retraction-retract-arrow f g R) + ( coh-inclusion-retract-arrow f g R) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R) + ( coh-retract-arrow f g R) ( S)) ∙h ( ap-concat-htpy - ( is-retraction-map-codomain-precomp-retract-map ·r precomp f S) + ( is-retraction-map-codomain-precomp-retract-arrow ·r precomp f S) ( λ x → ap inv (eq-htpy-refl-htpy (precomp f S x)))) - is-retraction-hom-retraction-precomp-retract-map : + is-retraction-hom-retraction-precomp-retract-arrow : is-retraction-hom-arrow ( precomp f S) ( precomp g S) - ( inclusion-precomp-retract-map) - ( hom-retraction-precomp-retract-map) - pr1 is-retraction-hom-retraction-precomp-retract-map = - is-retraction-map-domain-precomp-retract-map - pr1 (pr2 is-retraction-hom-retraction-precomp-retract-map) = - is-retraction-map-codomain-precomp-retract-map - pr2 (pr2 is-retraction-hom-retraction-precomp-retract-map) = - coh-retract-precomp-retract-map - - retraction-precomp-retract-map : + ( inclusion-precomp-retract-arrow) + ( hom-retraction-precomp-retract-arrow) + pr1 is-retraction-hom-retraction-precomp-retract-arrow = + is-retraction-map-domain-precomp-retract-arrow + pr1 (pr2 is-retraction-hom-retraction-precomp-retract-arrow) = + is-retraction-map-codomain-precomp-retract-arrow + pr2 (pr2 is-retraction-hom-retraction-precomp-retract-arrow) = + coh-retract-precomp-retract-arrow + + retraction-precomp-retract-arrow : retraction-hom-arrow ( precomp f S) ( precomp g S) - ( inclusion-precomp-retract-map) - pr1 retraction-precomp-retract-map = - hom-retraction-precomp-retract-map - pr2 retraction-precomp-retract-map = - is-retraction-hom-retraction-precomp-retract-map - - retract-map-precomp-retract-map : (precomp f S) retract-of-map (precomp g S) - pr1 retract-map-precomp-retract-map = inclusion-precomp-retract-map - pr2 retract-map-precomp-retract-map = retraction-precomp-retract-map + ( inclusion-precomp-retract-arrow) + pr1 retraction-precomp-retract-arrow = + hom-retraction-precomp-retract-arrow + pr2 retraction-precomp-retract-arrow = + is-retraction-hom-retraction-precomp-retract-arrow + + retract-arrow-precomp-retract-arrow : (precomp f S) retract-of-arrow (precomp g S) + pr1 retract-arrow-precomp-retract-arrow = inclusion-precomp-retract-arrow + pr2 retract-arrow-precomp-retract-arrow = retraction-precomp-retract-arrow ``` ### If `f` is a retract of `g`, then `f ∘ -` is a retract of `g ∘ -` @@ -810,101 +812,101 @@ module _ ```agda module _ {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (R : f retract-of-map g) (S : UU l5) + (f : A → B) (g : X → Y) (R : f retract-of-arrow g) (S : UU l5) where - inclusion-postcomp-retract-map : hom-arrow (postcomp S f) (postcomp S g) - inclusion-postcomp-retract-map = - postcomp-hom-arrow f g (inclusion-retract-map f g R) S + inclusion-postcomp-retract-arrow : hom-arrow (postcomp S f) (postcomp S g) + inclusion-postcomp-retract-arrow = + postcomp-hom-arrow f g (inclusion-retract-arrow f g R) S - hom-retraction-postcomp-retract-map : hom-arrow (postcomp S g) (postcomp S f) - hom-retraction-postcomp-retract-map = - postcomp-hom-arrow g f (hom-retraction-retract-map f g R) S + hom-retraction-postcomp-retract-arrow : hom-arrow (postcomp S g) (postcomp S f) + hom-retraction-postcomp-retract-arrow = + postcomp-hom-arrow g f (hom-retraction-retract-arrow f g R) S - is-retraction-map-domain-postcomp-retract-map : + is-retraction-map-domain-postcomp-retract-arrow : is-retraction ( map-domain-hom-arrow ( postcomp S f) ( postcomp S g) - ( inclusion-postcomp-retract-map)) + ( inclusion-postcomp-retract-arrow)) ( map-domain-hom-arrow ( postcomp S g) ( postcomp S f) - ( hom-retraction-postcomp-retract-map)) - is-retraction-map-domain-postcomp-retract-map = - htpy-postcomp S (is-retraction-map-domain-hom-retraction-retract-map f g R) + ( hom-retraction-postcomp-retract-arrow)) + is-retraction-map-domain-postcomp-retract-arrow = + htpy-postcomp S (is-retraction-map-domain-hom-retraction-retract-arrow f g R) - is-retraction-map-codomain-postcomp-retract-map : + is-retraction-map-codomain-postcomp-retract-arrow : is-retraction ( map-codomain-hom-arrow ( postcomp S f) ( postcomp S g) - ( inclusion-postcomp-retract-map)) + ( inclusion-postcomp-retract-arrow)) ( map-codomain-hom-arrow ( postcomp S g) ( postcomp S f) - ( hom-retraction-postcomp-retract-map)) - is-retraction-map-codomain-postcomp-retract-map = + ( hom-retraction-postcomp-retract-arrow)) + is-retraction-map-codomain-postcomp-retract-arrow = htpy-postcomp S - ( is-retraction-map-codomain-hom-retraction-retract-map f g R) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R) - coh-retract-postcomp-retract-map : - coherence-retract-map + coh-retract-postcomp-retract-arrow : + coherence-retract-arrow ( postcomp S f) ( postcomp S g) - ( inclusion-postcomp-retract-map) - ( hom-retraction-postcomp-retract-map) - ( is-retraction-map-domain-postcomp-retract-map) - ( is-retraction-map-codomain-postcomp-retract-map) - coh-retract-postcomp-retract-map = + ( inclusion-postcomp-retract-arrow) + ( hom-retraction-postcomp-retract-arrow) + ( is-retraction-map-domain-postcomp-retract-arrow) + ( is-retraction-map-codomain-postcomp-retract-arrow) + coh-retract-postcomp-retract-arrow = ( postcomp-vertical-coherence-prism-inv-triangles-maps ( id) - ( map-domain-hom-retraction-retract-map f g R) - ( map-domain-inclusion-retract-map f g R) + ( map-domain-hom-retraction-retract-arrow f g R) + ( map-domain-inclusion-retract-arrow f g R) ( id) - ( map-codomain-hom-retraction-retract-map f g R) - ( map-codomain-inclusion-retract-map f g R) + ( map-codomain-hom-retraction-retract-arrow f g R) + ( map-codomain-inclusion-retract-arrow f g R) ( f) ( g) ( f) - ( is-retraction-map-domain-hom-retraction-retract-map f g R) + ( is-retraction-map-domain-hom-retraction-retract-arrow f g R) ( refl-htpy) - ( coh-hom-retraction-retract-map f g R) - ( coh-inclusion-retract-map f g R) - ( is-retraction-map-codomain-hom-retraction-retract-map f g R) - ( coh-retract-map f g R) + ( coh-hom-retraction-retract-arrow f g R) + ( coh-inclusion-retract-arrow f g R) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R) + ( coh-retract-arrow f g R) ( S)) ∙h ( ap-concat-htpy - ( is-retraction-map-codomain-postcomp-retract-map ·r postcomp S f) + ( is-retraction-map-codomain-postcomp-retract-arrow ·r postcomp S f) ( eq-htpy-refl-htpy ∘ postcomp S f)) - is-retraction-hom-retraction-postcomp-retract-map : + is-retraction-hom-retraction-postcomp-retract-arrow : is-retraction-hom-arrow ( postcomp S f) ( postcomp S g) - ( inclusion-postcomp-retract-map) - ( hom-retraction-postcomp-retract-map) - pr1 is-retraction-hom-retraction-postcomp-retract-map = - is-retraction-map-domain-postcomp-retract-map - pr1 (pr2 is-retraction-hom-retraction-postcomp-retract-map) = - is-retraction-map-codomain-postcomp-retract-map - pr2 (pr2 is-retraction-hom-retraction-postcomp-retract-map) = - coh-retract-postcomp-retract-map - - retraction-postcomp-retract-map : + ( inclusion-postcomp-retract-arrow) + ( hom-retraction-postcomp-retract-arrow) + pr1 is-retraction-hom-retraction-postcomp-retract-arrow = + is-retraction-map-domain-postcomp-retract-arrow + pr1 (pr2 is-retraction-hom-retraction-postcomp-retract-arrow) = + is-retraction-map-codomain-postcomp-retract-arrow + pr2 (pr2 is-retraction-hom-retraction-postcomp-retract-arrow) = + coh-retract-postcomp-retract-arrow + + retraction-postcomp-retract-arrow : retraction-hom-arrow ( postcomp S f) ( postcomp S g) - ( inclusion-postcomp-retract-map) - pr1 retraction-postcomp-retract-map = - hom-retraction-postcomp-retract-map - pr2 retraction-postcomp-retract-map = - is-retraction-hom-retraction-postcomp-retract-map - - retract-map-postcomp-retract-map : - (postcomp S f) retract-of-map (postcomp S g) - pr1 retract-map-postcomp-retract-map = inclusion-postcomp-retract-map - pr2 retract-map-postcomp-retract-map = retraction-postcomp-retract-map + ( inclusion-postcomp-retract-arrow) + pr1 retraction-postcomp-retract-arrow = + hom-retraction-postcomp-retract-arrow + pr2 retraction-postcomp-retract-arrow = + is-retraction-hom-retraction-postcomp-retract-arrow + + retract-arrow-postcomp-retract-arrow : + (postcomp S f) retract-of-arrow (postcomp S g) + pr1 retract-arrow-postcomp-retract-arrow = inclusion-postcomp-retract-arrow + pr2 retract-arrow-postcomp-retract-arrow = retraction-postcomp-retract-arrow ``` ### If `A` is a retract of `B` and `S` is a retract of `T` then `diagonal-exponential A S` is a retract of `diagonal-exponential B T` @@ -929,8 +931,8 @@ module _ postcomp S (map-retraction-retract R) ∘ precomp (inclusion-retract Q) B , refl-htpy) - coh-retract-map-diagonal-exponential-retract : - coherence-retract-map + coh-retract-arrow-diagonal-exponential-retract : + coherence-retract-arrow ( diagonal-exponential A S) ( diagonal-exponential B T) ( inclusion-diagonal-exponential-retract) @@ -939,7 +941,7 @@ module _ ( horizontal-concat-htpy ( htpy-postcomp S (is-retraction-map-retraction-retract R)) ( htpy-precomp (is-retraction-map-retraction-retract Q) A)) - coh-retract-map-diagonal-exponential-retract x = + coh-retract-arrow-diagonal-exponential-retract x = ( compute-eq-htpy-ap-diagonal-exponential S ( map-retraction-retract R (inclusion-retract R x)) ( x) @@ -966,11 +968,11 @@ module _ ( horizontal-concat-htpy ( htpy-postcomp S (is-retraction-map-retraction-retract R)) ( htpy-precomp (is-retraction-map-retraction-retract Q) A)) , - ( coh-retract-map-diagonal-exponential-retract)) + ( coh-retract-arrow-diagonal-exponential-retract)) - retract-map-diagonal-exponential-retract : - (diagonal-exponential A S) retract-of-map (diagonal-exponential B T) - retract-map-diagonal-exponential-retract = + retract-arrow-diagonal-exponential-retract : + (diagonal-exponential A S) retract-of-arrow (diagonal-exponential B T) + retract-arrow-diagonal-exponential-retract = ( inclusion-diagonal-exponential-retract , hom-retraction-diagonal-exponential-retract , is-retraction-hom-retraction-diagonal-exponential-retract) diff --git a/src/foundation/retracts-of-types.lagda.md b/src/foundation/retracts-of-types.lagda.md index 1de9f4bdf06..ef5b1640bfb 100644 --- a/src/foundation/retracts-of-types.lagda.md +++ b/src/foundation/retracts-of-types.lagda.md @@ -182,5 +182,5 @@ iff-retract' = inv-iff ∘ iff-retract ## See also -- [Retracts of maps](foundation.retracts-of-maps.md) +- [Retracts of arrows](foundation.retracts-of-arrows.md) - [Retractive types](structured-types.retractive-types.md) diff --git a/src/foundation/small-maps.lagda.md b/src/foundation/small-maps.lagda.md index fb58031e156..0c261c3db62 100644 --- a/src/foundation/small-maps.lagda.md +++ b/src/foundation/small-maps.lagda.md @@ -9,7 +9,7 @@ module foundation.small-maps where ```agda open import foundation.dependent-pair-types open import foundation.locally-small-types -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.split-idempotent-maps open import foundation.universe-levels @@ -74,17 +74,17 @@ module _ is-small-map-Prop = is-small-map l f , is-prop-is-small-map ``` -### Small maps are closed under retracts of maps +### Small maps are closed under retracts of arrows ```agda module _ {l1 l2 l3 l4 l : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - {f : A → B} {g : X → Y} (R : f retract-of-map g) + {f : A → B} {g : X → Y} (R : f retract-of-arrow g) where is-small-map-retract : is-small-map l g → is-small-map l f is-small-map-retract is-small-g b = is-small-retract - ( is-small-g (map-codomain-inclusion-retract-map f g R b)) - ( retract-fiber-retract-map f g R b) + ( is-small-g (map-codomain-inclusion-retract-arrow f g R b)) + ( retract-fiber-retract-arrow f g R b) ``` diff --git a/src/logic/de-morgan-embeddings.lagda.md b/src/logic/de-morgan-embeddings.lagda.md index 3391dea43b7..b5184842630 100644 --- a/src/logic/de-morgan-embeddings.lagda.md +++ b/src/logic/de-morgan-embeddings.lagda.md @@ -25,7 +25,7 @@ open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-maps open import foundation.propositions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.subtype-identity-principle open import foundation.type-arithmetic-dependent-pair-types open import foundation.unit-type @@ -603,7 +603,7 @@ module _ ( is-de-morgan-prop-map-is-de-morgan-emb F)) ``` -### De Morgan embeddings are closed under retracts of maps +### De Morgan embeddings are closed under retracts of arrows ```agda module _ @@ -611,22 +611,22 @@ module _ {f : A → B} {g : X → Y} where - is-de-morgan-prop-map-retract-map : - f retract-of-map g → + is-de-morgan-prop-map-retract-arrow : + f retract-of-arrow g → is-de-morgan-prop-map g → is-de-morgan-prop-map f - is-de-morgan-prop-map-retract-map R G x = + is-de-morgan-prop-map-retract-arrow R G x = is-de-morgan-prop-retract-of - ( retract-fiber-retract-map f g R x) - ( G (map-codomain-inclusion-retract-map f g R x)) + ( retract-fiber-retract-arrow f g R x) + ( G (map-codomain-inclusion-retract-arrow f g R x)) - is-de-morgan-emb-retract-map : - f retract-of-map g → + is-de-morgan-emb-retract-arrow : + f retract-of-arrow g → is-de-morgan-emb g → is-de-morgan-emb f - is-de-morgan-emb-retract-map R G = + is-de-morgan-emb-retract-arrow R G = is-de-morgan-emb-is-de-morgan-prop-map - ( is-de-morgan-prop-map-retract-map R + ( is-de-morgan-prop-map-retract-arrow R ( is-de-morgan-prop-map-is-de-morgan-emb G)) ``` diff --git a/src/logic/de-morgan-maps.lagda.md b/src/logic/de-morgan-maps.lagda.md index 98d4d2b321f..a4c1369e307 100644 --- a/src/logic/de-morgan-maps.lagda.md +++ b/src/logic/de-morgan-maps.lagda.md @@ -27,7 +27,7 @@ open import foundation.injective-maps open import foundation.negation open import foundation.propositions open import foundation.retractions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.retracts-of-types open import foundation.transport-along-identifications open import foundation.unit-type @@ -319,7 +319,7 @@ module _ ( F (map-codomain-cartesian-hom-arrow g f α d)) ``` -### De Morgan maps are closed under retracts of maps +### De Morgan maps are closed under retracts of arrows ```agda module _ @@ -327,13 +327,13 @@ module _ {f : A → B} {g : X → Y} where - is-de-morgan-retract-map : - f retract-of-map g → + is-de-morgan-retract-arrow : + f retract-of-arrow g → is-de-morgan-map g → is-de-morgan-map f - is-de-morgan-retract-map R G x = + is-de-morgan-retract-arrow R G x = is-decidable-iff - ( map-neg (inclusion-retract (retract-fiber-retract-map f g R x))) - ( map-neg (map-retraction-retract (retract-fiber-retract-map f g R x))) - ( G (map-codomain-inclusion-retract-map f g R x)) + ( map-neg (inclusion-retract (retract-fiber-retract-arrow f g R x))) + ( map-neg (map-retraction-retract (retract-fiber-retract-arrow f g R x))) + ( G (map-codomain-inclusion-retract-arrow f g R x)) ``` diff --git a/src/logic/double-negation-eliminating-maps.lagda.md b/src/logic/double-negation-eliminating-maps.lagda.md index b5c1d526d1f..4d72dde0991 100644 --- a/src/logic/double-negation-eliminating-maps.lagda.md +++ b/src/logic/double-negation-eliminating-maps.lagda.md @@ -20,7 +20,7 @@ open import foundation.functoriality-coproduct-types open import foundation.hilbert-epsilon-operators-maps open import foundation.identity-types open import foundation.injective-maps -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.transport-along-identifications open import foundation.universe-levels @@ -314,7 +314,7 @@ module _ ( F (map-codomain-cartesian-hom-arrow g f α d)) ``` -### Double negation eliminating maps are closed under retracts of maps +### Double negation eliminating maps are closed under retracts of arrows ```agda module _ @@ -322,14 +322,14 @@ module _ {f : A → B} {g : X → Y} where - is-double-negation-eliminating-retract-map : - f retract-of-map g → + is-double-negation-eliminating-retract-arrow : + f retract-of-arrow g → is-double-negation-eliminating-map g → is-double-negation-eliminating-map f - is-double-negation-eliminating-retract-map R G x = + is-double-negation-eliminating-retract-arrow R G x = has-double-negation-elim-retract - ( retract-fiber-retract-map f g R x) - ( G (map-codomain-inclusion-retract-map f g R x)) + ( retract-fiber-retract-arrow f g R x) + ( G (map-codomain-inclusion-retract-arrow f g R x)) ``` ### Double negation eliminating maps have Hilbert ε-operators diff --git a/src/logic/double-negation-stable-embeddings.lagda.md b/src/logic/double-negation-stable-embeddings.lagda.md index f6f753758a9..cf8a48cc36b 100644 --- a/src/logic/double-negation-stable-embeddings.lagda.md +++ b/src/logic/double-negation-stable-embeddings.lagda.md @@ -22,7 +22,7 @@ open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositional-maps open import foundation.propositions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.subtype-identity-principle open import foundation.unit-type open import foundation.universal-property-equivalences @@ -663,7 +663,7 @@ module _ ( is-double-negation-stable-prop-map-is-double-negation-stable-emb F)) ``` -### Double negation stable embeddings are closed under retracts of maps +### Double negation stable embeddings are closed under retracts of arrows ```agda module _ @@ -671,22 +671,22 @@ module _ {f : A → B} {g : X → Y} where - is-double-negation-stable-prop-map-retract-map : - f retract-of-map g → + is-double-negation-stable-prop-map-retract-arrow : + f retract-of-arrow g → is-double-negation-stable-prop-map g → is-double-negation-stable-prop-map f - is-double-negation-stable-prop-map-retract-map R G x = + is-double-negation-stable-prop-map-retract-arrow R G x = is-double-negation-stable-prop-retract - ( retract-fiber-retract-map f g R x) - ( G (map-codomain-inclusion-retract-map f g R x)) + ( retract-fiber-retract-arrow f g R x) + ( G (map-codomain-inclusion-retract-arrow f g R x)) - is-double-negation-stable-emb-retract-map : - f retract-of-map g → + is-double-negation-stable-emb-retract-arrow : + f retract-of-arrow g → is-double-negation-stable-emb g → is-double-negation-stable-emb f - is-double-negation-stable-emb-retract-map R G = + is-double-negation-stable-emb-retract-arrow R G = is-double-negation-stable-emb-is-double-negation-stable-prop-map - ( is-double-negation-stable-prop-map-retract-map R + ( is-double-negation-stable-prop-map-retract-arrow R ( is-double-negation-stable-prop-map-is-double-negation-stable-emb G)) ``` diff --git a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md index 8f86a1c09da..5cd1cf6d7ad 100644 --- a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md +++ b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md @@ -80,7 +80,7 @@ module _ is-orthogonal-left-equiv-arrow α g (J g H) ``` -### Anodyne maps are closed under retracts of maps +### Anodyne maps are closed under retracts of arrows > This remains to be formalized. diff --git a/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md b/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md index 191cb040a68..a1145d14e79 100644 --- a/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md @@ -24,7 +24,7 @@ open import foundation.inhabited-types open import foundation.precomposition-dependent-functions open import foundation.precomposition-functions open import foundation.propositional-truncations -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.sections open import foundation.split-surjective-maps open import foundation.subtype-identity-principle @@ -734,7 +734,7 @@ module _ ( dependent-pullback-property-pushout-is-pushout f g c H) ``` -### `K`-connected maps are closed under retracts of maps +### `K`-connected maps are closed under retracts of arrows **Proof.** Given a retract of maps @@ -760,7 +760,7 @@ functoriality an induced retract of dependent precomposition maps Π(B'),U <--------- Π(B'),(U∘r'∘i') <----- Π(B),(U∘r') <--- Π(B'),(U), ``` -and since equivalences are closed under retracts of maps, if `f` is +and since equivalences are closed under retracts of arrows, if `f` is `K`-connected then so is `f'`. ∎ > This remains to be formalized. @@ -771,18 +771,18 @@ The formalization below takes a shortcut via the fiber condition. module _ {l1 l2 l3 l4 l5 l6 : Level} (K : subuniverse l1 l2) {A : UU l3} {B : UU l4} {C : UU l5} {D : UU l6} - {f : A → B} {g : C → D} (R : f retract-of-map g) + {f : A → B} {g : C → D} (R : f retract-of-arrow g) where - is-subuniverse-connected-map-retract-map' : + is-subuniverse-connected-map-retract-arrow' : ((y : D) → is-subuniverse-connected K (fiber g y)) → is-subuniverse-connected-map K f - is-subuniverse-connected-map-retract-map' H = + is-subuniverse-connected-map-retract-arrow' H = is-subuniverse-connected-map-is-subuniverse-connected-fibers K f ( λ b → is-subuniverse-connected-retract K - ( retract-fiber-retract-map f g R b) - ( H (map-codomain-inclusion-retract-map f g R b))) + ( retract-fiber-retract-arrow f g R b) + ( H (map-codomain-inclusion-retract-arrow f g R b))) ``` ### The total map induced by a family of maps is `K`-connected if and only if all maps in the family are `K`-connected diff --git a/src/orthogonal-factorization-systems/connected-types-at-subuniverses.lagda.md b/src/orthogonal-factorization-systems/connected-types-at-subuniverses.lagda.md index 9c55d85bf0b..0675ac087ce 100644 --- a/src/orthogonal-factorization-systems/connected-types-at-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/connected-types-at-subuniverses.lagda.md @@ -11,7 +11,7 @@ open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.diagonal-maps-of-types open import foundation.equivalences -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.retracts-of-types open import foundation.subuniverses open import foundation.unit-type @@ -223,10 +223,10 @@ module _ is-subuniverse-connected K B → is-subuniverse-connected K A is-subuniverse-connected-retract R H U = - is-equiv-retract-map-is-equiv + is-equiv-retract-arrow-is-equiv ( diagonal-exponential (pr1 U) A) ( diagonal-exponential (pr1 U) B) - ( retract-map-diagonal-exponential-retract id-retract R) + ( retract-arrow-diagonal-exponential-retract id-retract R) ( H U) ``` diff --git a/src/orthogonal-factorization-systems/functoriality-localizations-at-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/functoriality-localizations-at-global-subuniverses.lagda.md index 84d05820795..ee68ac8344c 100644 --- a/src/orthogonal-factorization-systems/functoriality-localizations-at-global-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/functoriality-localizations-at-global-subuniverses.lagda.md @@ -24,7 +24,7 @@ open import foundation.identity-types open import foundation.precomposition-functions open import foundation.propositions open import foundation.retractions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.retracts-of-types open import foundation.subuniverses open import foundation.unit-type @@ -360,7 +360,7 @@ module _ ( 𝒫) ( reflection-localization-global-subuniverse LX) ( up-localization-global-subuniverse LX) - ( is-equiv-retract-map-is-equiv' + ( is-equiv-retract-arrow-is-equiv' ( unit-localization-global-subuniverse LX) ( unit-localization-global-subuniverse LY) ( R) diff --git a/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md b/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md index 7d7e25d9c1e..560481febd6 100644 --- a/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md +++ b/src/orthogonal-factorization-systems/functoriality-pullback-hom.lagda.md @@ -25,7 +25,7 @@ open import foundation.morphisms-arrows open import foundation.morphisms-cospan-diagrams open import foundation.postcomposition-functions open import foundation.precomposition-functions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.universe-levels open import foundation.whiskering-higher-homotopies-composition open import foundation.whiskering-homotopies-composition diff --git a/src/orthogonal-factorization-systems/functoriality-reflective-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/functoriality-reflective-global-subuniverses.lagda.md index 495d59bdb18..4e02f4735cc 100644 --- a/src/orthogonal-factorization-systems/functoriality-reflective-global-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/functoriality-reflective-global-subuniverses.lagda.md @@ -23,7 +23,7 @@ open import foundation.identity-types open import foundation.precomposition-functions open import foundation.propositions open import foundation.retractions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.retracts-of-types open import foundation.subuniverses open import foundation.unit-type diff --git a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md index 921e0c45d7d..0cde3701c02 100644 --- a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md @@ -26,7 +26,7 @@ open import foundation.postcomposition-functions open import foundation.precomposition-functions open import foundation.propositions open import foundation.pullbacks -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.unit-type open import foundation.universal-property-family-of-fibers-of-maps open import foundation.universe-levels @@ -139,12 +139,12 @@ module _ {f : A → B} {g : C → D} {g' : E → F} where - is-local-retract-map : - is-local-map f g → g' retract-of-map g → is-local-map f g' - is-local-retract-map G R d = + is-local-retract-arrow : + is-local-map f g → g' retract-of-arrow g → is-local-map f g' + is-local-retract-arrow G R d = is-local-retract - ( retract-fiber-retract-map g' g R d) - ( G (map-codomain-inclusion-retract-map g' g R d)) + ( retract-fiber-retract-arrow g' g R d) + ( G (map-codomain-inclusion-retract-arrow g' g R d)) ``` ```agda @@ -154,10 +154,10 @@ module _ {f : A → B} {g : C → D} {f' : E → F} where - is-local-retract-map' : - is-local-map f g → f' retract-of-map f → is-local-map f' g - is-local-retract-map' F R d = - is-local-retract-map-is-local f' f R (fiber g d) (F d) + is-local-retract-arrow' : + is-local-map f g → f' retract-of-arrow f → is-local-map f' g + is-local-retract-arrow' F R d = + is-local-retract-arrow-is-local f' f R (fiber g d) (F d) ``` ## See also diff --git a/src/orthogonal-factorization-systems/null-types.lagda.md b/src/orthogonal-factorization-systems/null-types.lagda.md index d47b2a74fd6..a7799e80e18 100644 --- a/src/orthogonal-factorization-systems/null-types.lagda.md +++ b/src/orthogonal-factorization-systems/null-types.lagda.md @@ -25,7 +25,7 @@ open import foundation.precomposition-dependent-functions open import foundation.precomposition-functions open import foundation.propositions open import foundation.retractions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.retracts-of-types open import foundation.sections open import foundation.type-arithmetic-unit-type @@ -132,10 +132,10 @@ module _ is-null-retract : X retract-of Y → A retract-of B → is-null Y B → is-null X A is-null-retract e f = - is-equiv-retract-map-is-equiv + is-equiv-retract-arrow-is-equiv ( diagonal-exponential A X) ( diagonal-exponential B Y) - ( retract-map-diagonal-exponential-retract f e) + ( retract-arrow-diagonal-exponential-retract f e) module _ {l1 l2 l3 : Level} {Y : UU l1} {A : UU l2} {B : UU l3} diff --git a/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md index 7292a82aa04..ecccffcc352 100644 --- a/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md @@ -22,7 +22,7 @@ open import foundation.identity-types open import foundation.postcomposition-dependent-functions open import foundation.postcomposition-functions open import foundation.propositions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.retracts-of-types open import foundation.unit-type open import foundation.universal-property-empty-type @@ -183,15 +183,15 @@ module _ ```agda module _ {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (R : g retract-of-map f) (S : UU l5) + (f : A → B) (g : X → Y) (R : g retract-of-arrow f) (S : UU l5) where - is-colocal-retract-map-is-colocal : is-colocal f S → is-colocal g S - is-colocal-retract-map-is-colocal = - is-equiv-retract-map-is-equiv + is-colocal-retract-arrow-is-colocal : is-colocal f S → is-colocal g S + is-colocal-retract-arrow-is-colocal = + is-equiv-retract-arrow-is-equiv ( postcomp S g) ( postcomp S f) - ( retract-map-postcomp-retract-map g f R S) + ( retract-arrow-postcomp-retract-arrow g f R S) ``` In fact, the higher coherence of the retract is not needed: @@ -210,9 +210,9 @@ module _ (S : UU l5) where - is-colocal-retract-map-is-colocal' : is-colocal f S → is-colocal g S - is-colocal-retract-map-is-colocal' = - is-equiv-retract-map-is-equiv' + is-colocal-retract-arrow-is-colocal' : is-colocal f S → is-colocal g S + is-colocal-retract-arrow-is-colocal' = + is-equiv-retract-arrow-is-equiv' ( postcomp S g) ( postcomp S f) ( retract-postcomp S R₀) diff --git a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md index 61cd3a03c0e..4fb55695d5f 100644 --- a/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-local-at-maps.lagda.md @@ -32,7 +32,7 @@ open import foundation.precomposition-functions open import foundation.propositional-maps open import foundation.propositions open import foundation.retractions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.retracts-of-types open import foundation.sections open import foundation.transport-along-identifications @@ -223,7 +223,7 @@ module _ is-local-retract : A retract-of B → is-local f B → is-local f A is-local-retract R = - is-equiv-retract-map-is-equiv' + is-equiv-retract-arrow-is-equiv' ( precomp f A) ( precomp f B) ( retract-postcomp Y R) @@ -251,15 +251,15 @@ module _ ```agda module _ {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (R : f retract-of-map g) (S : UU l5) + (f : A → B) (g : X → Y) (R : f retract-of-arrow g) (S : UU l5) where - is-local-retract-map-is-local : is-local g S → is-local f S - is-local-retract-map-is-local = - is-equiv-retract-map-is-equiv + is-local-retract-arrow-is-local : is-local g S → is-local f S + is-local-retract-arrow-is-local = + is-equiv-retract-arrow-is-equiv ( precomp f S) ( precomp g S) - ( retract-map-precomp-retract-map f g R S) + ( retract-arrow-precomp-retract-arrow f g R S) ``` In fact, the higher coherence of the retract is not needed: @@ -278,9 +278,9 @@ module _ (S : UU l5) where - is-local-retract-map-is-local' : is-local g S → is-local f S - is-local-retract-map-is-local' = - is-equiv-retract-map-is-equiv' + is-local-retract-arrow-is-local' : is-local g S → is-local f S + is-local-retract-arrow-is-local' = + is-equiv-retract-arrow-is-equiv' ( precomp f S) ( precomp g S) ( retract-precomp R₁ S) diff --git a/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md index a2a1cdbe49c..76eaf486727 100644 --- a/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md +++ b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md @@ -14,7 +14,7 @@ open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-coproduct-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.unit-type open import foundation.universe-levels @@ -74,7 +74,7 @@ module _ ( is-orthogonal-terminal-map-is-local f (G x))) ``` -### Weakly anodyne maps are closed under retracts of maps +### Weakly anodyne maps are closed under retracts of arrows ```agda module _ @@ -83,8 +83,8 @@ module _ (f : A → B) {j : C → D} {j' : C' → D'} where - is-weakly-anodyne-map-retract-map : - retract-map j j' → is-weakly-anodyne-map f j → is-weakly-anodyne-map f j' - is-weakly-anodyne-map-retract-map α J g G x = - is-local-retract-map-is-local j' j α (fiber g x) (J g G x) + is-weakly-anodyne-map-retract-arrow : + retract-arrow j j' → is-weakly-anodyne-map f j → is-weakly-anodyne-map f j' + is-weakly-anodyne-map-retract-arrow α J g G x = + is-local-retract-arrow-is-local j' j α (fiber g x) (J g G x) ``` diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index a37d589205e..ac41654748a 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -34,7 +34,7 @@ open import foundation.precomposition-functions open import foundation.propositional-truncations open import foundation.propositions open import foundation.pullbacks -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.torsorial-type-families open import foundation.type-arithmetic-dependent-pair-types open import foundation.type-arithmetic-unit-type @@ -563,11 +563,11 @@ module _ where is-acyclic-map-retract-of : - f retract-of-map g → is-acyclic-map g → is-acyclic-map f + f retract-of-arrow g → is-acyclic-map g → is-acyclic-map f is-acyclic-map-retract-of R ac b = is-acyclic-retract-of - ( retract-fiber-retract-map f g R b) - ( ac (map-codomain-inclusion-retract-map f g R b)) + ( retract-fiber-retract-arrow f g R b) + ( ac (map-codomain-inclusion-retract-arrow f g R b)) ``` ## See also diff --git a/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md index 13ad9399bb5..635ec92720b 100644 --- a/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md @@ -202,4 +202,4 @@ module _ ## See also -- [Retracts of maps](foundation.retracts-of-maps.md) +- [Retracts of arrows](foundation.retracts-of-arrows.md) diff --git a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md index de8f09d97b7..873360d40a1 100644 --- a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md @@ -35,7 +35,7 @@ open import foundation.precomposition-functions open import foundation.propositional-truncations open import foundation.propositions open import foundation.pullbacks -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.torsorial-type-families open import foundation.truncated-types open import foundation.truncation-equivalences @@ -529,13 +529,13 @@ module _ where is-truncated-acyclic-map-retract-of : - f retract-of-map g → + f retract-of-arrow g → is-truncated-acyclic-map k g → is-truncated-acyclic-map k f is-truncated-acyclic-map-retract-of R ac b = is-truncated-acyclic-retract-of - ( retract-fiber-retract-map f g R b) - ( ac (map-codomain-inclusion-retract-map f g R b)) + ( retract-fiber-retract-arrow f g R b) + ( ac (map-codomain-inclusion-retract-arrow f g R b)) ``` ### `k`-acyclic maps are closed under pushouts From 87d999a9ed3c785b921008e753ef1f49d1f9e968 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 8 Dec 2025 20:06:07 +0000 Subject: [PATCH 2/8] split equivalences of arrows --- src/foundation-core.lagda.md | 1 + .../equivalences-arrows.lagda.md | 265 ++++++++++++++++++ src/foundation.lagda.md | 1 + src/foundation/equivalences-arrows.lagda.md | 227 ++------------- ...oriality-dependent-function-types.lagda.md | 13 +- .../functoriality-function-types.lagda.md | 26 +- src/foundation/monomorphisms.lagda.md | 102 ++++--- src/foundation/retracts-of-arrows.lagda.md | 42 ++- .../univalent-type-families.lagda.md | 1 - 9 files changed, 418 insertions(+), 260 deletions(-) create mode 100644 src/foundation-core/equivalences-arrows.lagda.md diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index 8291e2bc800..f08a3e2fe06 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -28,6 +28,7 @@ open import foundation-core.endomorphisms public open import foundation-core.equality-dependent-pair-types public open import foundation-core.equivalence-relations public open import foundation-core.equivalences public +open import foundation-core.equivalences-arrows public open import foundation-core.families-of-equivalences public open import foundation-core.fibers-of-maps public open import foundation-core.function-types public diff --git a/src/foundation-core/equivalences-arrows.lagda.md b/src/foundation-core/equivalences-arrows.lagda.md new file mode 100644 index 00000000000..47c011f38ee --- /dev/null +++ b/src/foundation-core/equivalences-arrows.lagda.md @@ -0,0 +1,265 @@ +# Equivalences of arrows + +```agda +module foundation-core.equivalences-arrows where +``` + +
Imports + +```agda +open import foundation.commuting-squares-of-maps +open import foundation.dependent-pair-types +open import foundation.homotopies +open import foundation.morphisms-arrows +open import foundation.span-diagrams +open import foundation.spans +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.equivalences +``` + +
+ +## Idea + +An {{#concept "equivalence of arrows" Agda=equiv-arrow}} from a function +`f : A → B` to a function `g : X → Y` is a +[morphism of arrows](foundation.morphisms-arrows.md) + +```text + i + A ------> X + | | + f | | g + ∨ ∨ + B ------> Y + j +``` + +in which `i` and `j` are [equivalences](foundation-core.equivalences.md). + +## Definitions + +### The predicate of being an equivalence of arrows + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + (f : A → B) (g : X → Y) (h : hom-arrow f g) + where + + is-equiv-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + is-equiv-hom-arrow = + ( is-equiv (map-domain-hom-arrow f g h)) × + ( is-equiv (map-codomain-hom-arrow f g h)) + + is-equiv-map-domain-is-equiv-hom-arrow : + is-equiv-hom-arrow → is-equiv (map-domain-hom-arrow f g h) + is-equiv-map-domain-is-equiv-hom-arrow = pr1 + + is-equiv-map-codomain-is-equiv-hom-arrow : + is-equiv-hom-arrow → is-equiv (map-codomain-hom-arrow f g h) + is-equiv-map-codomain-is-equiv-hom-arrow = pr2 +``` + +### Equivalences of arrows + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + (f : A → B) (g : X → Y) + where + + coherence-equiv-arrow : (A ≃ X) → (B ≃ Y) → UU (l1 ⊔ l4) + coherence-equiv-arrow i j = + coherence-hom-arrow f g (map-equiv i) (map-equiv j) + + equiv-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + equiv-arrow = Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i)) + + module _ + (e : equiv-arrow) + where + + equiv-domain-equiv-arrow : A ≃ X + equiv-domain-equiv-arrow = pr1 e + + map-domain-equiv-arrow : A → X + map-domain-equiv-arrow = map-equiv equiv-domain-equiv-arrow + + map-inv-domain-equiv-arrow : X → A + map-inv-domain-equiv-arrow = map-inv-equiv equiv-domain-equiv-arrow + + is-equiv-map-domain-equiv-arrow : is-equiv map-domain-equiv-arrow + is-equiv-map-domain-equiv-arrow = + is-equiv-map-equiv equiv-domain-equiv-arrow + + equiv-codomain-equiv-arrow : B ≃ Y + equiv-codomain-equiv-arrow = pr1 (pr2 e) + + map-codomain-equiv-arrow : B → Y + map-codomain-equiv-arrow = map-equiv equiv-codomain-equiv-arrow + + map-inv-codomain-equiv-arrow : Y → B + map-inv-codomain-equiv-arrow = map-inv-equiv equiv-codomain-equiv-arrow + + is-equiv-map-codomain-equiv-arrow : is-equiv map-codomain-equiv-arrow + is-equiv-map-codomain-equiv-arrow = + is-equiv-map-equiv equiv-codomain-equiv-arrow + + coh-equiv-arrow : + coherence-equiv-arrow + ( equiv-domain-equiv-arrow) + ( equiv-codomain-equiv-arrow) + coh-equiv-arrow = pr2 (pr2 e) + + hom-equiv-arrow : hom-arrow f g + pr1 hom-equiv-arrow = map-domain-equiv-arrow + pr1 (pr2 hom-equiv-arrow) = map-codomain-equiv-arrow + pr2 (pr2 hom-equiv-arrow) = coh-equiv-arrow + + is-equiv-equiv-arrow : is-equiv-hom-arrow f g hom-equiv-arrow + pr1 is-equiv-equiv-arrow = is-equiv-map-domain-equiv-arrow + pr2 is-equiv-equiv-arrow = is-equiv-map-codomain-equiv-arrow + + span-equiv-arrow : + span l1 B X + span-equiv-arrow = + span-hom-arrow f g hom-equiv-arrow + + span-diagram-equiv-arrow : span-diagram l2 l3 l1 + pr1 span-diagram-equiv-arrow = B + pr1 (pr2 span-diagram-equiv-arrow) = X + pr2 (pr2 span-diagram-equiv-arrow) = span-equiv-arrow +``` + +### The identity equivalence of arrows + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + id-equiv-arrow : equiv-arrow f f + pr1 id-equiv-arrow = id-equiv + pr1 (pr2 id-equiv-arrow) = id-equiv + pr2 (pr2 id-equiv-arrow) = refl-htpy +``` + +### Composition of equivalences of arrows + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6} + (f : A → B) (g : X → Y) (h : U → V) + (b : equiv-arrow g h) (a : equiv-arrow f g) + where + + equiv-domain-comp-equiv-arrow : A ≃ U + equiv-domain-comp-equiv-arrow = + equiv-domain-equiv-arrow g h b ∘e equiv-domain-equiv-arrow f g a + + map-domain-comp-equiv-arrow : A → U + map-domain-comp-equiv-arrow = map-equiv equiv-domain-comp-equiv-arrow + + equiv-codomain-comp-equiv-arrow : B ≃ V + equiv-codomain-comp-equiv-arrow = + equiv-codomain-equiv-arrow g h b ∘e equiv-codomain-equiv-arrow f g a + + map-codomain-comp-equiv-arrow : B → V + map-codomain-comp-equiv-arrow = map-equiv equiv-codomain-comp-equiv-arrow + + coh-comp-equiv-arrow : + coherence-equiv-arrow f h + ( equiv-domain-comp-equiv-arrow) + ( equiv-codomain-comp-equiv-arrow) + coh-comp-equiv-arrow = + coh-comp-hom-arrow f g h + ( hom-equiv-arrow g h b) + ( hom-equiv-arrow f g a) + + comp-equiv-arrow : equiv-arrow f h + pr1 comp-equiv-arrow = equiv-domain-comp-equiv-arrow + pr1 (pr2 comp-equiv-arrow) = equiv-codomain-comp-equiv-arrow + pr2 (pr2 comp-equiv-arrow) = coh-comp-equiv-arrow + + hom-comp-equiv-arrow : hom-arrow f h + hom-comp-equiv-arrow = hom-equiv-arrow f h comp-equiv-arrow +``` + +### Inverses of equivalences of arrows + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + (f : A → B) (g : X → Y) (α : equiv-arrow f g) + where + + equiv-domain-inv-equiv-arrow : X ≃ A + equiv-domain-inv-equiv-arrow = inv-equiv (equiv-domain-equiv-arrow f g α) + + map-domain-inv-equiv-arrow : X → A + map-domain-inv-equiv-arrow = map-equiv equiv-domain-inv-equiv-arrow + + equiv-codomain-inv-equiv-arrow : Y ≃ B + equiv-codomain-inv-equiv-arrow = inv-equiv (equiv-codomain-equiv-arrow f g α) + + map-codomain-inv-equiv-arrow : Y → B + map-codomain-inv-equiv-arrow = map-equiv equiv-codomain-inv-equiv-arrow + + coh-inv-equiv-arrow : + coherence-equiv-arrow g f + ( equiv-domain-inv-equiv-arrow) + ( equiv-codomain-inv-equiv-arrow) + coh-inv-equiv-arrow = + horizontal-inv-equiv-coherence-square-maps + ( equiv-domain-equiv-arrow f g α) + ( f) + ( g) + ( equiv-codomain-equiv-arrow f g α) + ( coh-equiv-arrow f g α) + + inv-equiv-arrow : equiv-arrow g f + pr1 inv-equiv-arrow = equiv-domain-inv-equiv-arrow + pr1 (pr2 inv-equiv-arrow) = equiv-codomain-inv-equiv-arrow + pr2 (pr2 inv-equiv-arrow) = coh-inv-equiv-arrow + + hom-inv-equiv-arrow : hom-arrow g f + hom-inv-equiv-arrow = hom-equiv-arrow g f inv-equiv-arrow + + is-equiv-inv-equiv-arrow : is-equiv-hom-arrow g f hom-inv-equiv-arrow + is-equiv-inv-equiv-arrow = is-equiv-equiv-arrow g f inv-equiv-arrow +``` + +### If a map is equivalent to an equivalence, then it is an equivalence + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + (f : A → B) (g : X → Y) (α : equiv-arrow f g) + where + + is-equiv-source-is-equiv-target-equiv-arrow : is-equiv g → is-equiv f + is-equiv-source-is-equiv-target-equiv-arrow = + is-equiv-left-is-equiv-right-square + ( f) + ( g) + ( map-domain-equiv-arrow f g α) + ( map-codomain-equiv-arrow f g α) + ( coh-equiv-arrow f g α) + ( is-equiv-map-domain-equiv-arrow f g α) + ( is-equiv-map-codomain-equiv-arrow f g α) + + is-equiv-target-is-equiv-source-equiv-arrow : is-equiv f → is-equiv g + is-equiv-target-is-equiv-source-equiv-arrow = + is-equiv-right-is-equiv-left-square + ( f) + ( g) + ( map-domain-equiv-arrow f g α) + ( map-codomain-equiv-arrow f g α) + ( coh-equiv-arrow f g α) + ( is-equiv-map-domain-equiv-arrow f g α) + ( is-equiv-map-codomain-equiv-arrow f g α) +``` diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index cb38823d9b3..36b6a7ec9b2 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -394,6 +394,7 @@ open import foundation.relaxed-sigma-decompositions public open import foundation.repetitions-of-values public open import foundation.replacement public open import foundation.retractions public +open import foundation.retracts-of-arrows public open import foundation.retracts-of-types public open import foundation.sections public open import foundation.separated-types-subuniverses public diff --git a/src/foundation/equivalences-arrows.lagda.md b/src/foundation/equivalences-arrows.lagda.md index de15f1eb08c..12845486f87 100644 --- a/src/foundation/equivalences-arrows.lagda.md +++ b/src/foundation/equivalences-arrows.lagda.md @@ -2,6 +2,8 @@ ```agda module foundation.equivalences-arrows where + +open import foundation-core.equivalences-arrows public ```
Imports @@ -10,11 +12,12 @@ module foundation.equivalences-arrows where open import foundation.cartesian-morphisms-arrows open import foundation.commuting-squares-of-maps open import foundation.dependent-pair-types +open import foundation.embeddings open import foundation.equivalences open import foundation.homotopies open import foundation.morphisms-arrows open import foundation.retractions -open import foundation.retracts-of-maps +open import foundation.retracts-of-arrows open import foundation.sections open import foundation.span-diagrams open import foundation.spans @@ -27,24 +30,24 @@ open import foundation-core.propositions ## Idea -An {{#concept "equivalence of arrows"}} from a function `f : A → B` to a -function `g : X → Y` is a [morphism of arrows](foundation.morphisms-arrows.md) +An **equivalence of arrows** from a function `f : A → B` to a function +`g : X → Y` is a [morphism of arrows](foundation.morphisms-arrows.md) ```text i A ------> X - | ≃ | + | | f | | g - ∨ ≃ ∨ + ∨ ∨ B ------> Y j ``` in which `i` and `j` are [equivalences](foundation-core.equivalences.md). -## Definitions +## Properties -### The predicate of being an equivalence of arrows +### Being an equivalence of arrows is a proposition ```agda module _ @@ -58,193 +61,11 @@ module _ ( is-equiv-Prop (map-domain-hom-arrow f g h)) ( is-equiv-Prop (map-codomain-hom-arrow f g h)) - is-equiv-hom-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - is-equiv-hom-arrow = - type-Prop is-equiv-prop-hom-arrow - - is-prop-is-equiv-hom-arrow : is-prop is-equiv-hom-arrow + is-prop-is-equiv-hom-arrow : is-prop (is-equiv-hom-arrow f g h) is-prop-is-equiv-hom-arrow = is-prop-type-Prop is-equiv-prop-hom-arrow - - is-equiv-map-domain-is-equiv-hom-arrow : - is-equiv-hom-arrow → is-equiv (map-domain-hom-arrow f g h) - is-equiv-map-domain-is-equiv-hom-arrow = pr1 - - is-equiv-map-codomain-is-equiv-hom-arrow : - is-equiv-hom-arrow → is-equiv (map-codomain-hom-arrow f g h) - is-equiv-map-codomain-is-equiv-hom-arrow = pr2 ``` -### Equivalences of arrows - -```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) - where - - coherence-equiv-arrow : (A ≃ X) → (B ≃ Y) → UU (l1 ⊔ l4) - coherence-equiv-arrow i j = - coherence-hom-arrow f g (map-equiv i) (map-equiv j) - - equiv-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - equiv-arrow = Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i)) - - module _ - (e : equiv-arrow) - where - - equiv-domain-equiv-arrow : A ≃ X - equiv-domain-equiv-arrow = pr1 e - - map-domain-equiv-arrow : A → X - map-domain-equiv-arrow = map-equiv equiv-domain-equiv-arrow - - map-inv-domain-equiv-arrow : X → A - map-inv-domain-equiv-arrow = map-inv-equiv equiv-domain-equiv-arrow - - is-equiv-map-domain-equiv-arrow : is-equiv map-domain-equiv-arrow - is-equiv-map-domain-equiv-arrow = - is-equiv-map-equiv equiv-domain-equiv-arrow - - equiv-codomain-equiv-arrow : B ≃ Y - equiv-codomain-equiv-arrow = pr1 (pr2 e) - - map-codomain-equiv-arrow : B → Y - map-codomain-equiv-arrow = map-equiv equiv-codomain-equiv-arrow - - map-inv-codomain-equiv-arrow : Y → B - map-inv-codomain-equiv-arrow = map-inv-equiv equiv-codomain-equiv-arrow - - is-equiv-map-codomain-equiv-arrow : is-equiv map-codomain-equiv-arrow - is-equiv-map-codomain-equiv-arrow = - is-equiv-map-equiv equiv-codomain-equiv-arrow - - coh-equiv-arrow : - coherence-equiv-arrow - ( equiv-domain-equiv-arrow) - ( equiv-codomain-equiv-arrow) - coh-equiv-arrow = pr2 (pr2 e) - - hom-equiv-arrow : hom-arrow f g - pr1 hom-equiv-arrow = map-domain-equiv-arrow - pr1 (pr2 hom-equiv-arrow) = map-codomain-equiv-arrow - pr2 (pr2 hom-equiv-arrow) = coh-equiv-arrow - - is-equiv-equiv-arrow : is-equiv-hom-arrow f g hom-equiv-arrow - pr1 is-equiv-equiv-arrow = is-equiv-map-domain-equiv-arrow - pr2 is-equiv-equiv-arrow = is-equiv-map-codomain-equiv-arrow - - span-equiv-arrow : - span l1 B X - span-equiv-arrow = - span-hom-arrow f g hom-equiv-arrow - - span-diagram-equiv-arrow : span-diagram l2 l3 l1 - pr1 span-diagram-equiv-arrow = B - pr1 (pr2 span-diagram-equiv-arrow) = X - pr2 (pr2 span-diagram-equiv-arrow) = span-equiv-arrow -``` - -### The identity equivalence of arrows - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} - where - - id-equiv-arrow : equiv-arrow f f - pr1 id-equiv-arrow = id-equiv - pr1 (pr2 id-equiv-arrow) = id-equiv - pr2 (pr2 id-equiv-arrow) = refl-htpy -``` - -### Composition of equivalences of arrows - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6} - (f : A → B) (g : X → Y) (h : U → V) - (b : equiv-arrow g h) (a : equiv-arrow f g) - where - - equiv-domain-comp-equiv-arrow : A ≃ U - equiv-domain-comp-equiv-arrow = - equiv-domain-equiv-arrow g h b ∘e equiv-domain-equiv-arrow f g a - - map-domain-comp-equiv-arrow : A → U - map-domain-comp-equiv-arrow = map-equiv equiv-domain-comp-equiv-arrow - - equiv-codomain-comp-equiv-arrow : B ≃ V - equiv-codomain-comp-equiv-arrow = - equiv-codomain-equiv-arrow g h b ∘e equiv-codomain-equiv-arrow f g a - - map-codomain-comp-equiv-arrow : B → V - map-codomain-comp-equiv-arrow = map-equiv equiv-codomain-comp-equiv-arrow - - coh-comp-equiv-arrow : - coherence-equiv-arrow f h - ( equiv-domain-comp-equiv-arrow) - ( equiv-codomain-comp-equiv-arrow) - coh-comp-equiv-arrow = - coh-comp-hom-arrow f g h - ( hom-equiv-arrow g h b) - ( hom-equiv-arrow f g a) - - comp-equiv-arrow : equiv-arrow f h - pr1 comp-equiv-arrow = equiv-domain-comp-equiv-arrow - pr1 (pr2 comp-equiv-arrow) = equiv-codomain-comp-equiv-arrow - pr2 (pr2 comp-equiv-arrow) = coh-comp-equiv-arrow - - hom-comp-equiv-arrow : hom-arrow f h - hom-comp-equiv-arrow = hom-equiv-arrow f h comp-equiv-arrow -``` - -### Inverses of equivalences of arrows - -```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (α : equiv-arrow f g) - where - - equiv-domain-inv-equiv-arrow : X ≃ A - equiv-domain-inv-equiv-arrow = inv-equiv (equiv-domain-equiv-arrow f g α) - - map-domain-inv-equiv-arrow : X → A - map-domain-inv-equiv-arrow = map-equiv equiv-domain-inv-equiv-arrow - - equiv-codomain-inv-equiv-arrow : Y ≃ B - equiv-codomain-inv-equiv-arrow = inv-equiv (equiv-codomain-equiv-arrow f g α) - - map-codomain-inv-equiv-arrow : Y → B - map-codomain-inv-equiv-arrow = map-equiv equiv-codomain-inv-equiv-arrow - - coh-inv-equiv-arrow : - coherence-equiv-arrow g f - ( equiv-domain-inv-equiv-arrow) - ( equiv-codomain-inv-equiv-arrow) - coh-inv-equiv-arrow = - horizontal-inv-equiv-coherence-square-maps - ( equiv-domain-equiv-arrow f g α) - ( f) - ( g) - ( equiv-codomain-equiv-arrow f g α) - ( coh-equiv-arrow f g α) - - inv-equiv-arrow : equiv-arrow g f - pr1 inv-equiv-arrow = equiv-domain-inv-equiv-arrow - pr1 (pr2 inv-equiv-arrow) = equiv-codomain-inv-equiv-arrow - pr2 (pr2 inv-equiv-arrow) = coh-inv-equiv-arrow - - hom-inv-equiv-arrow : hom-arrow g f - hom-inv-equiv-arrow = hom-equiv-arrow g f inv-equiv-arrow - - is-equiv-inv-equiv-arrow : is-equiv-hom-arrow g f hom-inv-equiv-arrow - is-equiv-inv-equiv-arrow = is-equiv-equiv-arrow g f inv-equiv-arrow -``` - -### If a map is equivalent to an equivalence, then it is an equivalence +### If a map is equivalent to an embedding, then it is an embedding ```agda module _ @@ -252,25 +73,25 @@ module _ (f : A → B) (g : X → Y) (α : equiv-arrow f g) where - is-equiv-source-is-equiv-target-equiv-arrow : is-equiv g → is-equiv f - is-equiv-source-is-equiv-target-equiv-arrow = - is-equiv-left-is-equiv-right-square + is-emb-source-is-emb-target-equiv-arrow : is-emb g → is-emb f + is-emb-source-is-emb-target-equiv-arrow = + is-emb-top-is-emb-bottom-is-equiv-coherence-square-maps ( f) - ( g) ( map-domain-equiv-arrow f g α) ( map-codomain-equiv-arrow f g α) - ( coh-equiv-arrow f g α) + ( g) + ( inv-htpy (coh-equiv-arrow f g α)) ( is-equiv-map-domain-equiv-arrow f g α) ( is-equiv-map-codomain-equiv-arrow f g α) - is-equiv-target-is-equiv-source-equiv-arrow : is-equiv f → is-equiv g - is-equiv-target-is-equiv-source-equiv-arrow = - is-equiv-right-is-equiv-left-square + is-emb-target-is-emb-source-equiv-arrow : is-emb f → is-emb g + is-emb-target-is-emb-source-equiv-arrow = + is-emb-bottom-is-emb-top-is-equiv-coherence-square-maps ( f) - ( g) ( map-domain-equiv-arrow f g α) ( map-codomain-equiv-arrow f g α) - ( coh-equiv-arrow f g α) + ( g) + ( inv-htpy (coh-equiv-arrow f g α)) ( is-equiv-map-domain-equiv-arrow f g α) ( is-equiv-map-codomain-equiv-arrow f g α) ``` @@ -309,7 +130,7 @@ module _ reflects-retraction-equiv-arrow : equiv-arrow f g → retraction g → retraction f reflects-retraction-equiv-arrow α = - retraction-retract-map-retraction' f g + retraction-retract-arrow-retraction' f g ( retract-equiv (equiv-domain-equiv-arrow f g α)) ( map-codomain-equiv-arrow f g α) ( coh-equiv-arrow f g α) @@ -330,7 +151,7 @@ module _ preserves-section-equiv-arrow : equiv-arrow f g → section f → section g preserves-section-equiv-arrow α = - section-retract-map-section' g f + section-retract-arrow-section' g f ( map-domain-equiv-arrow f g α) ( retract-inv-equiv (equiv-codomain-equiv-arrow f g α)) ( coh-equiv-arrow f g α) diff --git a/src/foundation/functoriality-dependent-function-types.lagda.md b/src/foundation/functoriality-dependent-function-types.lagda.md index cc9c75b5652..a0273cd5a12 100644 --- a/src/foundation/functoriality-dependent-function-types.lagda.md +++ b/src/foundation/functoriality-dependent-function-types.lagda.md @@ -180,11 +180,11 @@ module _ ( compute-fiber-map-Π' α f h) ( is-trunc-Π k (λ j → H (α j) (h j))) - is-trunc-map-is-trunc-map-map-Π' : + is-trunc-map-is-trunc-map-map-Π'-lzero : (k : 𝕋) (f : (i : I) → A i → B i) → - ({l : Level} {J : UU l} (α : J → I) → is-trunc-map k (map-Π' α f)) → + ({J : UU lzero} (α : J → I) → is-trunc-map k (map-Π' α f)) → (i : I) → is-trunc-map k (f i) - is-trunc-map-is-trunc-map-map-Π' k f H i b = + is-trunc-map-is-trunc-map-map-Π'-lzero k f H i b = is-trunc-equiv' k ( fiber (map-Π (λ _ → f i)) (point b)) ( equiv-Σ @@ -197,6 +197,13 @@ module _ ( point b))) ( H (λ _ → i) (point b)) + is-trunc-map-is-trunc-map-map-Π' : + (k : 𝕋) (f : (i : I) → A i → B i) → + ({l : Level} {J : UU l} (α : J → I) → is-trunc-map k (map-Π' α f)) → + (i : I) → is-trunc-map k (f i) + is-trunc-map-is-trunc-map-map-Π' k f H i b = + is-trunc-map-is-trunc-map-map-Π'-lzero k f H i b + is-emb-map-Π' : {l4 : Level} {J : UU l4} (α : J → I) (f : (i : I) → A i → B i) → ((i : I) → is-emb (f i)) → is-emb (map-Π' α f) diff --git a/src/foundation/functoriality-function-types.lagda.md b/src/foundation/functoriality-function-types.lagda.md index 7797a47622c..55cee9d1d96 100644 --- a/src/foundation/functoriality-function-types.lagda.md +++ b/src/foundation/functoriality-function-types.lagda.md @@ -73,14 +73,20 @@ module _ is-trunc-map-postcomp-is-trunc-map is-trunc-f A = is-trunc-map-map-Π' k (terminal-map A) (point f) (point is-trunc-f) + is-trunc-map-is-trunc-map-postcomp-lzero : + ((A : UU lzero) → is-trunc-map k (postcomp A f)) → + is-trunc-map k f + is-trunc-map-is-trunc-map-postcomp-lzero is-trunc-postcomp-f = + is-trunc-map-is-trunc-map-map-Π'-lzero k + ( point f) + ( λ {J} α → is-trunc-postcomp-f J) + ( star) + is-trunc-map-is-trunc-map-postcomp : ({l3 : Level} (A : UU l3) → is-trunc-map k (postcomp A f)) → is-trunc-map k f is-trunc-map-is-trunc-map-postcomp is-trunc-postcomp-f = - is-trunc-map-is-trunc-map-map-Π' k - ( point f) - ( λ {l} {J} α → is-trunc-postcomp-f {l} J) - ( star) + is-trunc-map-is-trunc-map-postcomp-lzero is-trunc-postcomp-f module _ {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y) @@ -95,13 +101,19 @@ module _ ( is-prop-map-is-emb is-emb-f) ( A)) + is-emb-is-emb-postcomp-lzero : + ((A : UU lzero) → is-emb (postcomp A f)) → + is-emb f + is-emb-is-emb-postcomp-lzero is-emb-postcomp-f = + is-emb-is-prop-map + ( is-trunc-map-is-trunc-map-postcomp-lzero neg-one-𝕋 f + ( is-prop-map-is-emb ∘ is-emb-postcomp-f)) + is-emb-is-emb-postcomp : ({l3 : Level} (A : UU l3) → is-emb (postcomp A f)) → is-emb f is-emb-is-emb-postcomp is-emb-postcomp-f = - is-emb-is-prop-map - ( is-trunc-map-is-trunc-map-postcomp neg-one-𝕋 f - ( is-prop-map-is-emb ∘ is-emb-postcomp-f)) + is-emb-is-emb-postcomp-lzero is-emb-postcomp-f emb-postcomp : {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (f : X ↪ Y) (A : UU l3) → diff --git a/src/foundation/monomorphisms.lagda.md b/src/foundation/monomorphisms.lagda.md index 278c91c4350..3081d989b80 100644 --- a/src/foundation/monomorphisms.lagda.md +++ b/src/foundation/monomorphisms.lagda.md @@ -12,16 +12,20 @@ open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.function-extensionality open import foundation.functoriality-function-types +open import foundation.logical-equivalences open import foundation.postcomposition-functions open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation-core.equivalences +open import foundation-core.equivalences-arrows open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositional-maps open import foundation-core.propositions +open import foundation-core.retractions +open import foundation-core.sections open import foundation-core.truncation-levels ``` @@ -29,10 +33,12 @@ open import foundation-core.truncation-levels ## Idea -A function `f : A → B` is a monomorphism if whenever we have two functions -`g h : X → A` such that `f ∘ g = f ∘ h`, then in fact `g = h`. The way to state -this in Homotopy Type Theory is to say that postcomposition by `f` is an -embedding. +A function `f : A → B` is a +{{#concept "monomorphism" Disambiguation="of types" Agda=is-mono}} if whenever +we have two functions `g h : X → A` such that `f ∘ g = f ∘ h`, then in fact +`g = h`. The correct way to state this in Homotopy Type Theory is to say that +[postcomposition](foundation-core.postcomposition-functions.md) by `f` is an +[embedding](foundation-core.embeddings.md). ## Definition @@ -43,7 +49,7 @@ module _ where is-mono-Prop : Prop (l1 ⊔ l2 ⊔ lsuc l3) - is-mono-Prop = Π-Prop (UU l3) λ X → is-emb-Prop (postcomp X f) + is-mono-Prop = Π-Prop (UU l3) (λ X → is-emb-Prop (postcomp X f)) is-mono : UU (l1 ⊔ l2 ⊔ lsuc l3) is-mono = type-Prop is-mono-Prop @@ -69,7 +75,7 @@ module _ pr1 equiv-postcomp-is-mono = ap (f ∘_) pr2 equiv-postcomp-is-mono = p X g h - is-injective-postcomp-is-mono : (f ∘ g) ＝ (f ∘ h) → g ＝ h + is-injective-postcomp-is-mono : f ∘ g ＝ f ∘ h → g ＝ h is-injective-postcomp-is-mono = map-inv-equiv equiv-postcomp-is-mono ``` @@ -87,12 +93,16 @@ module _ ( is-prop-map-is-emb is-emb-f) ( X)) - is-emb-is-mono : ({l3 : Level} → is-mono l3 f) → is-emb f - is-emb-is-mono is-mono-f = + is-emb-is-mono-lzero : is-mono lzero f → is-emb f + is-emb-is-mono-lzero is-mono-f = is-emb-is-prop-map - ( is-trunc-map-is-trunc-map-postcomp neg-one-𝕋 f + ( is-trunc-map-is-trunc-map-postcomp-lzero neg-one-𝕋 f ( λ X → is-prop-map-is-emb (is-mono-f X))) + is-emb-is-mono : ({l3 : Level} → is-mono l3 f) → is-emb f + is-emb-is-mono is-mono-f = + is-emb-is-mono-lzero is-mono-f + equiv-postcomp-is-emb : is-emb f → {l3 : Level} {X : UU l3} (g h : X → A) → (g ＝ h) ≃ (f ∘ g ＝ f ∘ h) @@ -116,29 +126,55 @@ module _ {X : UU l3} (g h : X → A) where - map-inv-equiv-htpy-postcomp-is-emb : - (pr1 f ∘ g) ~ (pr1 f ∘ h) → g ~ h - map-inv-equiv-htpy-postcomp-is-emb H x = - map-inv-is-equiv (pr2 f (g x) (h x)) (H x) - - is-section-map-inv-equiv-htpy-postcomp-is-emb : - (pr1 f ·l_) ∘ map-inv-equiv-htpy-postcomp-is-emb ~ id - is-section-map-inv-equiv-htpy-postcomp-is-emb H = - eq-htpy (λ x → - is-section-map-inv-is-equiv (pr2 f (g x) (h x)) (H x)) - - is-retraction-map-inv-equiv-htpy-postcomp-is-emb : - map-inv-equiv-htpy-postcomp-is-emb ∘ (pr1 f ·l_) ~ id - is-retraction-map-inv-equiv-htpy-postcomp-is-emb H = - eq-htpy (λ x → - is-retraction-map-inv-is-equiv (pr2 f (g x) (h x)) (H x)) - - equiv-htpy-postcomp-is-emb : - (g ~ h) ≃ (pr1 f ∘ g ~ pr1 f ∘ h) - pr1 equiv-htpy-postcomp-is-emb = pr1 f ·l_ - pr2 equiv-htpy-postcomp-is-emb = + map-inv-equiv-htpy-postcomp-emb : + map-emb f ∘ g ~ map-emb f ∘ h → g ~ h + map-inv-equiv-htpy-postcomp-emb H x = + map-inv-is-equiv (is-emb-map-emb f (g x) (h x)) (H x) + + is-section-map-inv-equiv-htpy-postcomp-emb : + is-section + ( left-whisker-comp (map-emb f)) + ( map-inv-equiv-htpy-postcomp-emb) + is-section-map-inv-equiv-htpy-postcomp-emb H = + eq-htpy + ( λ x → is-section-map-inv-is-equiv (is-emb-map-emb f (g x) (h x)) (H x)) + + is-retraction-map-inv-equiv-htpy-postcomp-emb : + is-retraction + ( left-whisker-comp (map-emb f)) + ( map-inv-equiv-htpy-postcomp-emb) + is-retraction-map-inv-equiv-htpy-postcomp-emb H = + eq-htpy + ( λ x → + is-retraction-map-inv-is-equiv (is-emb-map-emb f (g x) (h x)) (H x)) + + is-equiv-left-whisker-emb : + is-equiv (left-whisker-comp (map-emb f) {g} {h}) + is-equiv-left-whisker-emb = is-equiv-is-invertible - map-inv-equiv-htpy-postcomp-is-emb - is-section-map-inv-equiv-htpy-postcomp-is-emb - is-retraction-map-inv-equiv-htpy-postcomp-is-emb + map-inv-equiv-htpy-postcomp-emb + is-section-map-inv-equiv-htpy-postcomp-emb + is-retraction-map-inv-equiv-htpy-postcomp-emb + + equiv-htpy-postcomp-emb : + (g ~ h) ≃ (map-emb f ∘ g ~ map-emb f ∘ h) + equiv-htpy-postcomp-emb = + ( left-whisker-comp (map-emb f) , is-equiv-left-whisker-emb) +``` + +### Smallness of the mono predicate + +In order to avoid cyclic dependencies, we need to type out the definition of +being small. + +```text +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + is-small-lzero-is-mono : + {l3 : Level} → Σ (UU (lsuc lzero ⊔ l1 ⊔ l2)) (λ P → is-mono l3 f ≃ P) + is-small-lzero-is-mono {l3} = + ( is-mono lzero f , + equiv-iff (is-mono-Prop l3 f) (is-mono-Prop lzero f) (λ X H → {! i !}) {! !}) ``` diff --git a/src/foundation/retracts-of-arrows.lagda.md b/src/foundation/retracts-of-arrows.lagda.md index a38114bd862..4780940e98d 100644 --- a/src/foundation/retracts-of-arrows.lagda.md +++ b/src/foundation/retracts-of-arrows.lagda.md @@ -174,10 +174,10 @@ module _ (f : A → B) (g : X → Y) where - infix 6 _retract-of-map_ + infix 6 _retract-of-arrow_ - _retract-of-map_ : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - _retract-of-map_ = retract-arrow g f + _retract-of-arrow_ : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + _retract-of-arrow_ = retract-arrow g f module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} @@ -209,7 +209,9 @@ module _ hom-retraction-retract-arrow : hom-arrow g f hom-retraction-retract-arrow = - hom-retraction-hom-arrow f g inclusion-retract-arrow retraction-retract-arrow + hom-retraction-hom-arrow f g + ( inclusion-retract-arrow) + ( retraction-retract-arrow) map-domain-hom-retraction-retract-arrow : X → A map-domain-hom-retraction-retract-arrow = @@ -229,7 +231,9 @@ module _ coh-hom-arrow g f hom-retraction-retract-arrow is-retraction-hom-retraction-retract-arrow : - is-retraction-hom-arrow f g inclusion-retract-arrow hom-retraction-retract-arrow + is-retraction-hom-arrow f g + ( inclusion-retract-arrow) + ( hom-retraction-retract-arrow) is-retraction-hom-retraction-retract-arrow = is-retraction-hom-retraction-hom-arrow f g ( inclusion-retract-arrow) @@ -241,7 +245,9 @@ module _ ( map-domain-hom-retraction-retract-arrow) is-retraction-map-domain-hom-retraction-retract-arrow = htpy-domain-htpy-hom-arrow f f - ( comp-hom-arrow f g f hom-retraction-retract-arrow inclusion-retract-arrow) + ( comp-hom-arrow f g f + ( hom-retraction-retract-arrow) + ( inclusion-retract-arrow)) ( id-hom-arrow) ( is-retraction-hom-retraction-retract-arrow) @@ -260,7 +266,9 @@ module _ ( map-codomain-hom-retraction-retract-arrow) is-retraction-map-codomain-hom-retraction-retract-arrow = htpy-codomain-htpy-hom-arrow f f - ( comp-hom-arrow f g f hom-retraction-retract-arrow inclusion-retract-arrow) + ( comp-hom-arrow f g f + ( hom-retraction-retract-arrow) + ( inclusion-retract-arrow)) ( id-hom-arrow) ( is-retraction-hom-retraction-retract-arrow) @@ -280,7 +288,9 @@ module _ ( is-retraction-map-codomain-hom-retraction-retract-arrow) coh-retract-arrow = coh-htpy-hom-arrow f f - ( comp-hom-arrow f g f hom-retraction-retract-arrow inclusion-retract-arrow) + ( comp-hom-arrow f g f + ( hom-retraction-retract-arrow) + ( inclusion-retract-arrow)) ( id-hom-arrow) ( is-retraction-hom-retraction-retract-arrow) ``` @@ -659,7 +669,8 @@ module _ ( inclusion-fiber f) ( inclusion-fiber f) ( tr-hom-arrow-inclusion-fiber f - ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R b)) + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R + ( b))) ( hom-arrow-fiber f f ( comp-hom-arrow f g f ( hom-retraction-retract-arrow f g R) @@ -734,7 +745,9 @@ module _ ( precomp f S) ( hom-retraction-precomp-retract-arrow)) is-retraction-map-domain-precomp-retract-arrow = - htpy-precomp (is-retraction-map-codomain-hom-retraction-retract-arrow f g R) S + htpy-precomp + ( is-retraction-map-codomain-hom-retraction-retract-arrow f g R) + ( S) is-retraction-map-codomain-precomp-retract-arrow : is-retraction @@ -802,7 +815,8 @@ module _ pr2 retraction-precomp-retract-arrow = is-retraction-hom-retraction-precomp-retract-arrow - retract-arrow-precomp-retract-arrow : (precomp f S) retract-of-arrow (precomp g S) + retract-arrow-precomp-retract-arrow : + (precomp f S) retract-of-arrow (precomp g S) pr1 retract-arrow-precomp-retract-arrow = inclusion-precomp-retract-arrow pr2 retract-arrow-precomp-retract-arrow = retraction-precomp-retract-arrow ``` @@ -819,7 +833,8 @@ module _ inclusion-postcomp-retract-arrow = postcomp-hom-arrow f g (inclusion-retract-arrow f g R) S - hom-retraction-postcomp-retract-arrow : hom-arrow (postcomp S g) (postcomp S f) + hom-retraction-postcomp-retract-arrow : + hom-arrow (postcomp S g) (postcomp S f) hom-retraction-postcomp-retract-arrow = postcomp-hom-arrow g f (hom-retraction-retract-arrow f g R) S @@ -834,7 +849,8 @@ module _ ( postcomp S f) ( hom-retraction-postcomp-retract-arrow)) is-retraction-map-domain-postcomp-retract-arrow = - htpy-postcomp S (is-retraction-map-domain-hom-retraction-retract-arrow f g R) + htpy-postcomp S + ( is-retraction-map-domain-hom-retraction-retract-arrow f g R) is-retraction-map-codomain-postcomp-retract-arrow : is-retraction diff --git a/src/foundation/univalent-type-families.lagda.md b/src/foundation/univalent-type-families.lagda.md index f41ed1df943..845198b0a17 100644 --- a/src/foundation/univalent-type-families.lagda.md +++ b/src/foundation/univalent-type-families.lagda.md @@ -19,7 +19,6 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.global-subuniverses open import foundation.identity-systems open import foundation.iterated-dependent-product-types -open import foundation.monomorphisms open import foundation.propositions open import foundation.retractions open import foundation.subtype-identity-principle From 8c2372375faeb9ae960569a78c17e1b84f6b731c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 8 Dec 2025 20:16:11 +0000 Subject: [PATCH 3/8] imports of `equivalences-arrows` --- src/foundation/composition-spans.lagda.md | 2 +- src/foundation/equivalences-double-arrows.lagda.md | 7 ++++--- src/foundation/equivalences-span-diagrams.lagda.md | 2 +- src/foundation/fibered-equivalences.lagda.md | 2 +- .../horizontal-composition-spans-of-spans.lagda.md | 2 +- src/foundation/mere-path-cosplit-maps.lagda.md | 2 +- src/foundation/morphisms-arrows.lagda.md | 2 +- src/foundation/operations-span-diagrams.lagda.md | 7 ++++--- src/foundation/operations-spans.lagda.md | 4 ++-- src/foundation/path-cosplit-maps.lagda.md | 2 +- .../vertical-composition-spans-of-spans.lagda.md | 2 +- .../connected-maps-at-subuniverses.lagda.md | 2 +- .../types-colocal-at-maps.lagda.md | 2 +- .../cartesian-morphisms-polynomial-endofunctors.lagda.md | 2 +- 14 files changed, 21 insertions(+), 19 deletions(-) diff --git a/src/foundation/composition-spans.lagda.md b/src/foundation/composition-spans.lagda.md index 2611cdf5b1f..68f79b272ff 100644 --- a/src/foundation/composition-spans.lagda.md +++ b/src/foundation/composition-spans.lagda.md @@ -10,7 +10,6 @@ module foundation.composition-spans where open import foundation.commuting-triangles-of-maps open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.equivalences-arrows open import foundation.equivalences-spans open import foundation.homotopies open import foundation.identity-types @@ -22,6 +21,7 @@ open import foundation.standard-pullbacks open import foundation.type-arithmetic-standard-pullbacks open import foundation.universe-levels +open import foundation-core.equivalences-arrows open import foundation-core.function-types ``` diff --git a/src/foundation/equivalences-double-arrows.lagda.md b/src/foundation/equivalences-double-arrows.lagda.md index 54c7f508e0d..d5b83f68c03 100644 --- a/src/foundation/equivalences-double-arrows.lagda.md +++ b/src/foundation/equivalences-double-arrows.lagda.md @@ -12,10 +12,11 @@ open import foundation.commuting-squares-of-maps open import foundation.dependent-pair-types open import foundation.double-arrows open import foundation.equivalences -open import foundation.equivalences-arrows open import foundation.homotopies open import foundation.morphisms-double-arrows open import foundation.universe-levels + +open import foundation-core.equivalences-arrows ```
@@ -45,8 +46,8 @@ referred to as the _domain equivalence_, and the `j` as the _codomain equivalence_. Alternatively, an equivalence of double arrows is a pair of -[equivalences of arrows](foundation.equivalences-arrows.md) `f ≃ h` and `g ≃ k` -that share the underlying maps. +[equivalences of arrows](foundation-core.equivalences-arrows.md) `f ≃ h` and +`g ≃ k` that share the underlying maps. ## Definitions diff --git a/src/foundation/equivalences-span-diagrams.lagda.md b/src/foundation/equivalences-span-diagrams.lagda.md index 92238d6cff9..83c132a950f 100644 --- a/src/foundation/equivalences-span-diagrams.lagda.md +++ b/src/foundation/equivalences-span-diagrams.lagda.md @@ -10,7 +10,6 @@ module foundation.equivalences-span-diagrams where open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.equivalences-arrows open import foundation.equivalences-spans open import foundation.fundamental-theorem-of-identity-types open import foundation.morphisms-span-diagrams @@ -24,6 +23,7 @@ open import foundation.univalence open import foundation.universe-levels open import foundation-core.commuting-squares-of-maps +open import foundation-core.equivalences-arrows open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import foundation-core.torsorial-type-families diff --git a/src/foundation/fibered-equivalences.lagda.md b/src/foundation/fibered-equivalences.lagda.md index 3d899df149c..0f0651ceff8 100644 --- a/src/foundation/fibered-equivalences.lagda.md +++ b/src/foundation/fibered-equivalences.lagda.md @@ -395,5 +395,5 @@ module _ ## See also -- [Equivalences of arrows](foundation.equivalences-arrows.md) for the same +- [Equivalences of arrows](foundation-core.equivalences-arrows.md) for the same concept under a different name. diff --git a/src/foundation/horizontal-composition-spans-of-spans.lagda.md b/src/foundation/horizontal-composition-spans-of-spans.lagda.md index eed15671157..4ec5e8622ea 100644 --- a/src/foundation/horizontal-composition-spans-of-spans.lagda.md +++ b/src/foundation/horizontal-composition-spans-of-spans.lagda.md @@ -12,7 +12,6 @@ open import foundation.composition-spans open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.equivalences-arrows open import foundation.equivalences-spans open import foundation.homotopies open import foundation.identity-types @@ -26,6 +25,7 @@ open import foundation.type-arithmetic-standard-pullbacks open import foundation.universe-levels open import foundation.whiskering-homotopies-composition +open import foundation-core.equivalences-arrows open import foundation-core.function-types ``` diff --git a/src/foundation/mere-path-cosplit-maps.lagda.md b/src/foundation/mere-path-cosplit-maps.lagda.md index a32550ef062..3bf95ad14f3 100644 --- a/src/foundation/mere-path-cosplit-maps.lagda.md +++ b/src/foundation/mere-path-cosplit-maps.lagda.md @@ -9,7 +9,6 @@ module foundation.mere-path-cosplit-maps where ```agda open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types -open import foundation.equivalences-arrows open import foundation.functoriality-propositional-truncation open import foundation.inhabited-types open import foundation.iterated-dependent-product-types @@ -22,6 +21,7 @@ open import foundation.universe-levels open import foundation-core.contractible-maps open import foundation-core.contractible-types open import foundation-core.equivalences +open import foundation-core.equivalences-arrows open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.propositions diff --git a/src/foundation/morphisms-arrows.lagda.md b/src/foundation/morphisms-arrows.lagda.md index 0c53c53eb76..0f14fc5117a 100644 --- a/src/foundation/morphisms-arrows.lagda.md +++ b/src/foundation/morphisms-arrows.lagda.md @@ -430,7 +430,7 @@ module _ ## See also -- [Equivalences of arrows](foundation.equivalences-arrows.md) +- [Equivalences of arrows](foundation-core.equivalences-arrows.md) - [Morphisms of twisted arrows](foundation.morphisms-twisted-arrows.md). - [Fibered maps](foundation.fibered-maps.md) for the same concept under a different name. diff --git a/src/foundation/operations-span-diagrams.lagda.md b/src/foundation/operations-span-diagrams.lagda.md index 9337e9f12a3..1571a61cce7 100644 --- a/src/foundation/operations-span-diagrams.lagda.md +++ b/src/foundation/operations-span-diagrams.lagda.md @@ -10,11 +10,12 @@ open import foundation-core.operations-span-diagrams public ```agda open import foundation.dependent-pair-types -open import foundation.equivalences-arrows open import foundation.operations-spans open import foundation.span-diagrams open import foundation.spans open import foundation.universe-levels + +open import foundation-core.equivalences-arrows ```
@@ -38,7 +39,7 @@ Consider a span diagram `𝒮` given by A <----- S -----> B ``` -and an [equivalence of arrows](foundation.equivalences-arrows.md) +and an [equivalence of arrows](foundation-core.equivalences-arrows.md) `h : equiv-arrow f' f` as indicated in the diagram ```text @@ -107,7 +108,7 @@ Consider a span diagram `𝒮` given by A <----- S -----> B ``` -and a [equivalence of arrows](foundation.equivalences-arrows.md) +and a [equivalence of arrows](foundation-core.equivalences-arrows.md) `h : equiv-arrow g' g` as indicated in the diagram ```text diff --git a/src/foundation/operations-spans.lagda.md b/src/foundation/operations-spans.lagda.md index 6562513941e..ff5f6880765 100644 --- a/src/foundation/operations-spans.lagda.md +++ b/src/foundation/operations-spans.lagda.md @@ -10,11 +10,11 @@ open import foundation-core.operations-spans public ```agda open import foundation.dependent-pair-types -open import foundation.equivalences-arrows open import foundation.morphisms-arrows open import foundation.spans open import foundation.universe-levels +open import foundation-core.equivalences-arrows open import foundation-core.function-types ``` @@ -38,7 +38,7 @@ Consider a span `s` given by A <----- S -----> B ``` -and an [equivalence of arrows](foundation.equivalences-arrows.md) +and an [equivalence of arrows](foundation-core.equivalences-arrows.md) `h : equiv-arrow f' f` as indicated in the diagram ```text diff --git a/src/foundation/path-cosplit-maps.lagda.md b/src/foundation/path-cosplit-maps.lagda.md index 3d9de9f6984..b72a69f1155 100644 --- a/src/foundation/path-cosplit-maps.lagda.md +++ b/src/foundation/path-cosplit-maps.lagda.md @@ -17,7 +17,6 @@ open import foundation.empty-types open import foundation.equality-cartesian-product-types open import foundation.equality-coproduct-types open import foundation.equality-dependent-pair-types -open import foundation.equivalences-arrows open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-action-on-identifications-functions @@ -47,6 +46,7 @@ open import foundation-core.contractible-maps open import foundation-core.contractible-types open import foundation-core.embeddings open import foundation-core.equivalences +open import foundation-core.equivalences-arrows open import foundation-core.homotopies open import foundation-core.injective-maps open import foundation-core.propositions diff --git a/src/foundation/vertical-composition-spans-of-spans.lagda.md b/src/foundation/vertical-composition-spans-of-spans.lagda.md index 785b4827451..9eaf32e217b 100644 --- a/src/foundation/vertical-composition-spans-of-spans.lagda.md +++ b/src/foundation/vertical-composition-spans-of-spans.lagda.md @@ -11,7 +11,6 @@ open import foundation.commuting-triangles-of-maps open import foundation.composition-spans open import foundation.dependent-pair-types open import foundation.equivalences -open import foundation.equivalences-arrows open import foundation.equivalences-spans open import foundation.homotopies open import foundation.identity-types @@ -25,6 +24,7 @@ open import foundation.type-arithmetic-standard-pullbacks open import foundation.universe-levels open import foundation.whiskering-homotopies-composition +open import foundation-core.equivalences-arrows open import foundation-core.function-types ``` diff --git a/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md b/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md index a1145d14e79..666a1c72980 100644 --- a/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/connected-maps-at-subuniverses.lagda.md @@ -13,7 +13,6 @@ open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.dependent-universal-property-equivalences open import foundation.equivalences -open import foundation.equivalences-arrows open import foundation.function-extensionality open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-coproduct-types @@ -39,6 +38,7 @@ open import foundation.universe-levels open import foundation-core.contractible-maps open import foundation-core.embeddings +open import foundation-core.equivalences-arrows open import foundation-core.fibers-of-maps open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types diff --git a/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md b/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md index ecccffcc352..ae60e287ae6 100644 --- a/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/types-colocal-at-maps.lagda.md @@ -14,7 +14,6 @@ open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.equivalences -open import foundation.equivalences-arrows open import foundation.function-extensionality open import foundation.function-types open import foundation.homotopies @@ -30,6 +29,7 @@ open import foundation.universal-property-equivalences open import foundation.universe-levels open import foundation.whiskering-homotopies-composition +open import foundation-core.equivalences-arrows open import foundation-core.fibers-of-maps ``` diff --git a/src/trees/cartesian-morphisms-polynomial-endofunctors.lagda.md b/src/trees/cartesian-morphisms-polynomial-endofunctors.lagda.md index bc400925adf..4d7d05d893d 100644 --- a/src/trees/cartesian-morphisms-polynomial-endofunctors.lagda.md +++ b/src/trees/cartesian-morphisms-polynomial-endofunctors.lagda.md @@ -17,7 +17,6 @@ open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types open import foundation.equivalences -open import foundation.equivalences-arrows open import foundation.fibers-of-maps open import foundation.function-types open import foundation.functoriality-dependent-function-types @@ -47,6 +46,7 @@ open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation-core.equality-dependent-pair-types +open import foundation-core.equivalences-arrows open import foundation-core.retractions open import foundation-core.torsorial-type-families From 9bba892ecb72086285ab38c117be5b372e7684cb Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 8 Dec 2025 20:56:45 +0000 Subject: [PATCH 4/8] split monomorphisms and optimize imports --- src/foundation-core.lagda.md | 1 + src/foundation-core/monomorphisms.lagda.md | 161 +++++++++++++++++ src/foundation/monomorphisms.lagda.md | 168 +++--------------- .../postcomposition-extensions-maps.lagda.md | 3 +- 4 files changed, 191 insertions(+), 142 deletions(-) create mode 100644 src/foundation-core/monomorphisms.lagda.md diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index f08a3e2fe06..a070b97d8c2 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -39,6 +39,7 @@ open import foundation-core.identity-types public open import foundation-core.injective-maps public open import foundation-core.invertible-maps public open import foundation-core.iterating-functions public +open import foundation-core.monomorphisms public open import foundation-core.negation public open import foundation-core.operations-span-diagrams public open import foundation-core.operations-spans public diff --git a/src/foundation-core/monomorphisms.lagda.md b/src/foundation-core/monomorphisms.lagda.md new file mode 100644 index 00000000000..280c0355e7e --- /dev/null +++ b/src/foundation-core/monomorphisms.lagda.md @@ -0,0 +1,161 @@ +# Monomorphisms + +```agda +module foundation-core.monomorphisms where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.function-extensionality +open import foundation.functoriality-function-types +open import foundation.postcomposition-functions +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition + +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.propositional-maps +open import foundation-core.propositions +open import foundation-core.retractions +open import foundation-core.sections +open import foundation-core.truncation-levels +``` + +
+ +## Idea + +A function `f : A → B` is a +{{#concept "monomorphism" Disambiguation="of types" Agda=is-mono}} if whenever +we have two functions `g h : X → A` such that `f ∘ g = f ∘ h`, then in fact +`g = h`. The correct way to state this in Homotopy Type Theory is to say that +[postcomposition](foundation-core.postcomposition-functions.md) by `f` is an +[embedding](foundation-core.embeddings.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} (l3 : Level) + {A : UU l1} {B : UU l2} (f : A → B) + where + + is-mono-Prop : Prop (l1 ⊔ l2 ⊔ lsuc l3) + is-mono-Prop = Π-Prop (UU l3) (λ X → is-emb-Prop (postcomp X f)) + + is-mono : UU (l1 ⊔ l2 ⊔ lsuc l3) + is-mono = type-Prop is-mono-Prop + + is-prop-is-mono : is-prop is-mono + is-prop-is-mono = is-prop-type-Prop is-mono-Prop +``` + +## Properties + +If `f : A → B` is a monomorphism then for any `g h : X → A` we have an +equivalence `(f ∘ g = f ∘ h) ≃ (g = h)`. In particular, if `f ∘ g = f ∘ h` then +`g = h`. + +```agda +module _ + {l1 l2 : Level} (l3 : Level) + {A : UU l1} {B : UU l2} (f : A → B) + (p : is-mono l3 f) {X : UU l3} (g h : X → A) + where + + equiv-postcomp-is-mono : (g ＝ h) ≃ (f ∘ g ＝ f ∘ h) + pr1 equiv-postcomp-is-mono = ap (f ∘_) + pr2 equiv-postcomp-is-mono = p X g h + + is-injective-postcomp-is-mono : f ∘ g ＝ f ∘ h → g ＝ h + is-injective-postcomp-is-mono = map-inv-equiv equiv-postcomp-is-mono +``` + +A function is a monomorphism if and only if it is an embedding. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + is-mono-is-emb : is-emb f → {l3 : Level} → is-mono l3 f + is-mono-is-emb is-emb-f X = + is-emb-is-prop-map + ( is-trunc-map-postcomp-is-trunc-map neg-one-𝕋 f + ( is-prop-map-is-emb is-emb-f) + ( X)) + + is-emb-is-mono-lzero : is-mono lzero f → is-emb f + is-emb-is-mono-lzero is-mono-f = + is-emb-is-prop-map + ( is-trunc-map-is-trunc-map-postcomp-lzero neg-one-𝕋 f + ( λ X → is-prop-map-is-emb (is-mono-f X))) + + is-emb-is-mono : ({l3 : Level} → is-mono l3 f) → is-emb f + is-emb-is-mono is-mono-f = + is-emb-is-mono-lzero is-mono-f + + equiv-postcomp-is-emb : + is-emb f → + {l3 : Level} {X : UU l3} (g h : X → A) → (g ＝ h) ≃ (f ∘ g ＝ f ∘ h) + equiv-postcomp-is-emb H {l3} = equiv-postcomp-is-mono l3 f (is-mono-is-emb H) + +equiv-postcomp-emb : + {l1 l2 l3 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} + (f : A ↪ B) (g h : X → A) → + (g ＝ h) ≃ (map-emb f ∘ g ＝ map-emb f ∘ h) +equiv-postcomp-emb (f , H) = equiv-postcomp-is-emb f H +``` + +We construct an explicit equivalence for postcomposition for homotopies between +functions (rather than equality) when the map is an embedding. + +```agda +module _ + {l1 l2 l3 : Level} + {A : UU l1} {B : UU l2} (f : A ↪ B) + {X : UU l3} (g h : X → A) + where + + map-inv-equiv-htpy-postcomp-emb : + map-emb f ∘ g ~ map-emb f ∘ h → g ~ h + map-inv-equiv-htpy-postcomp-emb H x = + map-inv-is-equiv (is-emb-map-emb f (g x) (h x)) (H x) + + is-section-map-inv-equiv-htpy-postcomp-emb : + is-section + ( left-whisker-comp (map-emb f)) + ( map-inv-equiv-htpy-postcomp-emb) + is-section-map-inv-equiv-htpy-postcomp-emb H = + eq-htpy + ( λ x → is-section-map-inv-is-equiv (is-emb-map-emb f (g x) (h x)) (H x)) + + is-retraction-map-inv-equiv-htpy-postcomp-emb : + is-retraction + ( left-whisker-comp (map-emb f)) + ( map-inv-equiv-htpy-postcomp-emb) + is-retraction-map-inv-equiv-htpy-postcomp-emb H = + eq-htpy + ( λ x → + is-retraction-map-inv-is-equiv (is-emb-map-emb f (g x) (h x)) (H x)) + + is-equiv-left-whisker-emb : + is-equiv (left-whisker-comp (map-emb f) {g} {h}) + is-equiv-left-whisker-emb = + is-equiv-is-invertible + map-inv-equiv-htpy-postcomp-emb + is-section-map-inv-equiv-htpy-postcomp-emb + is-retraction-map-inv-equiv-htpy-postcomp-emb + + equiv-htpy-postcomp-emb : + (g ~ h) ≃ (map-emb f ∘ g ~ map-emb f ∘ h) + equiv-htpy-postcomp-emb = + ( left-whisker-comp (map-emb f) , is-equiv-left-whisker-emb) +``` diff --git a/src/foundation/monomorphisms.lagda.md b/src/foundation/monomorphisms.lagda.md index 3081d989b80..7bd863d82ff 100644 --- a/src/foundation/monomorphisms.lagda.md +++ b/src/foundation/monomorphisms.lagda.md @@ -2,31 +2,24 @@ ```agda module foundation.monomorphisms where + +open import foundation-core.monomorphisms public ```
Imports ```agda -open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.embeddings -open import foundation.function-extensionality -open import foundation.functoriality-function-types open import foundation.logical-equivalences open import foundation.postcomposition-functions +open import foundation.precomposition-functions +open import foundation.raising-universe-levels +open import foundation.universal-property-equivalences open import foundation.universe-levels -open import foundation.whiskering-homotopies-composition open import foundation-core.equivalences -open import foundation-core.equivalences-arrows -open import foundation-core.function-types open import foundation-core.homotopies -open import foundation-core.identity-types -open import foundation-core.propositional-maps -open import foundation-core.propositions -open import foundation-core.retractions -open import foundation-core.sections -open import foundation-core.truncation-levels ```
@@ -40,141 +33,34 @@ we have two functions `g h : X → A` such that `f ∘ g = f ∘ h`, then in fac [postcomposition](foundation-core.postcomposition-functions.md) by `f` is an [embedding](foundation-core.embeddings.md). -## Definition - -```agda -module _ - {l1 l2 : Level} (l3 : Level) - {A : UU l1} {B : UU l2} (f : A → B) - where - - is-mono-Prop : Prop (l1 ⊔ l2 ⊔ lsuc l3) - is-mono-Prop = Π-Prop (UU l3) (λ X → is-emb-Prop (postcomp X f)) - - is-mono : UU (l1 ⊔ l2 ⊔ lsuc l3) - is-mono = type-Prop is-mono-Prop - - is-prop-is-mono : is-prop is-mono - is-prop-is-mono = is-prop-type-Prop is-mono-Prop -``` - ## Properties -If `f : A → B` is a monomorphism then for any `g h : X → A` we have an -equivalence `(f ∘ g = f ∘ h) ≃ (g = h)`. In particular, if `f ∘ g = f ∘ h` then -`g = h`. - -```agda -module _ - {l1 l2 : Level} (l3 : Level) - {A : UU l1} {B : UU l2} (f : A → B) - (p : is-mono l3 f) {X : UU l3} (g h : X → A) - where - - equiv-postcomp-is-mono : (g ＝ h) ≃ (f ∘ g ＝ f ∘ h) - pr1 equiv-postcomp-is-mono = ap (f ∘_) - pr2 equiv-postcomp-is-mono = p X g h - - is-injective-postcomp-is-mono : f ∘ g ＝ f ∘ h → g ＝ h - is-injective-postcomp-is-mono = map-inv-equiv equiv-postcomp-is-mono -``` - -A function is a monomorphism if and only if it is an embedding. - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) - where - - is-mono-is-emb : is-emb f → {l3 : Level} → is-mono l3 f - is-mono-is-emb is-emb-f X = - is-emb-is-prop-map - ( is-trunc-map-postcomp-is-trunc-map neg-one-𝕋 f - ( is-prop-map-is-emb is-emb-f) - ( X)) - - is-emb-is-mono-lzero : is-mono lzero f → is-emb f - is-emb-is-mono-lzero is-mono-f = - is-emb-is-prop-map - ( is-trunc-map-is-trunc-map-postcomp-lzero neg-one-𝕋 f - ( λ X → is-prop-map-is-emb (is-mono-f X))) - - is-emb-is-mono : ({l3 : Level} → is-mono l3 f) → is-emb f - is-emb-is-mono is-mono-f = - is-emb-is-mono-lzero is-mono-f - - equiv-postcomp-is-emb : - is-emb f → - {l3 : Level} {X : UU l3} (g h : X → A) → (g ＝ h) ≃ (f ∘ g ＝ f ∘ h) - equiv-postcomp-is-emb H {l3} = equiv-postcomp-is-mono l3 f (is-mono-is-emb H) - -equiv-postcomp-emb : - {l1 l2 l3 : Level} - {A : UU l1} {B : UU l2} {X : UU l3} - (f : A ↪ B) (g h : X → A) → - (g ＝ h) ≃ (map-emb f ∘ g ＝ map-emb f ∘ h) -equiv-postcomp-emb (f , H) = equiv-postcomp-is-emb f H -``` - -We construct an explicit equivalence for postcomposition for homotopies between -functions (rather than equality) when the map is an embedding. - -```agda -module _ - {l1 l2 l3 : Level} - {A : UU l1} {B : UU l2} (f : A ↪ B) - {X : UU l3} (g h : X → A) - where - - map-inv-equiv-htpy-postcomp-emb : - map-emb f ∘ g ~ map-emb f ∘ h → g ~ h - map-inv-equiv-htpy-postcomp-emb H x = - map-inv-is-equiv (is-emb-map-emb f (g x) (h x)) (H x) - - is-section-map-inv-equiv-htpy-postcomp-emb : - is-section - ( left-whisker-comp (map-emb f)) - ( map-inv-equiv-htpy-postcomp-emb) - is-section-map-inv-equiv-htpy-postcomp-emb H = - eq-htpy - ( λ x → is-section-map-inv-is-equiv (is-emb-map-emb f (g x) (h x)) (H x)) - - is-retraction-map-inv-equiv-htpy-postcomp-emb : - is-retraction - ( left-whisker-comp (map-emb f)) - ( map-inv-equiv-htpy-postcomp-emb) - is-retraction-map-inv-equiv-htpy-postcomp-emb H = - eq-htpy - ( λ x → - is-retraction-map-inv-is-equiv (is-emb-map-emb f (g x) (h x)) (H x)) - - is-equiv-left-whisker-emb : - is-equiv (left-whisker-comp (map-emb f) {g} {h}) - is-equiv-left-whisker-emb = - is-equiv-is-invertible - map-inv-equiv-htpy-postcomp-emb - is-section-map-inv-equiv-htpy-postcomp-emb - is-retraction-map-inv-equiv-htpy-postcomp-emb - - equiv-htpy-postcomp-emb : - (g ~ h) ≃ (map-emb f ∘ g ~ map-emb f ∘ h) - equiv-htpy-postcomp-emb = - ( left-whisker-comp (map-emb f) , is-equiv-left-whisker-emb) -``` - ### Smallness of the mono predicate -In order to avoid cyclic dependencies, we need to type out the definition of -being small. - -```text +```agda module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) where - is-small-lzero-is-mono : - {l3 : Level} → Σ (UU (lsuc lzero ⊔ l1 ⊔ l2)) (λ P → is-mono l3 f ≃ P) - is-small-lzero-is-mono {l3} = - ( is-mono lzero f , - equiv-iff (is-mono-Prop l3 f) (is-mono-Prop lzero f) (λ X H → {! i !}) {! !}) + is-mono-is-mono-lub : (l3 l4 : Level) → is-mono (l3 ⊔ l4) f → is-mono l3 f + is-mono-is-mono-lub l3 l4 H X = + is-emb-bottom-is-emb-top-is-equiv-coherence-square-maps + ( postcomp (raise l4 X) f) + ( precomp map-raise A) + ( precomp map-raise B) + ( postcomp X f) + ( refl-htpy) + ( is-equiv-precomp-is-equiv map-raise is-equiv-map-raise A) + ( is-equiv-precomp-is-equiv map-raise is-equiv-map-raise B) + ( H (raise l4 X)) + + is-small-is-mono : + {l3 : Level} → Σ (UU (l1 ⊔ l2)) (λ P → is-mono l3 f ≃ P) + is-small-is-mono {l3} = + ( is-emb f , + equiv-iff + ( is-mono-Prop l3 f) + ( is-emb-Prop f) + ( λ H → is-emb-is-mono-lzero f (is-mono-is-mono-lub lzero l3 H)) + ( λ H → is-mono-is-emb f H)) ``` diff --git a/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md index 1de516712d0..a13433b2d44 100644 --- a/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md +++ b/src/orthogonal-factorization-systems/postcomposition-extensions-maps.lagda.md @@ -15,13 +15,14 @@ open import foundation.function-types open import foundation.functoriality-dependent-function-types open import foundation.functoriality-dependent-pair-types open import foundation.functoriality-function-types -open import foundation.monomorphisms open import foundation.postcomposition-functions open import foundation.truncated-maps open import foundation.truncation-levels open import foundation.universe-levels open import foundation.whiskering-homotopies-composition +open import foundation-core.monomorphisms + open import orthogonal-factorization-systems.extensions-maps ``` From 5a0ab5c8841722e9f2cbdc2fe78929454c80949c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 9 Dec 2025 16:35:47 +0000 Subject: [PATCH 5/8] modularize --- src/foundation/monomorphisms.lagda.md | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/src/foundation/monomorphisms.lagda.md b/src/foundation/monomorphisms.lagda.md index 7bd863d82ff..7db7012e0e0 100644 --- a/src/foundation/monomorphisms.lagda.md +++ b/src/foundation/monomorphisms.lagda.md @@ -20,6 +20,7 @@ open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.homotopies +open import foundation-core.small-types ``` @@ -54,13 +55,20 @@ module _ ( is-equiv-precomp-is-equiv map-raise is-equiv-map-raise B) ( H (raise l4 X)) - is-small-is-mono : - {l3 : Level} → Σ (UU (l1 ⊔ l2)) (λ P → is-mono l3 f ≃ P) - is-small-is-mono {l3} = - ( is-emb f , - equiv-iff - ( is-mono-Prop l3 f) - ( is-emb-Prop f) - ( λ H → is-emb-is-mono-lzero f (is-mono-is-mono-lub lzero l3 H)) - ( λ H → is-mono-is-emb f H)) + is-emb-is-mono-Level : {l3 : Level} → is-mono l3 f → is-emb f + is-emb-is-mono-Level {l3} H = + is-emb-is-mono-lzero f (is-mono-is-mono-lub lzero l3 H) + + is-emb-iff-is-mono : {l3 : Level} → is-mono l3 f ↔ is-emb f + is-emb-iff-is-mono = (is-emb-is-mono-Level , (λ H → is-mono-is-emb f H)) + + equiv-is-emb-is-mono : {l3 : Level} → is-mono l3 f ≃ is-emb f + equiv-is-emb-is-mono {l3} = + equiv-iff' + ( is-mono-Prop l3 f) + ( is-emb-Prop f) + ( is-emb-iff-is-mono) + + is-small-is-mono : {l3 : Level} → is-small (l1 ⊔ l2) (is-mono l3 f) + is-small-is-mono = (is-emb f , equiv-is-emb-is-mono) ``` From ad5682f6b52cca2b545e2d9f3615955494cd71ae Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 9 Dec 2025 16:35:57 +0000 Subject: [PATCH 6/8] typos in `synthetic-homotopy-theory.dependent-pushout-products` --- .../dependent-pushout-products.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md b/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md index 265ce6a2c99..77af3c8b4c1 100644 --- a/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md +++ b/src/synthetic-homotopy-theory/dependent-pushout-products.lagda.md @@ -25,7 +25,7 @@ open import synthetic-homotopy-theory.universal-property-pushouts The **dependent pushout-product** is a generalization of the [pushout-product](synthetic-homotopy-theory.pushout-products.md). Consider a map -`f : A → B` and a family of maps `g : (x : X) → B x → Y x`. The **dependent +`f : A → X` and a family of maps `g : (x : X) → B x → Y x`. The **dependent pushout-product** is the [cogap map](synthetic-homotopy-theory.pushouts.md) of the [commuting square](foundation-core.commuting-squares-of-maps.md) @@ -39,7 +39,7 @@ the [commuting square](foundation-core.commuting-squares-of-maps.md) Σ f id ``` -The [fiber](foundation-core.fibers-of-maps.md) of the dependent pushout product +The [fiber](foundation-core.fibers-of-maps.md) of the dependent pushout-product at `(x , y)` is [equivalent](foundation-core.equivalences.md) to the join of fibers From fd903cbde510f81fa14b78f2d3ce85d282a90ece Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 9 Dec 2025 16:37:20 +0000 Subject: [PATCH 7/8] remove linebreak --- src/foundation/monomorphisms.lagda.md | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/foundation/monomorphisms.lagda.md b/src/foundation/monomorphisms.lagda.md index 7db7012e0e0..9e37833ea6d 100644 --- a/src/foundation/monomorphisms.lagda.md +++ b/src/foundation/monomorphisms.lagda.md @@ -64,10 +64,7 @@ module _ equiv-is-emb-is-mono : {l3 : Level} → is-mono l3 f ≃ is-emb f equiv-is-emb-is-mono {l3} = - equiv-iff' - ( is-mono-Prop l3 f) - ( is-emb-Prop f) - ( is-emb-iff-is-mono) + equiv-iff' (is-mono-Prop l3 f) (is-emb-Prop f) (is-emb-iff-is-mono) is-small-is-mono : {l3 : Level} → is-small (l1 ⊔ l2) (is-mono l3 f) is-small-is-mono = (is-emb f , equiv-is-emb-is-mono) From f0a6438fceacdd3dfe2e5727391182e3297769e7 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 10 Dec 2025 17:50:20 +0000 Subject: [PATCH 8/8] edit a proof --- ...toriality-cartesian-product-types.lagda.md | 52 +++++++++++-------- 1 file changed, 30 insertions(+), 22 deletions(-) diff --git a/src/foundation/functoriality-cartesian-product-types.lagda.md b/src/foundation/functoriality-cartesian-product-types.lagda.md index 6c4ad9ae0af..128fb80cf1e 100644 --- a/src/foundation/functoriality-cartesian-product-types.lagda.md +++ b/src/foundation/functoriality-cartesian-product-types.lagda.md @@ -262,35 +262,43 @@ module _ (f : A → C) (g : B → D) where + is-contr-map-left-factor-is-contr-map-map-product' : + D → is-contr-map (map-product f g) → is-contr-map f + is-contr-map-left-factor-is-contr-map-map-product' d is-contr-map-fg x = + is-contr-left-factor-product + ( fiber f x) + ( fiber g d) + ( is-contr-is-equiv' + ( fiber (map-product f g) (x , d)) + ( map-compute-fiber-map-product f g (x , d)) + ( is-equiv-map-compute-fiber-map-product f g (x , d)) + ( is-contr-map-fg (x , d))) + is-equiv-left-factor-is-equiv-map-product' : D → is-equiv (map-product f g) → is-equiv f - is-equiv-left-factor-is-equiv-map-product' - d is-equiv-fg = + is-equiv-left-factor-is-equiv-map-product' d is-equiv-fg = is-equiv-is-contr-map - ( λ x → - is-contr-left-factor-product - ( fiber f x) - ( fiber g d) - ( is-contr-is-equiv' - ( fiber (map-product f g) (x , d)) - ( map-compute-fiber-map-product f g (x , d)) - ( is-equiv-map-compute-fiber-map-product f g (x , d)) - ( is-contr-map-is-equiv is-equiv-fg (x , d)))) + ( is-contr-map-left-factor-is-contr-map-map-product' d + ( is-contr-map-is-equiv is-equiv-fg)) + + is-contr-map-right-factor-is-contr-map-map-product' : + C → is-contr-map (map-product f g) → is-contr-map g + is-contr-map-right-factor-is-contr-map-map-product' c is-contr-map-fg y = + is-contr-right-factor-product + ( fiber f c) + ( fiber g y) + ( is-contr-is-equiv' + ( fiber (map-product f g) (c , y)) + ( map-compute-fiber-map-product f g (c , y)) + ( is-equiv-map-compute-fiber-map-product f g (c , y)) + ( is-contr-map-fg (c , y))) is-equiv-right-factor-is-equiv-map-product' : C → is-equiv (map-product f g) → is-equiv g - is-equiv-right-factor-is-equiv-map-product' - c is-equiv-fg = + is-equiv-right-factor-is-equiv-map-product' c is-equiv-fg = is-equiv-is-contr-map - ( λ y → - is-contr-right-factor-product - ( fiber f c) - ( fiber g y) - ( is-contr-is-equiv' - ( fiber (map-product f g) (c , y)) - ( map-compute-fiber-map-product f g (c , y)) - ( is-equiv-map-compute-fiber-map-product f g (c , y)) - ( is-contr-map-is-equiv is-equiv-fg (c , y)))) + ( is-contr-map-right-factor-is-contr-map-map-product' c + ( is-contr-map-is-equiv is-equiv-fg)) ``` ### The functorial action of products on arrows