From f4400b1796c531efde2e8439fc6a0a49622470db Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 17 Apr 2024 12:49:49 +0200 Subject: [PATCH] Splitting idempotents (#1105) ### Summary - Retracts of a type - Define retracts of a type - Characterize equality of retracts - Weakly constant maps - The type of fixed points of weakly constant maps is a proposition - Idempotent maps - Rename "preidempotent maps" to "idempotent maps". This mirrors how we treat "invertible maps" vs "coherently invertible maps", although there is an essential difference between the two concepts: idempotent maps are not "coherentifiable" like invertible maps. That role is taken by "quasicoherently idempotent maps" instead. - Quasicoherently idempotent maps (called "quasiidempotent maps" in [Shu17]) - Define quasicoherently idempotent maps - Quasicoherently idempotent maps are closed under homotopy (without funext) - Split idempotent maps - Define split idempotent maps - Split idempotent maps are quasicoherently idempotent - Idempotent maps on sets split - Weakly constant idempotent maps split - Quasicoherently idempotent maps split - Retracts of small types are small Work towards #1103. --- references.bib | 92 +- .../natural-numbers.lagda.md | 10 + src/foundation-core.lagda.md | 1 + .../coherently-invertible-maps.lagda.md | 2 +- .../contractible-types.lagda.md | 2 +- src/foundation-core/homotopies.lagda.md | 52 + src/foundation-core/identity-types.lagda.md | 2 +- src/foundation-core/invertible-maps.lagda.md | 9 +- src/foundation-core/retractions.lagda.md | 2 +- .../retracts-of-types.lagda.md | 191 +++ src/foundation-core/small-types.lagda.md | 4 + src/foundation-core/truncated-types.lagda.md | 2 +- src/foundation.lagda.md | 5 +- .../coherently-invertible-maps.lagda.md | 5 - .../commuting-prisms-of-maps.lagda.md | 1 - .../commuting-squares-of-homotopies.lagda.md | 1 - ...commuting-triangles-of-homotopies.lagda.md | 3 - ...ting-triangles-of-identifications.lagda.md | 5 +- ...ing-triangles-of-morphisms-arrows.lagda.md | 5 - src/foundation/connected-types.lagda.md | 2 +- src/foundation/decidable-equality.lagda.md | 2 +- src/foundation/decidable-types.lagda.md | 2 +- src/foundation/equivalence-induction.lagda.md | 2 +- src/foundation/equivalences.lagda.md | 16 + .../fixed-points-endofunctions.lagda.md | 36 + .../function-extensionality.lagda.md | 1 - .../functoriality-truncation.lagda.md | 2 +- ...amental-theorem-of-identity-types.lagda.md | 2 +- src/foundation/idempotent-maps.lagda.md | 162 +++ src/foundation/identity-types.lagda.md | 24 +- src/foundation/involutions.lagda.md | 11 + src/foundation/path-algebra.lagda.md | 3 - src/foundation/preidempotent-maps.lagda.md | 49 - .../quasicoherently-idempotent-maps.lagda.md | 388 ++++++ src/foundation/retractions.lagda.md | 2 +- src/foundation/retracts-of-maps.lagda.md | 2 +- src/foundation/retracts-of-types.lagda.md | 212 +-- src/foundation/sections.lagda.md | 2 +- src/foundation/sequential-limits.lagda.md | 21 +- src/foundation/small-maps.lagda.md | 58 +- src/foundation/small-types.lagda.md | 8 +- src/foundation/split-idempotent-maps.lagda.md | 1204 +++++++++++++++++ ...tal-concatenation-identifications.lagda.md | 2 +- ...ropositional-truncation-into-sets.lagda.md | 40 +- src/foundation/weakly-constant-maps.lagda.md | 116 +- ...whiskering-homotopies-composition.lagda.md | 35 +- ...iskering-homotopies-concatenation.lagda.md | 1 - src/set-theory/cumulative-hierarchy.lagda.md | 2 +- src/synthetic-homotopy-theory/circle.lagda.md | 47 +- 49 files changed, 2548 insertions(+), 300 deletions(-) create mode 100644 src/foundation-core/retracts-of-types.lagda.md create mode 100644 src/foundation/fixed-points-endofunctions.lagda.md create mode 100644 src/foundation/idempotent-maps.lagda.md delete mode 100644 src/foundation/preidempotent-maps.lagda.md create mode 100644 src/foundation/quasicoherently-idempotent-maps.lagda.md create mode 100644 src/foundation/split-idempotent-maps.lagda.md diff --git a/references.bib b/references.bib index 6e9796dc04..7f75bb02cd 100644 --- a/references.bib +++ b/references.bib @@ -23,7 +23,6 @@ @online{BCDE21 url = {https://www.cs.bham.ac.uk/~mhe/TypeTopology/Groups.Free.html} } - @online{BCFR23, title = {Central {{H-spaces}} and Banded Types}, author = {Buchholtz, Ulrik and Christensen, J. Daniel and Flaten, Jarl G. Taxerås and Rijke, Egbert}, @@ -38,6 +37,21 @@ @online{BCFR23 keywords = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Logic} } +@online{BdJR24, + title = {Epimorphisms and {{Acyclic Types}} in {{Univalent Mathematics}}}, + author = {Buchholtz, Ulrik and {{de}} Jong, Tom and Rijke, Egbert}, + citeas = {BdJR24}, + date = {2024-01-25}, + year = {2024}, + month = {01}, + eprint = {2401.14106}, + eprinttype = {arxiv}, + eprintclass = {cs, math}, + abstract = {We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with $0$-connected, pointed $1$-types. Many of our results are formalized as part of the agda-unimath library.}, + pubstate = {preprint}, + keywords = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory} +} + @online{BDR18, title = {Higher {{Groups}} in {{Homotopy Type Theory}}}, author = {Buchholtz, Ulrik and {{van}} Doorn, Floris and Rijke, Egbert}, @@ -53,21 +67,6 @@ @online{BDR18 keywords = {03B15,Computer Science - Logic in Computer Science,F.4.1,Mathematics - Algebraic Topology,Mathematics - Logic} } -@online{BJR24, - title = {Epimorphisms and {{Acyclic Types}} in {{Univalent Mathematics}}}, - author = {Buchholtz, Ulrik and {{de}} Jong, Tom and Rijke, Egbert}, - citeas = {BJR24}, - date = {2024-01-25}, - year = {2024}, - month = {01}, - eprint = {2401.14106}, - eprinttype = {arxiv}, - eprintclass = {cs, math}, - abstract = {We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with $0$-connected, pointed $1$-types. Many of our results are formalized as part of the agda-unimath library.}, - pubstate = {preprint}, - keywords = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory} -} - @book{BSCS05, title = {Absztrakt algebrai feladatok}, author = {Bálintné Szendrei, Mária and Czédli, Gábor and Szendrei, Ágnes}, @@ -139,6 +138,40 @@ @article{CR21 keywords = {algebraic geometry,cohesive homotopy type theory,factorization systems,Homotopy type theory,modal homotopy type theory} } +@article{dJE23, + title = {{On Small Types in Univalent Foundations}}, + author = {{{de}} Jong, Tom and Escardó, Martín Hötzel}, + url = {https://lmcs.episciences.org/11270}, + doi = {10.46298/lmcs-19(2:8)2023}, + journal = {{Logical Methods in Computer Science}}, + volume = {19}, + issue = {2}, + year = {2023}, + month = {05}, + keywords = {Computer Science - Logic in Computer Science ; Mathematics - Logic}, + eprint = {2111.00482}, + eprinttype = {arxiv}, + eprintclass = {cs}, + citeas = {dJE23} +} + +@inproceedings{dJKFC23, + title = {Set-{{Theoretic}} and {{Type-Theoretic Ordinals Coincide}}}, + booktitle = {2023 38th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}} ({{LICS}})}, + author = {{{de}} Jong, Tom and Kraus, Nicolai and Forsberg, Fredrik Nordvall and Xu, Chuangjie}, + citeas = {dJKFC23}, + date = {2023-06-26}, + year = {2023}, + month = {06}, + eprint = {2301.10696}, + eprinttype = {arxiv}, + eprintclass = {cs, math}, + pages = {1--13}, + doi = {10.1109/LICS56636.2023.10175762}, + abstract = {In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.}, + keywords = {Computer Science - Logic in Computer Science,Mathematics - Logic} +} + @online{Dlicata335/Cohesion-Agda, title = {Dlicata335/Cohesion-Agda}, author = {Licata, Dan}, @@ -218,21 +251,20 @@ @online{GGMS24 keywords = {Computer Science - Logic in Computer Science,Mathematics - Logic} } -@inproceedings{JKFC23, - title = {Set-{{Theoretic}} and {{Type-Theoretic Ordinals Coincide}}}, - booktitle = {2023 38th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}} ({{LICS}})}, - author = {{{de}} Jong, Tom and Kraus, Nicolai and Forsberg, Fredrik Nordvall and Xu, Chuangjie}, - citeas = {JKFC23}, - date = {2023-06-26}, - year = {2023}, - month = {06}, - eprint = {2301.10696}, +@article{KECA17, + title = {{Notions of Anonymous Existence in {{Martin-L\"of}} Type Theory}}, + author = {Nicolai Kraus and Martín Escardó and Thierry Coquand and Thorsten Altenkirch}, + url = {https://lmcs.episciences.org/3217}, + doi = {10.23638/LMCS-13(1:15)2017}, + journal = {{Logical Methods in Computer Science}}, + volume = {13}, + issue = {1}, + year = {2017}, + month = {03}, + keywords = {Computer Science - Logic in Computer Science ; 03B15 ; F.4.1}, + eprint = {1610.03346}, eprinttype = {arxiv}, - eprintclass = {cs, math}, - pages = {1--13}, - doi = {10.1109/LICS56636.2023.10175762}, - abstract = {In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.}, - keywords = {Computer Science - Logic in Computer Science,Mathematics - Logic} + eprintclass = {cs} } @book{May12, diff --git a/src/elementary-number-theory/natural-numbers.lagda.md b/src/elementary-number-theory/natural-numbers.lagda.md index 9e6f400bbd..54c546f857 100644 --- a/src/elementary-number-theory/natural-numbers.lagda.md +++ b/src/elementary-number-theory/natural-numbers.lagda.md @@ -11,6 +11,7 @@ open import foundation.dependent-pair-types open import foundation.universe-levels open import foundation-core.empty-types +open import foundation-core.function-types open import foundation-core.identity-types open import foundation-core.injective-maps open import foundation-core.negation @@ -34,6 +35,15 @@ data ℕ : UU lzero where succ-ℕ : ℕ → ℕ {-# BUILTIN NATURAL ℕ #-} + +second-succ-ℕ : ℕ → ℕ +second-succ-ℕ = succ-ℕ ∘ succ-ℕ + +third-succ-ℕ : ℕ → ℕ +third-succ-ℕ = succ-ℕ ∘ second-succ-ℕ + +fourth-succ-ℕ : ℕ → ℕ +fourth-succ-ℕ = succ-ℕ ∘ third-succ-ℕ ``` ### Useful predicates on the natural numbers diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index 0120bb03b2..fc536f02cc 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -48,6 +48,7 @@ open import foundation-core.propositional-maps public open import foundation-core.propositions public open import foundation-core.pullbacks public open import foundation-core.retractions public +open import foundation-core.retracts-of-types public open import foundation-core.sections public open import foundation-core.sets public open import foundation-core.small-types public diff --git a/src/foundation-core/coherently-invertible-maps.lagda.md b/src/foundation-core/coherently-invertible-maps.lagda.md index 2632a615a2..dca846c82f 100644 --- a/src/foundation-core/coherently-invertible-maps.lagda.md +++ b/src/foundation-core/coherently-invertible-maps.lagda.md @@ -31,7 +31,7 @@ open import foundation-core.whiskering-homotopies-concatenation A [(two-sided) inverse](foundation-core.invertible-maps.md) for a map `f : A → B` is a map `g : B → A` equipped with -[homotopies](foundation-core.homotopies.md) ` S : f ∘ g ~ id` and +[homotopies](foundation-core.homotopies.md) `S : f ∘ g ~ id` and `R : g ∘ f ~ id`. Such data, however is [structure](foundation.structure.md) on the map `f`, and not generally a [property](foundation-core.propositions.md). One way to make the type of inverses into a property is by adding a single diff --git a/src/foundation-core/contractible-types.lagda.md b/src/foundation-core/contractible-types.lagda.md index 113035f9ff..55bb4cc7d1 100644 --- a/src/foundation-core/contractible-types.lagda.md +++ b/src/foundation-core/contractible-types.lagda.md @@ -12,7 +12,6 @@ open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.function-extensionality open import foundation.implicit-function-types -open import foundation.retracts-of-types open import foundation.universe-levels open import foundation-core.cartesian-product-types @@ -20,6 +19,7 @@ open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences open import foundation-core.homotopies open import foundation-core.identity-types +open import foundation-core.retracts-of-types open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation-core/homotopies.lagda.md b/src/foundation-core/homotopies.lagda.md index 2159d361ea..e7d8019d57 100644 --- a/src/foundation-core/homotopies.lagda.md +++ b/src/foundation-core/homotopies.lagda.md @@ -227,6 +227,18 @@ module _ inv-htpy-right-inv-htpy = inv-htpy right-inv-htpy ``` +### Inverting homotopies is an involution + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + {f g : (x : A) → B x} (H : f ~ g) + where + + inv-inv-htpy : inv-htpy (inv-htpy H) ~ H + inv-inv-htpy = inv-inv ∘ H +``` + ### Distributivity of `inv` over `concat` for homotopies ```agda @@ -328,6 +340,46 @@ module _ ap-inv-htpy K x = ap inv (K x) ``` +### Concatenating with an inverse homotopy is inverse to concatenating + +We show that the operation `K ↦ inv-htpy H ∙h K` is inverse to the operation +`K ↦ H ∙h K` by constructing homotopies + +```text + inv-htpy H ∙h (H ∙h K) ~ K + H ∙h (inv H ∙h K) ~ K. +``` + +Similarly, we show that the operation `H ↦ H ∙h inv-htpy K` is inverse to the +operation `H ↦ H ∙h K` by constructing homotopies + +```text + (H ∙h K) ∙h inv-htpy K ~ H + (H ∙h inv-htpy K) ∙h K ~ H. +``` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x} + where + + is-retraction-inv-concat-htpy : + (H : f ~ g) (K : g ~ h) → inv-htpy H ∙h (H ∙h K) ~ K + is-retraction-inv-concat-htpy H K x = is-retraction-inv-concat (H x) (K x) + + is-section-inv-concat-htpy : + (H : f ~ g) (L : f ~ h) → H ∙h (inv-htpy H ∙h L) ~ L + is-section-inv-concat-htpy H L x = is-section-inv-concat (H x) (L x) + + is-retraction-inv-concat-htpy' : + (K : g ~ h) (H : f ~ g) → (H ∙h K) ∙h inv-htpy K ~ H + is-retraction-inv-concat-htpy' K H x = is-retraction-inv-concat' (K x) (H x) + + is-section-inv-concat-htpy' : + (K : g ~ h) (L : f ~ h) → (L ∙h inv-htpy K) ∙h K ~ L + is-section-inv-concat-htpy' K L x = is-section-inv-concat' (K x) (L x) +``` + ## Reasoning with homotopies Homotopies can be constructed by equational reasoning in the following way: diff --git a/src/foundation-core/identity-types.lagda.md b/src/foundation-core/identity-types.lagda.md index 8a4289d598..b4c54955d7 100644 --- a/src/foundation-core/identity-types.lagda.md +++ b/src/foundation-core/identity-types.lagda.md @@ -421,7 +421,7 @@ module _ double-transpose-eq-concat : {x y u v : A} (r : x ＝ u) (p : x ＝ y) (s : u ＝ v) (q : y ＝ v) → - p ∙ q ＝ r ∙ s → (inv r) ∙ p ＝ s ∙ (inv q) + p ∙ q ＝ r ∙ s → inv r ∙ p ＝ s ∙ inv q double-transpose-eq-concat refl p s refl α = (inv right-unit ∙ α) ∙ inv right-unit diff --git a/src/foundation-core/invertible-maps.lagda.md b/src/foundation-core/invertible-maps.lagda.md index 8a82664b41..c4af35f5a7 100644 --- a/src/foundation-core/invertible-maps.lagda.md +++ b/src/foundation-core/invertible-maps.lagda.md @@ -24,10 +24,11 @@ open import foundation-core.sections ## Idea -An **inverse** for a map `f : A → B` is a map `g : B → A` equipped with -[homotopies](foundation-core.homotopies.md) ` (f ∘ g) ~ id` and `(g ∘ f) ~ id`. -Such data, however is [structure](foundation.structure.md) on the map `f`, and -not generally a [property](foundation-core.propositions.md). +An {{#concept "inverse" Disambiguation="maps of types" Agda=is-inverse}} for a +map `f : A → B` is a map `g : B → A` equipped with +[homotopies](foundation-core.homotopies.md) `f ∘ g ~ id` and `g ∘ f ~ id`. Such +data, however, is [structure](foundation.structure.md) on the map `f`, and not +generally a [property](foundation-core.propositions.md). ## Definition diff --git a/src/foundation-core/retractions.lagda.md b/src/foundation-core/retractions.lagda.md index ebbe0f7039..7ba3ebc1f4 100644 --- a/src/foundation-core/retractions.lagda.md +++ b/src/foundation-core/retractions.lagda.md @@ -240,6 +240,6 @@ module _ ## See also - Retracts of types are defined in - [`foundation.retracts-of-types`](foundation.retracts-of-types.md). + [`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). diff --git a/src/foundation-core/retracts-of-types.lagda.md b/src/foundation-core/retracts-of-types.lagda.md new file mode 100644 index 0000000000..8811b4a08c --- /dev/null +++ b/src/foundation-core/retracts-of-types.lagda.md @@ -0,0 +1,191 @@ +# Retracts of types + +```agda +module foundation-core.retracts-of-types where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.function-extensionality +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition + +open import foundation-core.function-types +open import foundation-core.identity-types +open import foundation-core.postcomposition-functions +open import foundation-core.precomposition-functions +open import foundation-core.retractions +open import foundation-core.sections +``` + +
+ +## Idea + +We say that a type `A` is a +{{#concept "retract" Disambiguation="of types" Agda=retracts}} of a type `B` if +the types `A` and `B` come equipped with +{{#concept "retract data" Disambiguation="of types" Agda=retract}}, i.e., with +maps + +```text + i r + A -----> B -----> A +``` + +such that `r` is a [retraction](foundation-core.retractions.md) of `i`, i.e., +there is a [homotopy](foundation-core.homotopies.md) `r ∘ i ~ id`. The map `i` +is called the **inclusion** of the retract data, and the map `r` is called the +**underlying map of the retraction**. + +## Definitions + +### The type of witnesses that `A` is a retract of `B` + +The predicate `retract B` is used to assert that a type is a retract of `B`, +i.e., the type `retract B A` is the type of maps from `A` to `B` that come +equipped with a retraction. + +We also introduce more intuitive infix notation `A retract-of B` to assert that +`A` is a retract of `B`. + +```agda +retract : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) +retract B A = Σ (A → B) (retraction) + +infix 6 _retract-of_ + +_retract-of_ : + {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) +A retract-of B = retract B A + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (R : retract B A) + where + + inclusion-retract : A → B + inclusion-retract = pr1 R + + retraction-retract : retraction inclusion-retract + retraction-retract = pr2 R + + map-retraction-retract : B → A + map-retraction-retract = map-retraction inclusion-retract retraction-retract + + is-retraction-map-retraction-retract : + is-section map-retraction-retract inclusion-retract + is-retraction-map-retraction-retract = + is-retraction-map-retraction inclusion-retract retraction-retract + + section-retract : section map-retraction-retract + pr1 section-retract = inclusion-retract + pr2 section-retract = is-retraction-map-retraction-retract +``` + +### The type of retracts of a type + +```agda +retracts : {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2) +retracts l2 A = Σ (UU l2) (_retract-of A) + +module _ + {l1 l2 : Level} {A : UU l1} (R : retracts l2 A) + where + + type-retracts : UU l2 + type-retracts = pr1 R + + retract-retracts : type-retracts retract-of A + retract-retracts = pr2 R + + inclusion-retracts : type-retracts → A + inclusion-retracts = inclusion-retract retract-retracts + + retraction-retracts : retraction inclusion-retracts + retraction-retracts = retraction-retract retract-retracts + + map-retraction-retracts : A → type-retracts + map-retraction-retracts = map-retraction-retract retract-retracts + + is-retraction-map-retraction-retracts : + is-section map-retraction-retracts inclusion-retracts + is-retraction-map-retraction-retracts = + is-retraction-map-retraction-retract retract-retracts + + section-retracts : section map-retraction-retracts + section-retracts = section-retract retract-retracts +``` + +## Properties + +### If `A` is a retract of `B` with inclusion `i : A → B`, then `x ＝ y` is a retract of `i x ＝ i y` for any two elements `x y : A` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (R : A retract-of B) (x y : A) + where + + retract-eq : + (x ＝ y) retract-of (inclusion-retract R x ＝ inclusion-retract R y) + pr1 retract-eq = ap (inclusion-retract R) + pr2 retract-eq = retraction-ap (inclusion-retract R) (retraction-retract R) +``` + +### If `A` is a retract of `B` then `A → S` is a retract of `B → S` via precomposition + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (R : A retract-of B) (S : UU l3) + where + + retract-precomp : + (A → S) retract-of (B → S) + pr1 retract-precomp = + precomp (map-retraction-retract R) S + pr1 (pr2 retract-precomp) = + precomp (inclusion-retract R) S + pr2 (pr2 retract-precomp) h = + eq-htpy (h ·l is-retraction-map-retraction-retract R) +``` + +### If `A` is a retract of `B` then `S → A` is a retract of `S → B` via postcomposition + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (S : UU l3) (R : A retract-of B) + where + + retract-postcomp : + (S → A) retract-of (S → B) + pr1 retract-postcomp = + postcomp S (inclusion-retract R) + pr1 (pr2 retract-postcomp) = + postcomp S (map-retraction-retract R) + pr2 (pr2 retract-postcomp) h = + eq-htpy (is-retraction-map-retraction-retract R ·r h) +``` + +### Composition of retracts + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + where + + comp-retract : B retract-of C → A retract-of B → A retract-of C + pr1 (comp-retract r r') = + inclusion-retract r ∘ inclusion-retract r' + pr2 (comp-retract r r') = + retraction-comp + ( inclusion-retract r) + ( inclusion-retract r') + ( retraction-retract r) + ( retraction-retract r') +``` + +## See also + +- [Retracts of maps](foundation.retracts-of-maps.md) diff --git a/src/foundation-core/small-types.lagda.md b/src/foundation-core/small-types.lagda.md index dd0762ef81..040e367ebb 100644 --- a/src/foundation-core/small-types.lagda.md +++ b/src/foundation-core/small-types.lagda.md @@ -307,3 +307,7 @@ is-small-logical-equivalence : is-small-logical-equivalence H K = is-small-product (is-small-function-type H K) (is-small-function-type K H) ``` + +## See also + +- [Small maps](foundation.small-maps.md) diff --git a/src/foundation-core/truncated-types.lagda.md b/src/foundation-core/truncated-types.lagda.md index 1f474dbdd4..ef0e87f4a0 100644 --- a/src/foundation-core/truncated-types.lagda.md +++ b/src/foundation-core/truncated-types.lagda.md @@ -11,7 +11,6 @@ open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.function-extensionality -open import foundation.retracts-of-types open import foundation.universe-levels open import foundation-core.cartesian-product-types @@ -22,6 +21,7 @@ open import foundation-core.equivalences open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositions +open import foundation-core.retracts-of-types open import foundation-core.transport-along-identifications open import foundation-core.truncation-levels ``` diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 3ac04d2000..563cc1c995 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -181,6 +181,7 @@ open import foundation.fibered-maps public open import foundation.fibers-of-maps public open import foundation.finitely-coherent-equivalences public open import foundation.finitely-coherently-invertible-maps public +open import foundation.fixed-points-endofunctions public open import foundation.full-subtypes public open import foundation.function-extensionality public open import foundation.function-types public @@ -207,6 +208,7 @@ open import foundation.homotopies-morphisms-arrows public open import foundation.homotopy-algebra public open import foundation.homotopy-induction public open import foundation.homotopy-preorder-of-types public +open import foundation.idempotent-maps public open import foundation.identity-systems public open import foundation.identity-truncated-types public open import foundation.identity-types public @@ -299,7 +301,6 @@ open import foundation.precomposition-dependent-functions public open import foundation.precomposition-functions public open import foundation.precomposition-functions-into-subuniverses public open import foundation.precomposition-type-families public -open import foundation.preidempotent-maps public open import foundation.preimages-of-subtypes public open import foundation.preunivalence public open import foundation.preunivalent-type-families public @@ -321,6 +322,7 @@ open import foundation.propositional-truncations public open import foundation.propositions public open import foundation.pullbacks public open import foundation.pullbacks-subtypes public +open import foundation.quasicoherently-idempotent-maps public open import foundation.raising-universe-levels public open import foundation.reflecting-maps-equivalence-relations public open import foundation.reflexive-relations public @@ -356,6 +358,7 @@ open import foundation.span-diagrams public open import foundation.span-diagrams-families-of-types public open import foundation.spans public open import foundation.spans-families-of-types public +open import foundation.split-idempotent-maps public open import foundation.split-surjective-maps public open import foundation.standard-apartness-relations public open import foundation.standard-pullbacks public diff --git a/src/foundation/coherently-invertible-maps.lagda.md b/src/foundation/coherently-invertible-maps.lagda.md index e2e34ab431..03f1ed4655 100644 --- a/src/foundation/coherently-invertible-maps.lagda.md +++ b/src/foundation/coherently-invertible-maps.lagda.md @@ -10,22 +10,17 @@ open import foundation-core.coherently-invertible-maps public ```agda open import foundation.action-on-identifications-functions -open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.identity-types open import foundation.logical-equivalences open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels -open import foundation.whiskering-higher-homotopies-composition -open import foundation-core.commuting-squares-of-homotopies open import foundation-core.contractible-maps open import foundation-core.contractible-types open import foundation-core.fibers-of-maps open import foundation-core.functoriality-dependent-pair-types -open import foundation-core.homotopies open import foundation-core.propositions -open import foundation-core.retractions open import foundation-core.sections open import foundation-core.type-theoretic-principle-of-choice ``` diff --git a/src/foundation/commuting-prisms-of-maps.lagda.md b/src/foundation/commuting-prisms-of-maps.lagda.md index 0c374973c9..c8567bf6b6 100644 --- a/src/foundation/commuting-prisms-of-maps.lagda.md +++ b/src/foundation/commuting-prisms-of-maps.lagda.md @@ -15,7 +15,6 @@ open import foundation.commuting-triangles-of-maps open import foundation.composition-algebra open import foundation.function-extensionality open import foundation.identity-types -open import foundation.path-algebra open import foundation.postcomposition-functions open import foundation.precomposition-functions open import foundation.universe-levels diff --git a/src/foundation/commuting-squares-of-homotopies.lagda.md b/src/foundation/commuting-squares-of-homotopies.lagda.md index fa4657be1f..96f412b0f0 100644 --- a/src/foundation/commuting-squares-of-homotopies.lagda.md +++ b/src/foundation/commuting-squares-of-homotopies.lagda.md @@ -16,7 +16,6 @@ open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.functoriality-dependent-function-types open import foundation-core.homotopies -open import foundation-core.identity-types ``` diff --git a/src/foundation/commuting-triangles-of-homotopies.lagda.md b/src/foundation/commuting-triangles-of-homotopies.lagda.md index d3f3b61b72..a9a57c0d7e 100644 --- a/src/foundation/commuting-triangles-of-homotopies.lagda.md +++ b/src/foundation/commuting-triangles-of-homotopies.lagda.md @@ -7,15 +7,12 @@ module foundation.commuting-triangles-of-homotopies where
Imports ```agda -open import foundation.action-on-identifications-functions open import foundation.commuting-triangles-of-identifications open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import foundation-core.function-types open import foundation-core.homotopies -open import foundation-core.identity-types -open import foundation-core.whiskering-identifications-concatenation ```
diff --git a/src/foundation/commuting-triangles-of-identifications.lagda.md b/src/foundation/commuting-triangles-of-identifications.lagda.md index 8ca143645b..ab6e12a82d 100644 --- a/src/foundation/commuting-triangles-of-identifications.lagda.md +++ b/src/foundation/commuting-triangles-of-identifications.lagda.md @@ -9,16 +9,13 @@ module foundation.commuting-triangles-of-identifications where ```agda open import foundation.action-on-identifications-functions open import foundation.binary-equivalences -open import foundation.commuting-squares-of-identifications open import foundation.dependent-pair-types open import foundation.identity-types -open import foundation.path-algebra open import foundation.universe-levels open import foundation.whiskering-identifications-concatenation +open import foundation-core.commuting-squares-of-identifications open import foundation-core.equivalences -open import foundation-core.function-types -open import foundation-core.homotopies ``` diff --git a/src/foundation/commuting-triangles-of-morphisms-arrows.lagda.md b/src/foundation/commuting-triangles-of-morphisms-arrows.lagda.md index 0f44383140..2e375cefa7 100644 --- a/src/foundation/commuting-triangles-of-morphisms-arrows.lagda.md +++ b/src/foundation/commuting-triangles-of-morphisms-arrows.lagda.md @@ -10,11 +10,6 @@ module foundation.commuting-triangles-of-morphisms-arrows where open import foundation.homotopies-morphisms-arrows open import foundation.morphisms-arrows open import foundation.universe-levels -open import foundation.whiskering-homotopies-composition - -open import foundation-core.commuting-squares-of-maps -open import foundation-core.commuting-triangles-of-maps -open import foundation-core.homotopies ``` diff --git a/src/foundation/connected-types.lagda.md b/src/foundation/connected-types.lagda.md index 60482bcaa2..193097e706 100644 --- a/src/foundation/connected-types.lagda.md +++ b/src/foundation/connected-types.lagda.md @@ -15,7 +15,6 @@ open import foundation.functoriality-truncation open import foundation.inhabited-types open import foundation.propositional-truncations open import foundation.propositions -open import foundation.retracts-of-types open import foundation.truncations open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels @@ -26,6 +25,7 @@ open import foundation-core.equivalences open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import foundation-core.precomposition-functions +open import foundation-core.retracts-of-types open import foundation-core.truncated-types open import foundation-core.truncation-levels ``` diff --git a/src/foundation/decidable-equality.lagda.md b/src/foundation/decidable-equality.lagda.md index 39b6f711fc..7309925bf4 100644 --- a/src/foundation/decidable-equality.lagda.md +++ b/src/foundation/decidable-equality.lagda.md @@ -14,7 +14,6 @@ open import foundation.dependent-pair-types open import foundation.double-negation open import foundation.injective-maps open import foundation.negation -open import foundation.retracts-of-types open import foundation.sections open import foundation.sets open import foundation.type-arithmetic-dependent-pair-types @@ -28,6 +27,7 @@ open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.identity-types open import foundation-core.propositions +open import foundation-core.retracts-of-types open import foundation-core.transport-along-identifications ``` diff --git a/src/foundation/decidable-types.lagda.md b/src/foundation/decidable-types.lagda.md index 8073a1ae80..3bed2fac28 100644 --- a/src/foundation/decidable-types.lagda.md +++ b/src/foundation/decidable-types.lagda.md @@ -15,7 +15,6 @@ open import foundation.hilberts-epsilon-operators open import foundation.negation open import foundation.propositional-truncations open import foundation.raising-universe-levels -open import foundation.retracts-of-types open import foundation.type-arithmetic-empty-type open import foundation.unit-type open import foundation.universe-levels @@ -24,6 +23,7 @@ open import foundation-core.cartesian-product-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.propositions +open import foundation-core.retracts-of-types ``` diff --git a/src/foundation/equivalence-induction.lagda.md b/src/foundation/equivalence-induction.lagda.md index 4db46b81af..a4b437a51f 100644 --- a/src/foundation/equivalence-induction.lagda.md +++ b/src/foundation/equivalence-induction.lagda.md @@ -9,7 +9,6 @@ module foundation.equivalence-induction where ```agda open import foundation.dependent-pair-types open import foundation.identity-systems -open import foundation.postcomposition-functions open import foundation.subuniverses open import foundation.univalence open import foundation.universal-property-identity-systems @@ -20,6 +19,7 @@ open import foundation-core.contractible-maps open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.identity-types +open import foundation-core.postcomposition-functions open import foundation-core.sections open import foundation-core.torsorial-type-families ``` diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md index 3b62d1bde4..0a3a32779f 100644 --- a/src/foundation/equivalences.lagda.md +++ b/src/foundation/equivalences.lagda.md @@ -34,6 +34,7 @@ open import foundation-core.injective-maps open import foundation-core.propositions open import foundation-core.pullbacks open import foundation-core.retractions +open import foundation-core.retracts-of-types open import foundation-core.sections open import foundation-core.subtypes open import foundation-core.truncation-levels @@ -135,6 +136,21 @@ module _ ( is-contr-map-is-equiv (is-equiv-precomp-is-equiv f is-equiv-f A) id) ``` +### The underlying retract of an equivalence + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + retract-equiv : A ≃ B → A retract-of B + retract-equiv e = + ( map-equiv e , map-inv-equiv e , is-retraction-map-inv-equiv e) + + retract-inv-equiv : B ≃ A → A retract-of B + retract-inv-equiv = retract-equiv ∘ inv-equiv +``` + ### Being an equivalence is a property ```agda diff --git a/src/foundation/fixed-points-endofunctions.lagda.md b/src/foundation/fixed-points-endofunctions.lagda.md new file mode 100644 index 0000000000..58d4618a9e --- /dev/null +++ b/src/foundation/fixed-points-endofunctions.lagda.md @@ -0,0 +1,36 @@ +# Fixed points of endofunctions + +```agda +module foundation.fixed-points-endofunctions where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import foundation-core.identity-types +``` + +
+ +## Idea + +Given an [endofunction](foundation-core.endomorphisms.md) `f : A → A`, the type +of {{#concept "fixed points"}} is the type of elements `x : A` such that +`f x ＝ x`. + +## Definitions + +```agda +module _ + {l : Level} {A : UU l} (f : A → A) + where + + fixed-point : UU l + fixed-point = Σ A (λ x → f x ＝ x) + + fixed-point' : UU l + fixed-point' = Σ A (λ x → x ＝ f x) +``` diff --git a/src/foundation/function-extensionality.lagda.md b/src/foundation/function-extensionality.lagda.md index 65ac8d469b..7ba761bdd8 100644 --- a/src/foundation/function-extensionality.lagda.md +++ b/src/foundation/function-extensionality.lagda.md @@ -13,7 +13,6 @@ open import foundation.dependent-pair-types open import foundation.evaluation-functions open import foundation.implicit-function-types open import foundation.universe-levels -open import foundation.whiskering-homotopies-composition open import foundation-core.equivalences open import foundation-core.function-types diff --git a/src/foundation/functoriality-truncation.lagda.md b/src/foundation/functoriality-truncation.lagda.md index c83d626984..92e1760616 100644 --- a/src/foundation/functoriality-truncation.lagda.md +++ b/src/foundation/functoriality-truncation.lagda.md @@ -10,7 +10,6 @@ module foundation.functoriality-truncation where open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.function-extensionality -open import foundation.retracts-of-types open import foundation.truncations open import foundation.universe-levels open import foundation.whiskering-homotopies-composition @@ -21,6 +20,7 @@ open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.retractions +open import foundation-core.retracts-of-types open import foundation-core.sections open import foundation-core.truncation-levels ``` diff --git a/src/foundation/fundamental-theorem-of-identity-types.lagda.md b/src/foundation/fundamental-theorem-of-identity-types.lagda.md index a82990327e..9ac5bfc324 100644 --- a/src/foundation/fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/fundamental-theorem-of-identity-types.lagda.md @@ -8,7 +8,6 @@ module foundation.fundamental-theorem-of-identity-types where ```agda open import foundation.dependent-pair-types -open import foundation.retracts-of-types open import foundation.universe-levels open import foundation-core.contractible-types @@ -19,6 +18,7 @@ open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.retractions +open import foundation-core.retracts-of-types open import foundation-core.sections open import foundation-core.torsorial-type-families ``` diff --git a/src/foundation/idempotent-maps.lagda.md b/src/foundation/idempotent-maps.lagda.md new file mode 100644 index 0000000000..791fca96fa --- /dev/null +++ b/src/foundation/idempotent-maps.lagda.md @@ -0,0 +1,162 @@ +# Idempotent maps + +```agda +module foundation.idempotent-maps where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.homotopy-algebra +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition + +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.propositions +open import foundation-core.retractions +open import foundation-core.sets +``` + +
+ +## Idea + +An {{#concept "idempotent map" Disambiguation="of types" Agda=is-idempotent}} is +a map `f : A → A` [equipped](foundation.structure.md) with a +[homotopy](foundation-core.homotopies.md) + +```text + f ∘ f ~ f. +``` + +While this definition corresponds to the classical concept of an idempotent map +in [set](foundation-core.sets.md)-level mathematics, a homotopy `I : f ∘ f ~ f` +may fail to be coherent with itself in Homotopy Type Theory. For instance, one +may ask for a second-order coherence + +```text + J : f ·r I ~ I ·l f +``` + +giving the definition of a +[quasicoherently idempotent map](foundation.quasicoherently-idempotent-maps.md). + +The situation may be compared against that of +[invertible maps](foundation-core.invertible-maps.md) vs. +[coherently invertible maps](foundation-core.coherently-invertible-maps.md). +Recall that an _invertible map_ is a map `f : A → B` equipped with a converse +map `g : B → A` and homotopies `S : f ∘ g ~ id` and `R : g ∘ f ~ id` witnessing +that `g` is an _inverse_ of `f`, while a _coherently invertible map_ has an +additional coherence `f ·r R ~ S ·l f`. + +It is true that every invertible map is coherently invertible, but no such +construction preserves both of the homotopies `S` and `R`. Likewise, every +quasicoherently idempotent map is also coherently idempotent, although again the +coherence `J` is replaced as part of this construction. On the other hand, in +contrast to invertible maps, not every idempotent map can be made to be fully +coherent or even quasicoherent. For a counterexample see Section 4 of +{{#cite Shu17}}. + +**Terminology.** Our definition of an _idempotent map_ corresponds to the +definition of a _preidempotent map_ in {{#reference Shu17}} and +{{#reference Shu14SplittingIdempotents}}, while their definition of an +_idempotent map_ corresponds in our terminology to a _coherently idempotent +map_. + +## Definitions + +### The structure on a map of idempotence + +```agda +is-idempotent : {l : Level} {A : UU l} → (A → A) → UU l +is-idempotent f = f ∘ f ~ f +``` + +### The type of idempotent maps on a type + +```agda +idempotent-map : {l : Level} (A : UU l) → UU l +idempotent-map A = Σ (A → A) (is-idempotent) + +module _ + {l : Level} {A : UU l} (f : idempotent-map A) + where + + map-idempotent-map : A → A + map-idempotent-map = pr1 f + + is-idempotent-idempotent-map : + is-idempotent map-idempotent-map + is-idempotent-idempotent-map = pr2 f +``` + +## Properties + +### Being an idempotent operation on a set is a property + +```agda +module _ + {l : Level} {A : UU l} (is-set-A : is-set A) (f : A → A) + where + + is-prop-is-idempotent-is-set : is-prop (is-idempotent f) + is-prop-is-idempotent-is-set = + is-prop-Π (λ x → is-set-A (f (f x)) (f x)) + + is-idempotent-is-set-Prop : Prop l + is-idempotent-is-set-Prop = + ( is-idempotent f , is-prop-is-idempotent-is-set) + +module _ + {l : Level} (A : Set l) (f : type-Set A → type-Set A) + where + + is-prop-is-idempotent-Set : is-prop (is-idempotent f) + is-prop-is-idempotent-Set = + is-prop-is-idempotent-is-set (is-set-type-Set A) f + + is-idempotent-prop-Set : Prop l + is-idempotent-prop-Set = + ( is-idempotent f , is-prop-is-idempotent-Set) +``` + +### If `i` and `r` is an inclusion-retraction pair, then `i ∘ r` is idempotent + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + (i : B → A) (r : A → B) (H : is-retraction i r) + where + + is-idempotent-inclusion-retraction : is-idempotent (i ∘ r) + is-idempotent-inclusion-retraction = i ·l H ·r r +``` + +### Idempotence is preserved by homotopies + +If a map `g` is homotopic to an idempotent map `f`, then `g` is also idempotent. + +```agda +module _ + {l : Level} {A : UU l} {f g : A → A} (F : is-idempotent f) + where + + is-idempotent-htpy : g ~ f → is-idempotent g + is-idempotent-htpy H = + horizontal-concat-htpy H H ∙h F ∙h inv-htpy H + + is-idempotent-inv-htpy : f ~ g → is-idempotent g + is-idempotent-inv-htpy H = + horizontal-concat-htpy (inv-htpy H) (inv-htpy H) ∙h F ∙h H +``` + +## See also + +- [Quasicoherently idempotent maps](foundation.quasicoherently-idempotent-maps.md) +- [Split idempotent maps](foundation.split-idempotent-maps.md) + +## References + +{{#bibliography}} {{#reference Shu17}} {{#reference Shu14SplittingIdempotents}} diff --git a/src/foundation/identity-types.lagda.md b/src/foundation/identity-types.lagda.md index 80997d9a37..8bbd6bea4c 100644 --- a/src/foundation/identity-types.lagda.md +++ b/src/foundation/identity-types.lagda.md @@ -219,6 +219,20 @@ module _ ( ( ap (concat' _ s) (right-inv right-unit)))) ``` +### Applying the right unit law on one side of a higher identification is an equivalence + +```agda +module _ + {l : Level} {A : UU l} {x y : A} + where + + equiv-right-unit : (p : x ＝ y) (q : x ＝ y) → (p ＝ q) ≃ (p ∙ refl ＝ q) + equiv-right-unit p = equiv-concat right-unit + + equiv-right-unit' : (p : x ＝ y) (q : x ＝ y) → (p ＝ q ∙ refl) ≃ (p ＝ q) + equiv-right-unit' p q = equiv-concat' p right-unit +``` + ### Reassociating one side of a higher identification is an equivalence ```agda @@ -265,7 +279,7 @@ module _ left-transpose-eq-concat' : (p : x ＝ z) (q : x ＝ y) (r : y ＝ z) → - (p ＝ q ∙ r) → (inv q ∙ p ＝ r) + p ＝ q ∙ r → inv q ∙ p ＝ r left-transpose-eq-concat' p q r = map-equiv (equiv-left-transpose-eq-concat' p q r) @@ -282,7 +296,7 @@ module _ equiv-right-transpose-eq-concat : (p : x ＝ y) (q : y ＝ z) (r : x ＝ z) → - ((p ∙ q) ＝ r) ≃ (p ＝ (r ∙ (inv q))) + (p ∙ q ＝ r) ≃ (p ＝ r ∙ inv q) pr1 (equiv-right-transpose-eq-concat p q r) = right-transpose-eq-concat p q r pr2 (equiv-right-transpose-eq-concat p q r) = is-equiv-right-transpose-eq-concat p q r @@ -291,11 +305,13 @@ module _ (p : x ＝ z) (q : x ＝ y) (r : y ＝ z) → (p ＝ q ∙ r) ≃ (p ∙ inv r ＝ q) equiv-right-transpose-eq-concat' p q r = - equiv-inv _ _ ∘e equiv-right-transpose-eq-concat q r p ∘e equiv-inv _ _ + equiv-inv q (p ∙ inv r) ∘e + equiv-right-transpose-eq-concat q r p ∘e + equiv-inv p (q ∙ r) right-transpose-eq-concat' : (p : x ＝ z) (q : x ＝ y) (r : y ＝ z) → - (p ＝ q ∙ r) → (p ∙ inv r ＝ q) + p ＝ q ∙ r → p ∙ inv r ＝ q right-transpose-eq-concat' p q r = map-equiv (equiv-right-transpose-eq-concat' p q r) ``` diff --git a/src/foundation/involutions.lagda.md b/src/foundation/involutions.lagda.md index 4a0bc6a497..df78de65a1 100644 --- a/src/foundation/involutions.lagda.md +++ b/src/foundation/involutions.lagda.md @@ -203,6 +203,17 @@ pr2 (involution-Π-involution-fam i) f = eq-htpy (λ x → is-involution-map-involution (i x) (f x)) ``` +### Coherence of involutions + +```agda +module _ + {l : Level} {A : UU l} {f : A → A} (H : is-involution f) + where + + coherence-is-involution : UU l + coherence-is-involution = f ·l H ~ H ·r f +``` + ## Examples ### The identity function is an involution diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md index f22f14f192..febb5dc198 100644 --- a/src/foundation/path-algebra.lagda.md +++ b/src/foundation/path-algebra.lagda.md @@ -11,13 +11,10 @@ open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.binary-embeddings open import foundation.binary-equivalences -open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.universe-levels open import foundation-core.commuting-squares-of-identifications -open import foundation-core.constant-maps -open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.whiskering-identifications-concatenation diff --git a/src/foundation/preidempotent-maps.lagda.md b/src/foundation/preidempotent-maps.lagda.md deleted file mode 100644 index 90324eb1de..0000000000 --- a/src/foundation/preidempotent-maps.lagda.md +++ /dev/null @@ -1,49 +0,0 @@ -# Preidempotent maps - -```agda -module foundation.preidempotent-maps where -``` - -
Imports - -```agda -open import foundation.dependent-pair-types -open import foundation.universe-levels - -open import foundation-core.function-types -open import foundation-core.homotopies -open import foundation-core.propositions -open import foundation-core.sets -``` - -
- -## Idea - -A **preidempotent map** is a map `f : A → A` equipped with a homotopy -`f ∘ f ~ f`. - -## Definition - -```agda -is-preidempotent : {l : Level} {A : UU l} → (A → A) → UU l -is-preidempotent f = (f ∘ f) ~ f - -preidempotent-map : {l : Level} (A : UU l) → UU l -preidempotent-map A = Σ (A → A) is-preidempotent -``` - -## Properties - -### Being preidempotent over a set is a property - -```agda -is-prop-is-preidempotent-is-set : - {l : Level} {A : UU l} → is-set A → (f : A → A) → is-prop (is-preidempotent f) -is-prop-is-preidempotent-is-set is-set-A f = - is-prop-Π λ x → is-set-A (f (f x)) (f x) -``` - -## References - -{{#bibliography}} {{#reference Shu17}} {{#reference Shu14SplittingIdempotents}} diff --git a/src/foundation/quasicoherently-idempotent-maps.lagda.md b/src/foundation/quasicoherently-idempotent-maps.lagda.md new file mode 100644 index 0000000000..51a7b9982c --- /dev/null +++ b/src/foundation/quasicoherently-idempotent-maps.lagda.md @@ -0,0 +1,388 @@ +# Quasicoherently idempotent maps + +```agda +module foundation.quasicoherently-idempotent-maps where +``` + +
Imports + +```agda +open import foundation.1-types +open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types +open import foundation.homotopy-algebra +open import foundation.idempotent-maps +open import foundation.negation +open import foundation.universe-levels +open import foundation.whiskering-higher-homotopies-composition +open import foundation.whiskering-homotopies-composition + +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.propositions +open import foundation-core.retractions +open import foundation-core.sets + +open import synthetic-homotopy-theory.circle +``` + +
+ +## Idea + +A +{{#concept "quasicoherently idempotent map" Disambiguation="on a type" Agda=is-quasicoherently-idempotent}} +is a map `f : A → A` [equipped](foundation.structure.md) with a +[homotopy](foundation-core.homotopies.md) `I : f ∘ f ~ f` witnessing that `f` is +[idempotent](foundation.idempotent-maps.md), and a coherence + +```text + f ·l I ~ I ·r f. +``` + +While this data is not enough to capture a fully coherent idempotent map, it is +sufficient for showing that `f` can be made to be fully coherent. This is in +contrast to [idempotent maps](foundation.idempotent-maps.md), which may in +general fail to be coherent. + +**Terminology.** Our definition of a _quasicoherently idempotent map_ +corresponds to the definition of a _quasiidempotent map_ in {{#cite Shu17}} and +{{#cite Shu14SplittingIdempotents}}. + +## Definitions + +### The structure of quasicoherent idempotence on maps + +```agda +coherence-is-quasicoherently-idempotent : + {l : Level} {A : UU l} (f : A → A) → f ∘ f ~ f → UU l +coherence-is-quasicoherently-idempotent f I = f ·l I ~ I ·r f + +is-quasicoherently-idempotent : {l : Level} {A : UU l} → (A → A) → UU l +is-quasicoherently-idempotent f = + Σ (f ∘ f ~ f) (coherence-is-quasicoherently-idempotent f) + +module _ + {l : Level} {A : UU l} {f : A → A} (H : is-quasicoherently-idempotent f) + where + + is-idempotent-is-quasicoherently-idempotent : is-idempotent f + is-idempotent-is-quasicoherently-idempotent = pr1 H + + coh-is-quasicoherently-idempotent : + coherence-is-quasicoherently-idempotent f + ( is-idempotent-is-quasicoherently-idempotent) + coh-is-quasicoherently-idempotent = pr2 H +``` + +### The type of quasicoherently idempotent maps + +```agda +quasicoherently-idempotent-map : {l : Level} (A : UU l) → UU l +quasicoherently-idempotent-map A = Σ (A → A) (is-quasicoherently-idempotent) + +module _ + {l : Level} {A : UU l} (H : quasicoherently-idempotent-map A) + where + + map-quasicoherently-idempotent-map : A → A + map-quasicoherently-idempotent-map = pr1 H + + is-quasicoherently-idempotent-quasicoherently-idempotent-map : + is-quasicoherently-idempotent map-quasicoherently-idempotent-map + is-quasicoherently-idempotent-quasicoherently-idempotent-map = pr2 H + + is-idempotent-quasicoherently-idempotent-map : + is-idempotent map-quasicoherently-idempotent-map + is-idempotent-quasicoherently-idempotent-map = + is-idempotent-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map) + + coh-quasicoherently-idempotent-map : + coherence-is-quasicoherently-idempotent + ( map-quasicoherently-idempotent-map) + ( is-idempotent-quasicoherently-idempotent-map) + coh-quasicoherently-idempotent-map = + coh-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map) + + idempotent-map-quasicoherently-idempotent-map : idempotent-map A + idempotent-map-quasicoherently-idempotent-map = + ( map-quasicoherently-idempotent-map , + is-idempotent-quasicoherently-idempotent-map) +``` + +## Properties + +### Being quasicoherently idempotent on a set is a property + +```agda +module _ + {l : Level} {A : UU l} (is-set-A : is-set A) (f : A → A) + where + + is-prop-coherence-is-quasicoherently-idempotent-is-set : + (I : f ∘ f ~ f) → is-prop (coherence-is-quasicoherently-idempotent f I) + is-prop-coherence-is-quasicoherently-idempotent-is-set I = + is-prop-Π + ( λ x → + is-set-is-prop + ( is-set-A ((f ∘ f ∘ f) x) ((f ∘ f) x)) + ( (f ·l I) x) + ( (I ·r f) x)) + + is-prop-is-quasicoherently-idempotent-is-set : + is-prop (is-quasicoherently-idempotent f) + is-prop-is-quasicoherently-idempotent-is-set = + is-prop-Σ + ( is-prop-is-idempotent-is-set is-set-A f) + ( is-prop-coherence-is-quasicoherently-idempotent-is-set) + + is-quasicoherently-idempotent-is-set-Prop : Prop l + is-quasicoherently-idempotent-is-set-Prop = + ( is-quasicoherently-idempotent f , + is-prop-is-quasicoherently-idempotent-is-set) + +module _ + {l : Level} (A : Set l) (f : type-Set A → type-Set A) + where + + is-prop-is-quasicoherently-idempotent-Set : + is-prop (is-quasicoherently-idempotent f) + is-prop-is-quasicoherently-idempotent-Set = + is-prop-is-quasicoherently-idempotent-is-set (is-set-type-Set A) f + + is-quasicoherently-idempotent-prop-Set : Prop l + is-quasicoherently-idempotent-prop-Set = + ( is-quasicoherently-idempotent f , + is-prop-is-quasicoherently-idempotent-Set) +``` + +### Being quasicoherently idempotent is generally not a property + +Not even for [1-types](foundation.1-types.md): consider the identity function on +the [circle](synthetic-homotopy-theory.circle.md) + +```text + id : 𝕊¹ → 𝕊¹. +``` + +Two distinct witnesses that it is idempotent are given by `t ↦ refl` and +`t ↦ loop`. Both of these are quasicoherent, because + +```text + coherence-is-quasicoherently-idempotent id I ≐ (id ·l I ~ I ·r id) ≃ (I ~ I). +``` + +To formalize this result, we first need that the loop of the circle is +nontrivial. + +```text +is-not-prop-is-quasicoherently-idempotent-id-circle : + ¬ (is-prop (is-quasicoherently-idempotent (id {A = 𝕊¹}))) +is-not-prop-is-quasicoherently-idempotent-id-circle = ? +``` + +### Idempotent maps on sets are quasicoherently idempotent + +```agda +module _ + {l : Level} {A : UU l} (is-set-A : is-set A) {f : A → A} + where + + is-quasicoherently-idempotent-is-idempotent-is-set : + is-idempotent f → is-quasicoherently-idempotent f + pr1 (is-quasicoherently-idempotent-is-idempotent-is-set I) = I + pr2 (is-quasicoherently-idempotent-is-idempotent-is-set I) x = + eq-is-prop (is-set-A ((f ∘ f ∘ f) x) ((f ∘ f) x)) +``` + +### If `i` and `r` form an inclusion-retraction pair, then `i ∘ r` is quasicoherently idempotent + +This statement can be found as part of the proof of Lemma 3.6 in +{{#cite Shu17}}. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + (i : B → A) (r : A → B) (H : is-retraction i r) + where + + coherence-is-quasicoherently-idempotent-inclusion-retraction : + coherence-is-quasicoherently-idempotent + ( i ∘ r) + ( is-idempotent-inclusion-retraction i r H) + coherence-is-quasicoherently-idempotent-inclusion-retraction = + ( inv-preserves-comp-left-whisker-comp i r (i ·l H ·r r)) ∙h + ( double-whisker-comp² + ( i) + ( preserves-comp-left-whisker-comp r i H ∙h inv-coh-htpy-id H) + ( r)) + + is-quasicoherently-idempotent-inclusion-retraction : + is-quasicoherently-idempotent (i ∘ r) + is-quasicoherently-idempotent-inclusion-retraction = + ( is-idempotent-inclusion-retraction i r H , + coherence-is-quasicoherently-idempotent-inclusion-retraction) +``` + +### Quasicoherent idempotence is preserved by homotopies + +This fact does not explicitly appear in {{#cite Shu17}} although it is +implicitly used in Lemma 3.6. + +```agda +module _ + {l : Level} {A : UU l} {f g : A → A} (F : is-quasicoherently-idempotent f) + where + + abstract + coherence-is-quasicoherently-idempotent-htpy : + (H : g ~ f) → + coherence-is-quasicoherently-idempotent g + ( is-idempotent-htpy + ( is-idempotent-is-quasicoherently-idempotent F) + ( H)) + coherence-is-quasicoherently-idempotent-htpy H = + homotopy-reasoning + ( g ·l is-idempotent-htpy I H) + ~ ( H ·r (g ∘ g)) ∙h + ( f ·l (g ·l H ∙h H ·r f ∙h I ∙h inv-htpy H)) ∙h + ( inv-htpy (H ·r g)) + by + ( right-transpose-htpy-concat + ( g ·l is-idempotent-htpy I H) + ( H ·r g) + ( H ·r (g ∘ g) ∙h (f ·l (g ·l H ∙h H ·r f ∙h I ∙h inv-htpy H))) + ( inv-htpy (nat-htpy H ∘ (g ·l H ∙h H ·r f ∙h I ∙h inv-htpy H)))) + ~ g ·l H ·r g ∙h H ·r (f ∘ g) ∙h I ·r g ∙h inv-htpy (H ·r g) + by + ( ap-concat-htpy' + ( inv-htpy (H ·r g)) + ( ( ap-concat-htpy + ( H ·r ((g ∘ g))) + ( ( distributive-left-whisker-comp-concat f + ( g ·l H ∙h H ·r f ∙h I) + ( inv-htpy H)) ∙h + ( ap-concat-htpy' + ( f ·l inv-htpy H) + ( ( distributive-left-whisker-comp-concat f + ( g ·l H ∙h H ·r f) + ( I)) ∙h + ( ap-binary-concat-htpy + ( distributive-left-whisker-comp-concat f (g ·l H) (H ·r f)) + ( coh-is-quasicoherently-idempotent F)))) ∙h + ( assoc-htpy + ( f ·l g ·l H ∙h f ·l H ·r f) + ( I ·r f) + ( f ·l inv-htpy H)) ∙h + ( ap-concat-htpy + ( f ·l g ·l H ∙h f ·l H ·r f) + ( nat-htpy I ∘ inv-htpy H)) ∙h + ( inv-htpy + ( assoc-htpy + ( f ·l g ·l H ∙h f ·l H ·r f) + ( (f ∘ f) ·l inv-htpy H) + ( I ·r g))))) ∙h + ( inv-htpy + ( assoc-htpy + ( H ·r (g ∘ g)) + ( f ·l g ·l H ∙h f ·l H ·r f ∙h (f ∘ f) ·l inv-htpy H) + ( I ·r g))) ∙h + ( ap-concat-htpy' + ( I ·r g) + ( ( ap-concat-htpy + ( H ·r (g ∘ g)) + ( ap-concat-htpy' + ( (f ∘ f) ·l inv-htpy H) + ( ( ap-concat-htpy' + ( f ·l H ·r f) + ( preserves-comp-left-whisker-comp f g H)) ∙h + ( inv-htpy (nat-htpy (f ·l H) ∘ H))) ∙h + ( ap-concat-htpy + ( f ·l H ·r g ∙h (f ∘ f) ·l H) + ( left-whisker-inv-htpy (f ∘ f) H)) ∙h + ( is-retraction-inv-concat-htpy' + ( (f ∘ f) ·l H) + ( f ·l H ·r g)))) ∙h + ( nat-htpy H ∘ (H ·r g)))))) + where + I : is-idempotent f + I = is-idempotent-is-quasicoherently-idempotent F + + is-quasicoherently-idempotent-htpy : + g ~ f → is-quasicoherently-idempotent g + pr1 (is-quasicoherently-idempotent-htpy H) = + is-idempotent-htpy + ( is-idempotent-is-quasicoherently-idempotent F) + ( H) + pr2 (is-quasicoherently-idempotent-htpy H) = + coherence-is-quasicoherently-idempotent-htpy H + + is-quasicoherently-idempotent-inv-htpy : + f ~ g → is-quasicoherently-idempotent g + pr1 (is-quasicoherently-idempotent-inv-htpy H) = + is-idempotent-htpy + ( is-idempotent-is-quasicoherently-idempotent F) + ( inv-htpy H) + pr2 (is-quasicoherently-idempotent-inv-htpy H) = + coherence-is-quasicoherently-idempotent-htpy (inv-htpy H) +``` + +### Realigning the coherence of a quasicoherent idempotence proof + +Given a quasicoherently idempotent map `f`, any other idempotence homotopy +`I : f ∘ f ~ f` that is homotopic to the coherent one is also coherent. + +```agda +module _ + {l : Level} {A : UU l} {f : A → A} + (F : is-quasicoherently-idempotent f) + (I : f ∘ f ~ f) + where + + coherence-is-quasicoherently-idempotent-is-idempotent-htpy : + is-idempotent-is-quasicoherently-idempotent F ~ I → + coherence-is-quasicoherently-idempotent f I + coherence-is-quasicoherently-idempotent-is-idempotent-htpy α = + ( left-whisker-comp² f (inv-htpy α)) ∙h + ( coh-is-quasicoherently-idempotent F) ∙h + ( right-whisker-comp² α f) + + coherence-is-quasicoherently-idempotent-is-idempotent-inv-htpy : + I ~ is-idempotent-is-quasicoherently-idempotent F → + coherence-is-quasicoherently-idempotent f I + coherence-is-quasicoherently-idempotent-is-idempotent-inv-htpy α = + ( left-whisker-comp² f α) ∙h + ( coh-is-quasicoherently-idempotent F) ∙h + ( right-whisker-comp² (inv-htpy α) f) + + is-quasicoherently-idempotent-is-idempotent-htpy : + is-idempotent-is-quasicoherently-idempotent F ~ I → + is-quasicoherently-idempotent f + is-quasicoherently-idempotent-is-idempotent-htpy α = + ( I , coherence-is-quasicoherently-idempotent-is-idempotent-htpy α) + + is-quasicoherently-idempotent-is-idempotent-inv-htpy : + I ~ is-idempotent-is-quasicoherently-idempotent F → + is-quasicoherently-idempotent f + is-quasicoherently-idempotent-is-idempotent-inv-htpy α = + ( I , coherence-is-quasicoherently-idempotent-is-idempotent-inv-htpy α) +``` + +### Not every idempotent map is quasicoherently idempotent + +To be clear, what we are asking for is an idempotent map `f`, such that _no_ +idempotence homotopy `f ∘ f ~ f` is quasicoherent. A counterexample can be +constructed using the [cantor space](set-theory.cantor-space.md), see Section 4 +of {{#cite Shu17}} for more details. + +## See also + +- In [`foundation.split-idempotent-maps`](foundation.split-idempotent-maps.md) + we show that every quasicoherently idempotent map splits. Moreover, it is true + that split idempotent maps are a retract of quasicoherent idempotent maps. + +## References + +{{#bibliography}} {{#reference Shu17}} {{#reference Shu14SplittingIdempotents}} diff --git a/src/foundation/retractions.lagda.md b/src/foundation/retractions.lagda.md index fe2da2d349..2c623f4e14 100644 --- a/src/foundation/retractions.lagda.md +++ b/src/foundation/retractions.lagda.md @@ -11,7 +11,6 @@ open import foundation-core.retractions public ```agda open import foundation.coslice open import foundation.dependent-pair-types -open import foundation.retracts-of-types open import foundation.universe-levels open import foundation.whiskering-homotopies-composition @@ -19,6 +18,7 @@ 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.retracts-of-types ``` diff --git a/src/foundation/retracts-of-maps.lagda.md b/src/foundation/retracts-of-maps.lagda.md index fa6cbc559c..1ab6ec6ad7 100644 --- a/src/foundation/retracts-of-maps.lagda.md +++ b/src/foundation/retracts-of-maps.lagda.md @@ -17,7 +17,6 @@ open import foundation.homotopies-morphisms-arrows open import foundation.morphisms-arrows open import foundation.postcomposition-functions open import foundation.precomposition-functions -open import foundation.retracts-of-types open import foundation.universe-levels open import foundation.whiskering-homotopies-composition @@ -28,6 +27,7 @@ open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.retractions +open import foundation-core.retracts-of-types open import foundation-core.sections ``` diff --git a/src/foundation/retracts-of-types.lagda.md b/src/foundation/retracts-of-types.lagda.md index dcbdb1819b..12a25959b7 100644 --- a/src/foundation/retracts-of-types.lagda.md +++ b/src/foundation/retracts-of-types.lagda.md @@ -2,132 +2,168 @@ ```agda module foundation.retracts-of-types where + +open import foundation-core.retracts-of-types public ```
Imports ```agda -open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types -open import foundation.function-extensionality +open import foundation.equivalences +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.homotopy-algebra +open import foundation.homotopy-induction +open import foundation.structure-identity-principle +open import foundation.univalence open import foundation.universe-levels open import foundation.whiskering-homotopies-composition -open import foundation-core.function-types +open import foundation-core.contractible-types +open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types -open import foundation-core.postcomposition-functions -open import foundation-core.precomposition-functions -open import foundation-core.retractions -open import foundation-core.sections +open import foundation-core.torsorial-type-families ```
## Idea -We say that a type `A` is a **retract of** a type `B` if the types `A` and `B` -come equipped with **retract data**, i.e., with maps +We say that a type `A` is a +{{#concept "retract" Disambiguation="of types" Agda=retract}} of a type `B` if +the types `A` and `B` come equipped with +{{#concept "retract data" Disambiguation="of types" Agda=retract}}, i.e., with +maps ```text i r A -----> B -----> A ``` -and a [homotopy](foundation-core.homotopies.md) `r ∘ i ~ id`. The map `i` is -called the **inclusion** of the retract data, and the map `r` is called the +such that `r` is a [retraction](foundation-core.retractions.md) of `i`, i.e., +there is a [homotopy](foundation-core.homotopies.md) `r ∘ i ~ id`. The map `i` +is called the **inclusion** of the retract data, and the map `r` is called the **underlying map of the retraction**. -## Definitions - -### The type of witnesses that `A` is a retract of `B` - -The predicate `retract B` is used to assert that a type is a retract of `B`, -i.e., the type `retract B A` is the type of maps from `A` to `B` that come -equipped with a retraction. - -We also introduce more intuitive infix notation `A retract-of B` to assert that -`A` is a retract of `B`. - -```agda -retract : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) -retract B A = Σ (A → B) retraction - -infix 6 _retract-of_ - -_retract-of_ : - {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) -A retract-of B = retract B A - -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} (R : retract B A) - where - - inclusion-retract : A → B - inclusion-retract = pr1 R - - retraction-retract : retraction inclusion-retract - retraction-retract = pr2 R - - map-retraction-retract : B → A - map-retraction-retract = map-retraction inclusion-retract retraction-retract - - is-retraction-map-retraction-retract : - is-section map-retraction-retract inclusion-retract - is-retraction-map-retraction-retract = - is-retraction-map-retraction inclusion-retract retraction-retract - - section-retract : section map-retraction-retract - pr1 section-retract = inclusion-retract - pr2 section-retract = is-retraction-map-retraction-retract -``` - ## Properties -### If `A` is a retract of `B` with inclusion `i : A → B`, then `x ＝ y` is a retract of `i x ＝ i y` for any two elements `x y : A` - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} (R : A retract-of B) (x y : A) - where - - retract-eq : - (x ＝ y) retract-of (inclusion-retract R x ＝ inclusion-retract R y) - pr1 retract-eq = ap (inclusion-retract R) - pr2 retract-eq = retraction-ap (inclusion-retract R) (retraction-retract R) -``` - -### If `A` is a retract of `B` then `A → S` is a retract of `B → S` via precomposition +### Characterizing equality of retracts ```agda module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (R : A retract-of B) (S : UU l3) + {l1 l2 : Level} {A : UU l1} {B : UU l2} where - retract-precomp : - (A → S) retract-of (B → S) - pr1 retract-precomp = - precomp (map-retraction-retract R) S - pr1 (pr2 retract-precomp) = - precomp (inclusion-retract R) S - pr2 (pr2 retract-precomp) h = - eq-htpy (h ·l is-retraction-map-retraction-retract R) + coherence-htpy-retract : + (R S : A retract-of B) + (I : inclusion-retract R ~ inclusion-retract S) + (H : map-retraction-retract R ~ map-retraction-retract S) → + UU l1 + coherence-htpy-retract R S I H = + ( is-retraction-map-retraction-retract R) ~ + ( horizontal-concat-htpy H I ∙h is-retraction-map-retraction-retract S) + + htpy-retract : (R S : A retract-of B) → UU (l1 ⊔ l2) + htpy-retract R S = + Σ ( inclusion-retract R ~ inclusion-retract S) + ( λ I → + Σ ( map-retraction-retract R ~ map-retraction-retract S) + ( coherence-htpy-retract R S I)) + + refl-htpy-retract : (R : A retract-of B) → htpy-retract R R + refl-htpy-retract R = (refl-htpy , refl-htpy , refl-htpy) + + htpy-eq-retract : (R S : A retract-of B) → R ＝ S → htpy-retract R S + htpy-eq-retract R .R refl = refl-htpy-retract R + + is-torsorial-htpy-retract : + (R : A retract-of B) → is-torsorial (htpy-retract R) + is-torsorial-htpy-retract R = + is-torsorial-Eq-structure + ( is-torsorial-htpy (inclusion-retract R)) + ( inclusion-retract R , refl-htpy) + ( is-torsorial-Eq-structure + ( is-torsorial-htpy (map-retraction-retract R)) + ( map-retraction-retract R , refl-htpy) + ( is-torsorial-htpy (is-retraction-map-retraction-retract R))) + + is-equiv-htpy-eq-retract : + (R S : A retract-of B) → is-equiv (htpy-eq-retract R S) + is-equiv-htpy-eq-retract R = + fundamental-theorem-id (is-torsorial-htpy-retract R) (htpy-eq-retract R) + + equiv-htpy-eq-retract : (R S : A retract-of B) → (R ＝ S) ≃ htpy-retract R S + equiv-htpy-eq-retract R S = + ( htpy-eq-retract R S , is-equiv-htpy-eq-retract R S) + + eq-htpy-retract : (R S : A retract-of B) → htpy-retract R S → R ＝ S + eq-htpy-retract R S = map-inv-is-equiv (is-equiv-htpy-eq-retract R S) ``` -### If `A` is a retract of `B` then `S → A` is a retract of `S → B` via postcomposition +### Characterizing equality of the total type of retracts ```agda module _ - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (S : UU l3) (R : A retract-of B) + {l1 l2 : Level} {A : UU l1} where - retract-postcomp : - (S → A) retract-of (S → B) - pr1 retract-postcomp = - postcomp S (inclusion-retract R) - pr1 (pr2 retract-postcomp) = - postcomp S (map-retraction-retract R) - pr2 (pr2 retract-postcomp) h = - eq-htpy (is-retraction-map-retraction-retract R ·r h) + equiv-retracts : + {l3 : Level} (R : retracts l2 A) (S : retracts l3 A) → UU (l1 ⊔ l2 ⊔ l3) + equiv-retracts R S = + Σ ( type-retracts R ≃ type-retracts S) + ( λ e → + htpy-retract + ( retract-retracts R) + ( comp-retract (retract-retracts S) (retract-equiv e))) + + refl-equiv-retracts : (R : retracts l2 A) → equiv-retracts R R + refl-equiv-retracts R = + ( id-equiv , + refl-htpy , + refl-htpy , + ( ( inv-htpy + ( left-unit-law-left-whisker-comp + ( is-retraction-map-retraction-retracts R))) ∙h + ( inv-htpy-right-unit-htpy))) + + equiv-eq-retracts : (R S : retracts l2 A) → R ＝ S → equiv-retracts R S + equiv-eq-retracts R .R refl = refl-equiv-retracts R + + is-torsorial-equiv-retracts : + (R : retracts l2 A) → is-torsorial (equiv-retracts R) + is-torsorial-equiv-retracts R = + is-torsorial-Eq-structure + ( is-torsorial-equiv (type-retracts R)) + ( type-retracts R , id-equiv) + ( is-contr-equiv + ( Σ (retract A (type-retracts R)) (htpy-retract (retract-retracts R))) + ( equiv-tot + ( λ S → + equiv-tot + ( λ I → + equiv-tot + ( λ J → + equiv-concat-htpy' + ( is-retraction-map-retraction-retracts R) + ( ap-concat-htpy + ( horizontal-concat-htpy J I) + ( right-unit-htpy ∙h + left-unit-law-left-whisker-comp + ( is-retraction-map-retraction-retract S))))))) + ( is-torsorial-htpy-retract (retract-retracts R))) + + is-equiv-equiv-eq-retracts : + (R S : retracts l2 A) → is-equiv (equiv-eq-retracts R S) + is-equiv-equiv-eq-retracts R = + fundamental-theorem-id (is-torsorial-equiv-retracts R) (equiv-eq-retracts R) + + equiv-equiv-eq-retracts : (R S : retracts l2 A) → (R ＝ S) ≃ equiv-retracts R S + equiv-equiv-eq-retracts R S = + ( equiv-eq-retracts R S , is-equiv-equiv-eq-retracts R S) + + eq-equiv-retracts : (R S : retracts l2 A) → equiv-retracts R S → R ＝ S + eq-equiv-retracts R S = map-inv-is-equiv (is-equiv-equiv-eq-retracts R S) ``` ## See also diff --git a/src/foundation/sections.lagda.md b/src/foundation/sections.lagda.md index a7795d911d..0c9cd52162 100644 --- a/src/foundation/sections.lagda.md +++ b/src/foundation/sections.lagda.md @@ -13,7 +13,6 @@ open import foundation.action-on-identifications-functions open import foundation.commuting-triangles-of-homotopies open import foundation.dependent-pair-types open import foundation.function-extensionality -open import foundation.retracts-of-types open import foundation.structure-identity-principle open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels @@ -26,6 +25,7 @@ open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.injective-maps +open import foundation-core.retracts-of-types open import foundation-core.torsorial-type-families open import foundation-core.type-theoretic-principle-of-choice ``` diff --git a/src/foundation/sequential-limits.lagda.md b/src/foundation/sequential-limits.lagda.md index 563afddf8e..f2891ee0db 100644 --- a/src/foundation/sequential-limits.lagda.md +++ b/src/foundation/sequential-limits.lagda.md @@ -22,8 +22,6 @@ open import foundation.universal-property-sequential-limits open import foundation.universe-levels open import foundation-core.commuting-squares-of-homotopies -open import foundation-core.contractible-types -open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositions @@ -164,16 +162,23 @@ module _ {l : Level} (A : inverse-sequential-diagram l) where + coherence-Eq-standard-sequential-limit : + (s t : standard-sequential-limit A) + (H : + sequence-standard-sequential-limit A s ~ + sequence-standard-sequential-limit A t) → UU l + coherence-Eq-standard-sequential-limit s t H = + coherence-square-homotopies + ( H) + ( coherence-standard-sequential-limit A s) + ( coherence-standard-sequential-limit A t) + ( λ n → ap (map-inverse-sequential-diagram A n) (H (succ-ℕ n))) + Eq-standard-sequential-limit : (s t : standard-sequential-limit A) → UU l Eq-standard-sequential-limit s t = Σ ( sequence-standard-sequential-limit A s ~ sequence-standard-sequential-limit A t) - ( λ H → - coherence-square-homotopies - ( H) - ( coherence-standard-sequential-limit A s) - ( coherence-standard-sequential-limit A t) - ( λ n → ap (map-inverse-sequential-diagram A n) (H (succ-ℕ n)))) + ( coherence-Eq-standard-sequential-limit s t) refl-Eq-standard-sequential-limit : (s : standard-sequential-limit A) → Eq-standard-sequential-limit s s diff --git a/src/foundation/small-maps.lagda.md b/src/foundation/small-maps.lagda.md index 66a459477f..59c0c702b7 100644 --- a/src/foundation/small-maps.lagda.md +++ b/src/foundation/small-maps.lagda.md @@ -9,6 +9,8 @@ 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.split-idempotent-maps open import foundation.universe-levels open import foundation-core.fibers-of-maps @@ -20,7 +22,20 @@ open import foundation-core.small-types ## Idea -A map is said to be small if its fibers are small. +A map is said to be +{{#concept "small" Disambiguation="map of types" Agda=is-small-map}} if its +[fibers](foundation-core.fibers-of-maps.md) are +[small](foundation-core.small-types.md). + +More specifically, a map `f : A → B` is _small_ with respect to a universe `𝒰` +if, for every `b : B`, the fiber of `f` over `y` + +```text + fiber f b ≐ Σ (x : A), (f x ＝ b), +``` + +is [equivalent](foundation-core.equivalences.md) to a type in `𝒰` that may vary +depending on `b`. ## Definition @@ -38,25 +53,38 @@ is-small-map l {B = B} f = (b : B) → is-small l (fiber f b) ```agda abstract is-small-fiber : - (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → + {l l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → is-small l A → is-small l B → (b : B) → is-small l (fiber f b) - is-small-fiber l f H K b = + is-small-fiber f H K b = is-small-Σ H (λ a → is-locally-small-is-small K (f a) b) ``` ### Being a small map is a property ```agda -abstract - is-prop-is-small-map : - (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → - is-prop (is-small-map l f) - is-prop-is-small-map l f = - is-prop-Π (λ x → is-prop-is-small l (fiber f x)) - -is-small-map-Prop : - (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → - Prop (lsuc l ⊔ l1 ⊔ l2) -pr1 (is-small-map-Prop l f) = is-small-map l f -pr2 (is-small-map-Prop l f) = is-prop-is-small-map l f +module _ + (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + abstract + is-prop-is-small-map : is-prop (is-small-map l f) + is-prop-is-small-map = is-prop-Π (λ x → is-prop-is-small l (fiber f x)) + + is-small-map-Prop : Prop (lsuc l ⊔ l1 ⊔ l2) + is-small-map-Prop = is-small-map l f , is-prop-is-small-map +``` + +### Small maps are closed under retracts + +```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) + 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) ``` diff --git a/src/foundation/small-types.lagda.md b/src/foundation/small-types.lagda.md index 7ed5faf654..2d60593a75 100644 --- a/src/foundation/small-types.lagda.md +++ b/src/foundation/small-types.lagda.md @@ -37,7 +37,11 @@ is-small-is-surjective {f = f} H K L = is-small-equiv' ( im f) ( equiv-equiv-slice-uniqueness-im f id-emb - ( pair f refl-htpy) - ( is-image-is-surjective f id-emb (pair f refl-htpy) H)) + ( f , refl-htpy) + ( is-image-is-surjective f id-emb (f , refl-htpy) H)) ( replacement f K L) ``` + +## See also + +- [Small maps](foundation.small-maps.md) diff --git a/src/foundation/split-idempotent-maps.lagda.md b/src/foundation/split-idempotent-maps.lagda.md new file mode 100644 index 0000000000..5637824bc2 --- /dev/null +++ b/src/foundation/split-idempotent-maps.lagda.md @@ -0,0 +1,1204 @@ +# Split idempotent maps + +```agda +module foundation.split-idempotent-maps where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-higher-identifications-functions +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.fixed-points-endofunctions +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.homotopy-algebra +open import foundation.homotopy-induction +open import foundation.idempotent-maps +open import foundation.inverse-sequential-diagrams +open import foundation.path-algebra +open import foundation.quasicoherently-idempotent-maps +open import foundation.retracts-of-types +open import foundation.sequential-limits +open import foundation.structure-identity-principle +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.univalence +open import foundation.universe-levels +open import foundation.weakly-constant-maps +open import foundation.whiskering-homotopies-composition + +open import foundation-core.commuting-squares-of-homotopies +open import foundation-core.contractible-types +open import foundation-core.equality-dependent-pair-types +open import foundation-core.function-types +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.identity-types +open import foundation-core.propositions +open import foundation-core.retractions +open import foundation-core.sections +open import foundation-core.sets +open import foundation-core.small-types +open import foundation-core.torsorial-type-families +``` + +
+ +## Idea + +An endomap `f : A → A` is +{{#concept "split idempotent" Disambiguation="map of types" Agda=is-split-idempotent}} +if there is a type `B` and an inclusion-retraction pair `i , r` displaying `B` +as a [retract](foundation-core.retracts-of-types.md) of `A`, and such that +`H : i ∘ r ~ f`. In other words, if we have a commutative diagram + +```text + f + A ----> A + ∧ \ ∧ + i / \r / i + / ∨ / + B ====== B. +``` + +Observe that split idempotent maps are indeed +[idempotent](foundation.idempotent-maps.md), as witnessed by the composite + +```text + (H◽H)⁻¹ iRr H + f ∘ f ~ i ∘ r ∘ i ∘ r ~ i ∘ r ~ f +``` + +where `H : i ∘ r ~ f` and `R : r ∘ i ~ id`. + +One important fact about split idempotent maps is that every +[quasicoherently idempotent map](foundation.quasicoherently-idempotent-maps.md) +splits, and conversely, every split idempotent map is quasicoherently +idempotent. In fact, the type of proofs of split idempotence for an endomap `f` +is a retract of the type of proofs of quasicoherent idempotence. + +## Definitions + +### The structure on a map of being split idempotent + +```agda +is-split-idempotent : + {l1 : Level} (l2 : Level) {A : UU l1} → (A → A) → UU (l1 ⊔ lsuc l2) +is-split-idempotent l2 {A} f = + Σ ( UU l2) + ( λ B → + Σ ( B retract-of A) + ( λ R → inclusion-retract R ∘ map-retraction-retract R ~ f)) + +module _ + {l1 l2 : Level} {A : UU l1} {f : A → A} (H : is-split-idempotent l2 f) + where + + splitting-type-is-split-idempotent : UU l2 + splitting-type-is-split-idempotent = pr1 H + + retract-is-split-idempotent : + splitting-type-is-split-idempotent retract-of A + retract-is-split-idempotent = pr1 (pr2 H) + + inclusion-is-split-idempotent : splitting-type-is-split-idempotent → A + inclusion-is-split-idempotent = + inclusion-retract retract-is-split-idempotent + + map-retraction-is-split-idempotent : + A → splitting-type-is-split-idempotent + map-retraction-is-split-idempotent = + map-retraction-retract retract-is-split-idempotent + + retraction-is-split-idempotent : + retraction inclusion-is-split-idempotent + retraction-is-split-idempotent = + retraction-retract retract-is-split-idempotent + + is-retraction-map-retraction-is-split-idempotent : + is-retraction + ( inclusion-is-split-idempotent) + ( map-retraction-is-split-idempotent) + is-retraction-map-retraction-is-split-idempotent = + is-retraction-map-retraction-retract retract-is-split-idempotent + + htpy-is-split-idempotent : + inclusion-is-split-idempotent ∘ map-retraction-is-split-idempotent ~ + f + htpy-is-split-idempotent = pr2 (pr2 H) +``` + +### The type of split idempotent maps on a type + +```agda +split-idempotent-map : {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2) +split-idempotent-map l2 A = Σ (A → A) (is-split-idempotent l2) + +module _ + {l1 l2 : Level} {A : UU l1} (H : split-idempotent-map l2 A) + where + + map-split-idempotent-map : A → A + map-split-idempotent-map = pr1 H + + is-split-idempotent-split-idempotent-map : + is-split-idempotent l2 map-split-idempotent-map + is-split-idempotent-split-idempotent-map = pr2 H + + splitting-type-split-idempotent-map : UU l2 + splitting-type-split-idempotent-map = + splitting-type-is-split-idempotent + ( is-split-idempotent-split-idempotent-map) + + retract-split-idempotent-map : + splitting-type-split-idempotent-map retract-of A + retract-split-idempotent-map = + retract-is-split-idempotent is-split-idempotent-split-idempotent-map + + inclusion-split-idempotent-map : splitting-type-split-idempotent-map → A + inclusion-split-idempotent-map = + inclusion-is-split-idempotent is-split-idempotent-split-idempotent-map + + map-retraction-split-idempotent-map : A → splitting-type-split-idempotent-map + map-retraction-split-idempotent-map = + map-retraction-is-split-idempotent + ( is-split-idempotent-split-idempotent-map) + + retraction-split-idempotent-map : retraction inclusion-split-idempotent-map + retraction-split-idempotent-map = + retraction-is-split-idempotent is-split-idempotent-split-idempotent-map + + is-retraction-map-retraction-split-idempotent-map : + is-retraction + ( inclusion-split-idempotent-map) + ( map-retraction-split-idempotent-map) + is-retraction-map-retraction-split-idempotent-map = + is-retraction-map-retraction-is-split-idempotent + ( is-split-idempotent-split-idempotent-map) + + htpy-split-idempotent-map : + inclusion-split-idempotent-map ∘ map-retraction-split-idempotent-map ~ + map-split-idempotent-map + htpy-split-idempotent-map = + htpy-is-split-idempotent is-split-idempotent-split-idempotent-map +``` + +## Properties + +### Split idempotence is closed under homotopies of functions + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {f g : A → A} + (H : f ~ g) + (S : is-split-idempotent l3 f) + where + + is-split-idempotent-htpy : is-split-idempotent l3 g + is-split-idempotent-htpy = + ( splitting-type-is-split-idempotent S , + retract-is-split-idempotent S , + htpy-is-split-idempotent S ∙h H) +``` + +### Split idempotence is closed under equivalences of splitting types + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {f : A → A} + (H : is-split-idempotent l3 f) + (e : B ≃ splitting-type-is-split-idempotent H) + where + + inclusion-is-split-idempotent-equiv-splitting-type : B → A + inclusion-is-split-idempotent-equiv-splitting-type = + inclusion-is-split-idempotent H ∘ map-equiv e + + map-retraction-is-split-idempotent-equiv-splitting-type : A → B + map-retraction-is-split-idempotent-equiv-splitting-type = + map-inv-equiv e ∘ map-retraction-is-split-idempotent H + + htpy-is-split-idempotent-equiv-splitting-type : + inclusion-is-split-idempotent-equiv-splitting-type ∘ + map-retraction-is-split-idempotent-equiv-splitting-type ~ + f + htpy-is-split-idempotent-equiv-splitting-type = + ( double-whisker-comp + ( inclusion-is-split-idempotent H) + ( is-section-map-section-map-equiv e) + ( map-retraction-is-split-idempotent H)) ∙h + ( htpy-is-split-idempotent H) + + is-split-idempotent-equiv-splitting-type : + is-split-idempotent l2 f + is-split-idempotent-equiv-splitting-type = + ( B , + comp-retract (retract-is-split-idempotent H) (retract-equiv e) , + htpy-is-split-idempotent-equiv-splitting-type) +``` + +### The splitting type of a split idempotent map is essentially unique + +This is Lemma 3.4 in {{#cite Shu17}}. Note that it does not require any +postulates. + +**Proof.** Given two splittings of an endomap `f : A → A`, with +inclusion-retraction pairs `i , r` and `i' , r'`, we get mutual inverse maps +between the splitting types + +```text + r' ∘ i : B → B' and r ∘ i' : B' → B. +``` + +The computation that they form mutual inverses is straightforward: + +```text + rR'i R + r ∘ i' ∘ r' ∘ i ~ r ∘ i ~ id. +``` + +```agda +module _ + {l1 : Level} {A : UU l1} {f : A → A} + where + + map-essentially-unique-splitting-type-is-split-idempotent : + {l2 l3 : Level} + (H : is-split-idempotent l2 f) + (H' : is-split-idempotent l3 f) → + splitting-type-is-split-idempotent H → + splitting-type-is-split-idempotent H' + map-essentially-unique-splitting-type-is-split-idempotent H H' = + map-retraction-is-split-idempotent H' ∘ + inclusion-is-split-idempotent H + + is-fibered-involution-essentially-unique-splitting-type-is-split-idempotent' : + {l2 l3 : Level} + (H : is-split-idempotent l2 f) + (H' : is-split-idempotent l3 f) → + is-section + ( map-essentially-unique-splitting-type-is-split-idempotent H H') + ( map-essentially-unique-splitting-type-is-split-idempotent H' H) + is-fibered-involution-essentially-unique-splitting-type-is-split-idempotent' + H H' = + ( map-retraction-is-split-idempotent H' ·l + ( ( htpy-is-split-idempotent H) ∙h + ( inv-htpy (htpy-is-split-idempotent H'))) ·r + inclusion-is-split-idempotent H') ∙h + ( horizontal-concat-htpy + ( is-retraction-map-retraction-is-split-idempotent H') + ( is-retraction-map-retraction-is-split-idempotent H')) + + is-equiv-map-essentially-unique-splitting-type-is-split-idempotent : + {l2 l3 : Level} + (H : is-split-idempotent l2 f) + (H' : is-split-idempotent l3 f) → + is-equiv + ( map-essentially-unique-splitting-type-is-split-idempotent H H') + is-equiv-map-essentially-unique-splitting-type-is-split-idempotent H H' = + is-equiv-is-invertible + ( map-essentially-unique-splitting-type-is-split-idempotent H' H) + ( is-fibered-involution-essentially-unique-splitting-type-is-split-idempotent' + ( H) + ( H')) + ( is-fibered-involution-essentially-unique-splitting-type-is-split-idempotent' + ( H') + ( H)) + + essentially-unique-splitting-type-is-split-idempotent : + {l2 l3 : Level} + (H : is-split-idempotent l2 f) + (H' : is-split-idempotent l3 f) → + splitting-type-is-split-idempotent H ≃ + splitting-type-is-split-idempotent H' + essentially-unique-splitting-type-is-split-idempotent H H' = + ( map-essentially-unique-splitting-type-is-split-idempotent H H' , + is-equiv-map-essentially-unique-splitting-type-is-split-idempotent + ( H) + ( H')) +``` + +### The type of split idempotent maps on `A` is equivalent to retracts of `A` + +Note that the proof relies on the +[function extensionality](foundation.function-extensionality.md) axiom. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} + where + + compute-split-idempotent-map : split-idempotent-map l2 A ≃ retracts l2 A + compute-split-idempotent-map = + equivalence-reasoning + Σ ( A → A) + ( λ f → + Σ ( UU l2) + ( λ B → + Σ ( B retract-of A) + ( λ (i , r , R) → i ∘ r ~ f))) + ≃ Σ (A → A) (λ f → (Σ (retracts l2 A) (λ (B , i , r , R) → i ∘ r ~ f))) + by + equiv-tot + ( λ f → + inv-associative-Σ + ( UU l2) + ( _retract-of A) + ( λ (B , i , r , R) → i ∘ r ~ f)) + ≃ Σ (retracts l2 A) (λ (B , i , r , R) → Σ (A → A) (λ f → i ∘ r ~ f)) + by equiv-left-swap-Σ + ≃ retracts l2 A + by equiv-pr1 (λ (B , i , r , R) → is-torsorial-htpy (i ∘ r)) +``` + +### Characterizing equality of split idempotence structures + +We characterize equality of witnesses that an endomap `f` is split idempotent as +equivalences of splitting types such that the evident retracts are homotopic. In +particular, this characterization relies on the univalence axiom. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {f : A → A} + where + + coherence-equiv-is-split-idempotent : + {l3 : Level} + (R : is-split-idempotent l2 f) + (S : is-split-idempotent l3 f) → + (e : + splitting-type-is-split-idempotent R ≃ + splitting-type-is-split-idempotent S) + ( H : + htpy-retract + ( retract-is-split-idempotent R) + ( comp-retract (retract-is-split-idempotent S) (retract-equiv e))) → + UU l1 + coherence-equiv-is-split-idempotent R S e H = + htpy-is-split-idempotent R ~ + horizontal-concat-htpy (pr1 H) (pr1 (pr2 H)) ∙h + htpy-is-split-idempotent-equiv-splitting-type S e + + equiv-is-split-idempotent : + {l3 : Level} + (R : is-split-idempotent l2 f) + (S : is-split-idempotent l3 f) → + UU (l1 ⊔ l2 ⊔ l3) + equiv-is-split-idempotent R S = + Σ ( splitting-type-is-split-idempotent R ≃ + splitting-type-is-split-idempotent S) + ( λ e → + Σ ( htpy-retract + ( retract-is-split-idempotent R) + ( comp-retract + ( retract-is-split-idempotent S) + ( retract-equiv e))) + ( coherence-equiv-is-split-idempotent R S e)) + + id-equiv-is-split-idempotent : + (R : is-split-idempotent l2 f) → equiv-is-split-idempotent R R + id-equiv-is-split-idempotent R = + ( ( id-equiv) , + ( refl-htpy , + refl-htpy , + ( inv-htpy + ( left-unit-law-left-whisker-comp + ( is-retraction-map-retraction-is-split-idempotent R)) ∙h + inv-htpy-right-unit-htpy)) , + ( refl-htpy)) + + equiv-eq-is-split-idempotent : + (R S : is-split-idempotent l2 f) → + R ＝ S → equiv-is-split-idempotent R S + equiv-eq-is-split-idempotent R .R refl = + id-equiv-is-split-idempotent R + + abstract + is-torsorial-equiv-is-split-idempotent : + (R : is-split-idempotent l2 f) → + is-torsorial (equiv-is-split-idempotent {l2} R) + is-torsorial-equiv-is-split-idempotent R = + is-torsorial-Eq-structure + ( is-torsorial-equiv (splitting-type-is-split-idempotent R)) + ( splitting-type-is-split-idempotent R , id-equiv) + ( is-torsorial-Eq-structure + ( is-contr-equiv + ( Σ ( (splitting-type-is-split-idempotent R) retract-of A) + ( htpy-retract (retract-is-split-idempotent R))) + ( equiv-tot + ( λ S → + equiv-tot + ( λ I → + equiv-tot + ( λ J → + equiv-concat-htpy' + ( is-retraction-map-retraction-is-split-idempotent + ( R)) + ( ap-concat-htpy + ( horizontal-concat-htpy J I) + ( right-unit-htpy ∙h + left-unit-law-left-whisker-comp + ( is-retraction-map-retraction-retract S))))))) + ( is-torsorial-htpy-retract (retract-is-split-idempotent R))) + ( ( retract-is-split-idempotent R) , + ( ( refl-htpy) , + ( refl-htpy) , + ( inv-htpy + ( left-unit-law-left-whisker-comp + ( is-retraction-map-retraction-is-split-idempotent R)) ∙h + inv-htpy-right-unit-htpy))) + ( is-torsorial-htpy (htpy-is-split-idempotent R))) + + is-equiv-equiv-eq-is-split-idempotent : + (R S : is-split-idempotent l2 f) → + is-equiv (equiv-eq-is-split-idempotent R S) + is-equiv-equiv-eq-is-split-idempotent R = + fundamental-theorem-id + ( is-torsorial-equiv-is-split-idempotent R) + ( equiv-eq-is-split-idempotent R) + + equiv-equiv-eq-is-split-idempotent : + (R S : is-split-idempotent l2 f) → + (R ＝ S) ≃ equiv-is-split-idempotent R S + equiv-equiv-eq-is-split-idempotent R S = + ( equiv-eq-is-split-idempotent R S , + is-equiv-equiv-eq-is-split-idempotent R S) + + eq-equiv-is-split-idempotent : + (R S : is-split-idempotent l2 f) → + equiv-is-split-idempotent R S → R ＝ S + eq-equiv-is-split-idempotent R S = + map-inv-is-equiv (is-equiv-equiv-eq-is-split-idempotent R S) +``` + +### Split idempotent maps are idempotent + +This is Lemma 3.3 in {{#cite Shu17}}. + +**Proof.** Given a split idempotent map `f` with splitting `R : r ∘ i ~ id` and +homotopy `H : i ∘ r ~ f`, then `f` is idempotent via the following witness + +```text + (H◽H)⁻¹ iRr H + f ∘ f ~ i ∘ r ∘ i ∘ r ~ i ∘ r ~ f. +``` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {f : A → A} (H : is-split-idempotent l2 f) + where + + is-idempotent-is-split-idempotent : is-idempotent f + is-idempotent-is-split-idempotent = + is-idempotent-inv-htpy + ( is-idempotent-inclusion-retraction + ( inclusion-is-split-idempotent H) + ( map-retraction-is-split-idempotent H) + ( is-retraction-map-retraction-is-split-idempotent H)) + ( htpy-is-split-idempotent H) + +module _ + {l1 l2 : Level} {A : UU l1} (H : split-idempotent-map l2 A) + where + + is-idempotent-split-idempotent-map : + is-idempotent (map-split-idempotent-map H) + is-idempotent-split-idempotent-map = + is-idempotent-is-split-idempotent + ( is-split-idempotent-split-idempotent-map H) +``` + +### Split idempotent maps are quasicoherently idempotent + +This is Lemma 3.6 in {{#cite Shu17}}. + +**Proof.** Inclusion-retraction composites are quasicoherently idempotent, so +since quasicoherently idempotent maps are closed under homotopy we are done. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {f : A → A} (H : is-split-idempotent l2 f) + where + + abstract + coherence-is-quasicoherently-idempotent-is-split-idempotent : + coherence-is-quasicoherently-idempotent f + ( is-idempotent-is-split-idempotent H) + coherence-is-quasicoherently-idempotent-is-split-idempotent = + coherence-is-quasicoherently-idempotent-is-idempotent-htpy + ( is-quasicoherently-idempotent-inv-htpy + ( is-quasicoherently-idempotent-inclusion-retraction + ( inclusion-is-split-idempotent H) + ( map-retraction-is-split-idempotent H) + (is-retraction-map-retraction-is-split-idempotent H)) + ( htpy-is-split-idempotent H)) + ( is-idempotent-is-split-idempotent H) + ( ap-concat-htpy _ (inv-inv-htpy (htpy-is-split-idempotent H))) + + is-quasicoherently-idempotent-is-split-idempotent : + is-quasicoherently-idempotent f + is-quasicoherently-idempotent-is-split-idempotent = + ( is-idempotent-is-split-idempotent H , + coherence-is-quasicoherently-idempotent-is-split-idempotent) + +module _ + {l1 l2 : Level} {A : UU l1} (H : split-idempotent-map l2 A) + where + + is-quasicoherently-idempotent-split-idempotent-map : + is-quasicoherently-idempotent (map-split-idempotent-map H) + is-quasicoherently-idempotent-split-idempotent-map = + is-quasicoherently-idempotent-is-split-idempotent + ( is-split-idempotent-split-idempotent-map H) +``` + +### Every idempotent map on a set splits + +This is Theorem 3.7 of {{#cite Shu17}}. + +```agda +module _ + {l : Level} {A : UU l} {f : A → A} + (is-set-A : is-set A) (H : is-idempotent f) + where + + splitting-type-is-split-idempotent-is-idempotent-is-set : UU l + splitting-type-is-split-idempotent-is-idempotent-is-set = + fixed-point f + + inclusion-is-split-idempotent-is-idempotent-is-set : + splitting-type-is-split-idempotent-is-idempotent-is-set → A + inclusion-is-split-idempotent-is-idempotent-is-set = pr1 + + map-retraction-is-split-idempotent-is-idempotent-is-set : + A → splitting-type-is-split-idempotent-is-idempotent-is-set + map-retraction-is-split-idempotent-is-idempotent-is-set x = (f x , H x) + + is-retraction-map-retraction-is-split-idempotent-is-idempotent-is-set : + is-retraction + ( inclusion-is-split-idempotent-is-idempotent-is-set) + ( map-retraction-is-split-idempotent-is-idempotent-is-set) + is-retraction-map-retraction-is-split-idempotent-is-idempotent-is-set + (x , p) = + eq-pair-Σ p (eq-is-prop (is-set-A (f x) x)) + + retraction-is-split-idempotent-is-idempotent-is-set : + retraction (inclusion-is-split-idempotent-is-idempotent-is-set) + retraction-is-split-idempotent-is-idempotent-is-set = + ( map-retraction-is-split-idempotent-is-idempotent-is-set , + is-retraction-map-retraction-is-split-idempotent-is-idempotent-is-set) + + retract-is-split-idempotent-is-idempotent-is-set : + splitting-type-is-split-idempotent-is-idempotent-is-set retract-of A + retract-is-split-idempotent-is-idempotent-is-set = + ( inclusion-is-split-idempotent-is-idempotent-is-set , + retraction-is-split-idempotent-is-idempotent-is-set) + + htpy-is-split-idempotent-is-idempotent-is-set : + inclusion-is-split-idempotent-is-idempotent-is-set ∘ + map-retraction-is-split-idempotent-is-idempotent-is-set ~ + f + htpy-is-split-idempotent-is-idempotent-is-set = refl-htpy + + is-split-idempotent-is-idempotent-is-set : is-split-idempotent l f + is-split-idempotent-is-idempotent-is-set = + ( splitting-type-is-split-idempotent-is-idempotent-is-set , + retract-is-split-idempotent-is-idempotent-is-set , + htpy-is-split-idempotent-is-idempotent-is-set) +``` + +### Weakly constant idempotent maps split + +This is Theorem 3.9 of {{#cite Shu17}}. + +```agda +module _ + {l : Level} {A : UU l} {f : A → A} + (H : is-idempotent f) (W : is-weakly-constant f) + where + + splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent : + UU l + splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent = + fixed-point f + + inclusion-is-split-idempotent-is-weakly-constant-is-idempotent : + splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent → + A + inclusion-is-split-idempotent-is-weakly-constant-is-idempotent = pr1 + + map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent : + A → + splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent + map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent x = + ( f x , H x) + + is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent : + is-retraction + ( inclusion-is-split-idempotent-is-weakly-constant-is-idempotent) + ( map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent) + is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent + _ = + eq-is-prop (is-prop-fixed-point-is-weakly-constant W) + + retraction-is-split-idempotent-is-weakly-constant-is-idempotent : + retraction + ( inclusion-is-split-idempotent-is-weakly-constant-is-idempotent) + retraction-is-split-idempotent-is-weakly-constant-is-idempotent = + ( map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent , + is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent) + + retract-is-split-idempotent-is-weakly-constant-is-idempotent : + retract + ( A) + ( splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent) + retract-is-split-idempotent-is-weakly-constant-is-idempotent = + ( inclusion-is-split-idempotent-is-weakly-constant-is-idempotent , + retraction-is-split-idempotent-is-weakly-constant-is-idempotent) + + htpy-is-split-idempotent-is-weakly-constant-is-idempotent : + inclusion-is-split-idempotent-is-weakly-constant-is-idempotent ∘ + map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent ~ + f + htpy-is-split-idempotent-is-weakly-constant-is-idempotent = refl-htpy + + is-split-idempotent-is-weakly-constant-is-idempotent : + is-split-idempotent l f + is-split-idempotent-is-weakly-constant-is-idempotent = + ( splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent , + retract-is-split-idempotent-is-weakly-constant-is-idempotent , + htpy-is-split-idempotent-is-weakly-constant-is-idempotent) +``` + +### Quasicoherently idempotent maps split + +This is Theorem 5.3 of {{#cite Shu17}}. + +As per Remark 5.4 {{#cite Shu17}}, the inclusion of `A` into the splitting type +can be constructed for any endofunction `f`. + +```agda +module _ + {l : Level} {A : UU l} (f : A → A) + where + + inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent' : + inverse-sequential-diagram l + inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent' = + ( (λ _ → A) , (λ _ → f)) + + splitting-type-is-quasicoherently-idempotent' : UU l + splitting-type-is-quasicoherently-idempotent' = + standard-sequential-limit + ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent') + + inclusion-splitting-type-is-quasicoherently-idempotent' : + splitting-type-is-quasicoherently-idempotent' → A + inclusion-splitting-type-is-quasicoherently-idempotent' (a , α) = a 0 +``` + +Moreover, again by Remark 5.4 {{#cite Shu17}}, given only the idempotence +homotopy `f ∘ f ~ f`, we can construct the converse map to this inclusion and +show that this gives a factorization of `f`. Indeed, this factorization is +strict. + +```agda +module _ + {l : Level} {A : UU l} {f : A → A} + (I : is-idempotent f) + where + + map-retraction-splitting-type-is-quasicoherently-idempotent' : + A → splitting-type-is-quasicoherently-idempotent' f + map-retraction-splitting-type-is-quasicoherently-idempotent' x = + ( (λ _ → f x) , (λ _ → inv (I x))) + + htpy-is-split-idempotent-is-quasicoherently-idempotent' : + inclusion-splitting-type-is-quasicoherently-idempotent' f ∘ + map-retraction-splitting-type-is-quasicoherently-idempotent' ~ + f + htpy-is-split-idempotent-is-quasicoherently-idempotent' = refl-htpy +``` + +However, to show that these maps form an inclusion-retraction pair, we use the +coherence of quasicoherent idempotents as well as the function extensionality +axiom. + +```agda +module _ + {l : Level} {A : UU l} {f : A → A} + (H : is-quasicoherently-idempotent f) + where + + inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent : + inverse-sequential-diagram l + inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent = + inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent' + ( f) + + splitting-type-is-quasicoherently-idempotent : UU l + splitting-type-is-quasicoherently-idempotent = + splitting-type-is-quasicoherently-idempotent' f + + inclusion-splitting-type-is-quasicoherently-idempotent : + splitting-type-is-quasicoherently-idempotent → A + inclusion-splitting-type-is-quasicoherently-idempotent = + inclusion-splitting-type-is-quasicoherently-idempotent' f + + map-retraction-splitting-type-is-quasicoherently-idempotent : + A → splitting-type-is-quasicoherently-idempotent + map-retraction-splitting-type-is-quasicoherently-idempotent = + map-retraction-splitting-type-is-quasicoherently-idempotent' + ( is-idempotent-is-quasicoherently-idempotent H) + + htpy-is-split-idempotent-is-quasicoherently-idempotent : + inclusion-splitting-type-is-quasicoherently-idempotent ∘ + map-retraction-splitting-type-is-quasicoherently-idempotent ~ + f + htpy-is-split-idempotent-is-quasicoherently-idempotent = + htpy-is-split-idempotent-is-quasicoherently-idempotent' + ( is-idempotent-is-quasicoherently-idempotent H) +``` + +Now, to construct the desired retracting homotopy + +```text + r ∘ i ~ id +``` + +we subdivide the problem into two. First, we show that shifting the sequence and +whiskering by `f ∘ f` is homotopic to the identity + +```text + ((f (f a₍₋₎₊₁)) , (f ∘ f) ·l α₍₋₎₊₁) ~ (a , α). +``` + +```agda + shift-retraction-splitting-type-is-quasicoherently-idempotent : + standard-sequential-limit + ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent) → + standard-sequential-limit + ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent) + shift-retraction-splitting-type-is-quasicoherently-idempotent (a , α) = + ((f ∘ f ∘ a ∘ succ-ℕ) , ( (f ∘ f) ·l (α ∘ succ-ℕ))) + + htpy-sequence-shift-retraction-splitting-type-is-quasicoherently-idempotent : + ((a , α) : + standard-sequential-limit + ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent)) → + f ∘ f ∘ a ∘ succ-ℕ ~ a + htpy-sequence-shift-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α) n = + is-idempotent-is-quasicoherently-idempotent H (a (succ-ℕ n)) ∙ inv (α n) + + abstract + htpy-coherence-shift-retraction-splitting-type-is-quasicoherently-idempotent : + (x : + standard-sequential-limit + ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent)) → + coherence-Eq-standard-sequential-limit + ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent) + ( shift-retraction-splitting-type-is-quasicoherently-idempotent x) + ( x) + ( htpy-sequence-shift-retraction-splitting-type-is-quasicoherently-idempotent + ( x)) + htpy-coherence-shift-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α) n = + ( ap + ( ap (f ∘ f) (α (succ-ℕ n)) ∙_) + ( ( ap-concat f + ( is-idempotent-is-quasicoherently-idempotent H + ( a (second-succ-ℕ n))) + ( inv (α (succ-ℕ n)))) ∙ + ( ap + ( _∙ ap f (inv (α (succ-ℕ n)))) + ( coh-is-quasicoherently-idempotent H + ( a (second-succ-ℕ n)))))) ∙ + ( inv + ( assoc + ( ap (f ∘ f) (α (succ-ℕ n))) + ( is-idempotent-is-quasicoherently-idempotent H + ( f (a (second-succ-ℕ n)))) + ( ap f (inv (α (succ-ℕ n)))))) ∙ + ( ap + ( _∙ ap f (inv (α (succ-ℕ n)))) + ( inv + ( nat-htpy + ( is-idempotent-is-quasicoherently-idempotent H) + ( α (succ-ℕ n))))) ∙ + ( assoc + ( is-idempotent-is-quasicoherently-idempotent H (a (succ-ℕ n))) + ( ap f (α (succ-ℕ n))) + ( ap f (inv (α (succ-ℕ n))))) ∙ + ( ap + ( is-idempotent-is-quasicoherently-idempotent H (a (succ-ℕ n)) ∙_) + ( ( inv (ap-concat f (α (succ-ℕ n)) (inv (α (succ-ℕ n))))) ∙ + ( ap² f (right-inv (α (succ-ℕ n)))) ∙ + inv (left-inv (α n)))) ∙ + ( inv + ( assoc + ( is-idempotent-is-quasicoherently-idempotent H (a (succ-ℕ n))) + ( inv (α n)) + ( α n))) + + compute-shift-retraction-splitting-type-is-quasicoherently-idempotent : + shift-retraction-splitting-type-is-quasicoherently-idempotent ~ id + compute-shift-retraction-splitting-type-is-quasicoherently-idempotent + x = + eq-Eq-standard-sequential-limit + ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent) + ( shift-retraction-splitting-type-is-quasicoherently-idempotent x) + ( x) + ( ( htpy-sequence-shift-retraction-splitting-type-is-quasicoherently-idempotent + x) , + ( htpy-coherence-shift-retraction-splitting-type-is-quasicoherently-idempotent + x)) +``` + +Then we show that `r ∘ i` is homotopic to this operation. This time we proceed +by induction on `n`. + +```agda + htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent : + ( (a , α) : + standard-sequential-limit + ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent' + ( f))) → + ( λ _ → + f (inclusion-splitting-type-is-quasicoherently-idempotent (a , α))) ~ + ( f ∘ f ∘ a ∘ succ-ℕ) + htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α) 0 = ap f (α 0) + htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α) (succ-ℕ n) = + ( htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α) n) ∙ + ( is-idempotent-is-quasicoherently-idempotent H (a (succ-ℕ n))) ∙ + ( ap f (α (succ-ℕ n))) + + abstract + htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent : + ((a , α) : + standard-sequential-limit + ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent)) → + coherence-square-homotopies + ( htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α)) + ( λ n → + inv + ( is-idempotent-is-quasicoherently-idempotent H + ( inclusion-splitting-type-is-quasicoherently-idempotent + ( a , α)))) + ( λ n → ap (f ∘ f) (α (succ-ℕ n))) + ( λ n → + ap f + ( ( htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α) + ( n)) ∙ + ( is-idempotent-is-quasicoherently-idempotent H + ( a (succ-ℕ n))) ∙ + ( ap f (α (succ-ℕ n))))) + htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α) 0 = + ( ap + ( inv (is-idempotent-is-quasicoherently-idempotent H (a 0)) ∙_) + ( ( ap-concat f + ( ap f (α 0) ∙ + is-idempotent-is-quasicoherently-idempotent H (a 1)) + ( ap f (α 1))) ∙ + ( ap-binary (_∙_) + ( ap-concat f + ( ap f (α 0)) + ( is-idempotent-is-quasicoherently-idempotent H (a 1))) + ( inv (ap-comp f f (α 1)))))) ∙ + ( inv + ( assoc + ( inv (is-idempotent-is-quasicoherently-idempotent H (a 0))) + ( ap f (ap f (α 0)) ∙ + ap f (is-idempotent-is-quasicoherently-idempotent H (a 1))) + ( ap (f ∘ f) (α 1)))) ∙ + ( ap + ( _∙ ap (f ∘ f) (α 1)) + ( ap + ( inv (is-idempotent-is-quasicoherently-idempotent H (a 0)) ∙_) + ( ( ap-binary (_∙_) + ( inv (ap-comp f f (α 0))) + ( coh-is-quasicoherently-idempotent H (a 1))) ∙ + ( inv + ( nat-htpy + ( is-idempotent-is-quasicoherently-idempotent H) (α 0)))) ∙ + ( is-retraction-inv-concat + ( is-idempotent-is-quasicoherently-idempotent H (a 0)) + ( ap f (α 0))))) +``` + +For the inductive step we fill the following diagram as prescribed, in the +notation of {{#cite Shu17}}: + +```text + ξₙ₊₁ I aₙ₊₁ f (αₙ₊₁)⁻¹ + f a₀ ------------> f (f aₙ₊₁) ---> f aₙ₊₁ --------------------> f (f aₙ₊₂) + | | [nat-htpy] ___refl___/ | + (I⁻¹ a₀) [Ξₙ] | I (f aₙ₊₂) / (f ∘ f)(αₙ₊₂) + ∨ ∨ ------> / ∨ + f (f a₀) --------> f (f (f aₙ₊₂)) [J] f (f aₙ₊₂) ----------> f (f (f aₙ₊₃)) + (f (ξₙ ∙ I aₙ₊₁ ∙ f αₙ₊₁)) ------> (f ∘ f) (αₙ₊₂) + f (I aₙ₊₂) +``` + +where the symbols translate to code as follows: + +```text +I = is-idempotent-is-quasicoherently-idempotent H +J = coh-is-quasicoherently-idempotent H +ξ = htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent (a , α) +Ξ = htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent (a , α). +``` + +Note, in particular, that the left-hand square is the inductive hypothesis. + +```agda + htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α) (succ-ℕ n) = + ( ap + ( inv (I (a 0)) ∙_) + ( ( ap-concat f + ( ξ (succ-ℕ n) ∙ I (a (second-succ-ℕ n))) + ( ap f (α (second-succ-ℕ n)))) ∙ + ( ap-binary (_∙_) + ( ap-concat f (ξ (succ-ℕ n)) (I (a (second-succ-ℕ n)))) + ( inv (ap-comp f f (α (second-succ-ℕ n))))))) ∙ + ( inv + ( assoc + ( inv (I (a 0))) + ( ap f + ( ξ n ∙ + I (a (succ-ℕ n)) ∙ + ap f (α (succ-ℕ n))) ∙ + ap f (I (a (second-succ-ℕ n)))) + ( ap (f ∘ f) (α (second-succ-ℕ n))))) ∙ + ( ap + ( _∙ ap (f ∘ f) (α (second-succ-ℕ n))) + ( ( inv + ( assoc + ( inv (I (a 0))) + ( ap f (ξ n ∙ I (a (succ-ℕ n)) ∙ ap f (α (succ-ℕ n)))) + ( ap f (I (a (second-succ-ℕ n)))))) ∙ + ( ap + ( _∙ ap f (I ( a (second-succ-ℕ n)))) + ( htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α) + ( n))) ∙ + ( assoc + ( ξ n) + ( ap (f ∘ f) (α (succ-ℕ n))) + ( ap f (I (a (second-succ-ℕ n))))) ∙ + ( ap + ( ξ n ∙_) + ( ap + ( ap (f ∘ f) (α (succ-ℕ n)) ∙_) + ( coh-is-quasicoherently-idempotent H + ( a (succ-ℕ (succ-ℕ n)))) ∙ + ( inv (nat-htpy I (α (succ-ℕ n)))))) ∙ + ( inv (assoc (ξ n) (I (a (succ-ℕ n))) (ap f (α (succ-ℕ n))))))) + where + ξ : + ( λ _ → + f ( inclusion-splitting-type-is-quasicoherently-idempotent + ( a , α))) ~ + ( f ∘ f ∘ a ∘ succ-ℕ) + ξ = + htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( a , α) + I : is-idempotent f + I = pr1 H +``` + +Now it only remains to put it all together. + +```agda + abstract + compute-retraction-splitting-type-is-quasicoherently-idempotent : + map-retraction-splitting-type-is-quasicoherently-idempotent ∘ + inclusion-splitting-type-is-quasicoherently-idempotent ~ + shift-retraction-splitting-type-is-quasicoherently-idempotent + compute-retraction-splitting-type-is-quasicoherently-idempotent + x = + eq-Eq-standard-sequential-limit + ( inverse-sequential-diagram-splitting-type-is-quasicoherently-idempotent) + ( map-retraction-splitting-type-is-quasicoherently-idempotent + ( inclusion-splitting-type-is-quasicoherently-idempotent x)) + ( shift-retraction-splitting-type-is-quasicoherently-idempotent + ( x)) + ( htpy-sequence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( x) , + htpy-coherence-compute-retraction-splitting-type-is-quasicoherently-idempotent + ( x)) + + is-retraction-map-retraction-splitting-type-is-quasicoherently-idempotent : + is-retraction + ( inclusion-splitting-type-is-quasicoherently-idempotent) + ( map-retraction-splitting-type-is-quasicoherently-idempotent) + is-retraction-map-retraction-splitting-type-is-quasicoherently-idempotent = + compute-retraction-splitting-type-is-quasicoherently-idempotent ∙h + compute-shift-retraction-splitting-type-is-quasicoherently-idempotent + + retraction-splitting-type-is-quasicoherently-idempotent : + retraction (inclusion-splitting-type-is-quasicoherently-idempotent) + retraction-splitting-type-is-quasicoherently-idempotent = + ( map-retraction-splitting-type-is-quasicoherently-idempotent , + is-retraction-map-retraction-splitting-type-is-quasicoherently-idempotent) + + retract-splitting-type-is-quasicoherently-idempotent : + splitting-type-is-quasicoherently-idempotent retract-of A + retract-splitting-type-is-quasicoherently-idempotent = + ( inclusion-splitting-type-is-quasicoherently-idempotent , + retraction-splitting-type-is-quasicoherently-idempotent) + + splitting-is-quasicoherently-idempotent : retracts l A + splitting-is-quasicoherently-idempotent = + ( splitting-type-is-quasicoherently-idempotent , + retract-splitting-type-is-quasicoherently-idempotent) + + is-split-idempotent-is-quasicoherently-idempotent : + is-split-idempotent l f + is-split-idempotent-is-quasicoherently-idempotent = + ( splitting-type-is-quasicoherently-idempotent , + retract-splitting-type-is-quasicoherently-idempotent , + htpy-is-split-idempotent-is-quasicoherently-idempotent) +``` + +We record these same facts for the bundled data of a quasicoherently idempotent +map on `A`. + +```agda +module _ + {l : Level} {A : UU l} (f : quasicoherently-idempotent-map A) + where + + splitting-type-quasicoherently-idempotent-map : UU l + splitting-type-quasicoherently-idempotent-map = + splitting-type-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) + + inclusion-splitting-type-quasicoherently-idempotent-map : + splitting-type-quasicoherently-idempotent-map → A + inclusion-splitting-type-quasicoherently-idempotent-map = + inclusion-splitting-type-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) + + map-retraction-splitting-type-quasicoherently-idempotent-map : + A → splitting-type-quasicoherently-idempotent-map + map-retraction-splitting-type-quasicoherently-idempotent-map = + map-retraction-splitting-type-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) + + is-retraction-map-retraction-splitting-type-quasicoherently-idempotent-map : + is-retraction + ( inclusion-splitting-type-quasicoherently-idempotent-map) + ( map-retraction-splitting-type-quasicoherently-idempotent-map) + is-retraction-map-retraction-splitting-type-quasicoherently-idempotent-map = + is-retraction-map-retraction-splitting-type-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) + + retraction-splitting-type-quasicoherently-idempotent-map : + retraction (inclusion-splitting-type-quasicoherently-idempotent-map) + retraction-splitting-type-quasicoherently-idempotent-map = + retraction-splitting-type-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) + + retract-splitting-type-quasicoherently-idempotent-map : + splitting-type-quasicoherently-idempotent-map retract-of A + retract-splitting-type-quasicoherently-idempotent-map = + retract-splitting-type-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) + + splitting-quasicoherently-idempotent-map : retracts l A + splitting-quasicoherently-idempotent-map = + splitting-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) + + htpy-is-split-idempotent-quasicoherently-idempotent-map : + inclusion-splitting-type-quasicoherently-idempotent-map ∘ + map-retraction-splitting-type-quasicoherently-idempotent-map ~ + map-quasicoherently-idempotent-map f + htpy-is-split-idempotent-quasicoherently-idempotent-map = + htpy-is-split-idempotent-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) + + is-split-idempotent-quasicoherently-idempotent-map : + is-split-idempotent l (map-quasicoherently-idempotent-map f) + is-split-idempotent-quasicoherently-idempotent-map = + is-split-idempotent-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-quasicoherently-idempotent-map f) +``` + +### If a map is split idempotent at any universe level, it is split idempotent at its own universe level + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {f : A → A} (S : is-split-idempotent l2 f) + where + + is-small-split-idempotent-is-split-idempotent : + is-split-idempotent l1 f + is-small-split-idempotent-is-split-idempotent = + is-split-idempotent-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-is-split-idempotent S) +``` + +### Small types are closed under retracts + + + +This is Theorem 2.13 of {{#cite dJE23}}. Note, in particular, that it does not +rely on univalence. + +**Proof:** Assume given an inclusion-retraction pair `i , r` that displays `B` +as a retract of the small type `A`. By essential uniqueness of splitting types, +`B` is equivalent to every other splitting type of `i ∘ r`. Now, another +splitting type of `i ∘ r` is the splitting type as constructed for the witness + +```text + is-split-idempotent-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-inclusion-retraction i r ...), +``` + +and this is a small sequential limit. Hence `B` is equivalent to a small type, +and so is itself small. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-small-retract' : B retract-of A → is-small l1 B + pr1 (is-small-retract' R) = + splitting-type-is-quasicoherently-idempotent' + ( inclusion-retract R ∘ map-retraction-retract R) + pr2 (is-small-retract' R) = + essentially-unique-splitting-type-is-split-idempotent + ( B , R , refl-htpy) + ( is-split-idempotent-is-quasicoherently-idempotent + ( is-quasicoherently-idempotent-inclusion-retraction + ( inclusion-retract R) + ( map-retraction-retract R) + ( is-retraction-map-retraction-retract R))) + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} + where + + is-small-retract : is-small l3 A → B retract-of A → is-small l3 B + is-small-retract is-small-A r = + is-small-retract' + ( comp-retract (retract-equiv (equiv-is-small is-small-A)) r) +``` + +## References + +{{#bibliography}} {{#reference Shu17}} {{#reference Shu14SplittingIdempotents}} diff --git a/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md b/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md index e28331de4b..748f5c13d1 100644 --- a/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md +++ b/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md @@ -131,7 +131,7 @@ module _ left-inv-right-strict-concat : {x y : A} (p : x ＝ y) → inv p ∙ᵣ p ＝ refl left-inv-right-strict-concat refl = refl - right-inv-right-strict-concat : {x y : A} (p : x ＝ y) → p ∙ᵣ (inv p) ＝ refl + right-inv-right-strict-concat : {x y : A} (p : x ＝ y) → p ∙ᵣ inv p ＝ refl right-inv-right-strict-concat refl = refl inv-inv-right-strict-concat : {x y : A} (p : x ＝ y) → inv (inv p) ＝ p diff --git a/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md b/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md index 35ca2662b1..124181f37d 100644 --- a/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md +++ b/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md @@ -38,21 +38,21 @@ universal property of the propositional truncations with respect to sets. ### The precomposition map that is used to state the universal property ```agda -is-weakly-constant-map-precomp-unit-trunc-Prop : +is-weakly-constant-precomp-unit-trunc-Prop : {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : type-trunc-Prop A → B) → - is-weakly-constant-map (g ∘ unit-trunc-Prop) -is-weakly-constant-map-precomp-unit-trunc-Prop g x y = + is-weakly-constant (g ∘ unit-trunc-Prop) +is-weakly-constant-precomp-unit-trunc-Prop g x y = ap ( g) ( eq-is-prop (is-prop-type-trunc-Prop)) precomp-universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) → - (type-trunc-Prop A → type-Set B) → Σ (A → type-Set B) is-weakly-constant-map + (type-trunc-Prop A → type-Set B) → Σ (A → type-Set B) is-weakly-constant pr1 (precomp-universal-property-set-quotient-trunc-Prop B g) = g ∘ unit-trunc-Prop pr2 (precomp-universal-property-set-quotient-trunc-Prop B g) = - is-weakly-constant-map-precomp-unit-trunc-Prop g + is-weakly-constant-precomp-unit-trunc-Prop g ``` ## Properties @@ -61,11 +61,11 @@ pr2 (precomp-universal-property-set-quotient-trunc-Prop B g) = ```agda abstract - all-elements-equal-image-is-weakly-constant-map : + all-elements-equal-image-is-weakly-constant : {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → - is-weakly-constant-map f → + is-weakly-constant f → all-elements-equal (Σ (type-Set B) (λ b → type-trunc-Prop (fiber f b))) - all-elements-equal-image-is-weakly-constant-map B f H (x , s) (y , t) = + all-elements-equal-image-is-weakly-constant B f H (x , s) (y , t) = eq-type-subtype ( λ b → trunc-Prop (fiber f b)) ( apply-universal-property-trunc-Prop s @@ -76,21 +76,21 @@ abstract ( λ v → inv (pr2 u) ∙ H (pr1 u) (pr1 v) ∙ pr2 v))) abstract - is-prop-image-is-weakly-constant-map : + is-prop-image-is-weakly-constant : {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → - is-weakly-constant-map f → + is-weakly-constant f → is-prop (Σ (type-Set B) (λ b → type-trunc-Prop (fiber f b))) - is-prop-image-is-weakly-constant-map B f H = + is-prop-image-is-weakly-constant B f H = is-prop-all-elements-equal - ( all-elements-equal-image-is-weakly-constant-map B f H) + ( all-elements-equal-image-is-weakly-constant B f H) image-weakly-constant-map-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → - is-weakly-constant-map f → Prop (l1 ⊔ l2) + is-weakly-constant f → Prop (l1 ⊔ l2) pr1 (image-weakly-constant-map-Prop B f H) = Σ (type-Set B) (λ b → type-trunc-Prop (fiber f b)) pr2 (image-weakly-constant-map-Prop B f H) = - is-prop-image-is-weakly-constant-map B f H + is-prop-image-is-weakly-constant B f H ``` ### The universal property @@ -98,7 +98,7 @@ pr2 (image-weakly-constant-map-Prop B f H) = ```agda map-universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → - is-weakly-constant-map f → type-trunc-Prop A → type-Set B + is-weakly-constant f → type-trunc-Prop A → type-Set B map-universal-property-set-quotient-trunc-Prop B f H = ( pr1) ∘ ( map-universal-property-trunc-Prop @@ -107,20 +107,20 @@ map-universal-property-set-quotient-trunc-Prop B f H = map-universal-property-set-quotient-trunc-Prop' : {l1 l2 : Level} {A : UU l1} (B : Set l2) → - Σ (A → type-Set B) is-weakly-constant-map → type-trunc-Prop A → type-Set B + Σ (A → type-Set B) is-weakly-constant → type-trunc-Prop A → type-Set B map-universal-property-set-quotient-trunc-Prop' B (f , H) = map-universal-property-set-quotient-trunc-Prop B f H abstract htpy-universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → - (H : is-weakly-constant-map f) → + (H : is-weakly-constant f) → map-universal-property-set-quotient-trunc-Prop B f H ∘ unit-trunc-Prop ~ f htpy-universal-property-set-quotient-trunc-Prop B f H a = ap ( pr1) ( eq-is-prop' - ( is-prop-image-is-weakly-constant-map B f H) + ( is-prop-image-is-weakly-constant B f H) ( map-universal-property-trunc-Prop ( image-weakly-constant-map-Prop B f H) ( λ x → (f x , unit-trunc-Prop (x , refl))) @@ -133,7 +133,7 @@ abstract ( map-universal-property-set-quotient-trunc-Prop' B)) ~ id is-section-map-universal-property-set-quotient-trunc-Prop B (f , H) = eq-type-subtype - ( is-weakly-constant-map-Prop B) + ( is-weakly-constant-prop-Set B) ( eq-htpy (htpy-universal-property-set-quotient-trunc-Prop B f H)) is-retraction-map-universal-property-set-quotient-trunc-Prop : @@ -151,7 +151,7 @@ abstract ( g x)) ( htpy-universal-property-set-quotient-trunc-Prop B ( g ∘ unit-trunc-Prop) - ( is-weakly-constant-map-precomp-unit-trunc-Prop g))) + ( is-weakly-constant-precomp-unit-trunc-Prop g))) universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) → diff --git a/src/foundation/weakly-constant-maps.lagda.md b/src/foundation/weakly-constant-maps.lagda.md index 6cfa3de953..741e4c32c8 100644 --- a/src/foundation/weakly-constant-maps.lagda.md +++ b/src/foundation/weakly-constant-maps.lagda.md @@ -7,13 +7,18 @@ module foundation.weakly-constant-maps where
Imports ```agda +open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types +open import foundation.fixed-points-endofunctions +open import foundation.identity-types open import foundation.iterated-dependent-product-types open import foundation.universe-levels -open import foundation-core.identity-types +open import foundation-core.contractible-types +open import foundation-core.functoriality-dependent-pair-types open import foundation-core.propositions open import foundation-core.sets +open import foundation-core.torsorial-type-families ```
@@ -21,26 +26,115 @@ open import foundation-core.sets ## Idea A map `f : A → B` is said to be -{{#concept "weakly constant" Agda=is-weakly-constant-map}} if any two elements -in `A` are mapped to identical elements in `B`. +{{#concept "weakly constant" Disambiguation="map of types" Agda=is-weakly-constant}} +if any two elements in `A` are mapped to +[identical elements](foundation-core.identity-types.md) in `B`. -## Definition +## Definitions + +### The structure on a map of being weakly constant ```agda -is-weakly-constant-map : +is-weakly-constant : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) -is-weakly-constant-map {A = A} f = (x y : A) → f x ＝ f y +is-weakly-constant {A = A} f = (x y : A) → f x ＝ f y +``` + +### The type of weakly constant maps + +```agda +weakly-constant-map : {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2) +weakly-constant-map A B = Σ (A → B) (is-weakly-constant) +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : weakly-constant-map A B) + where + + map-weakly-constant-map : A → B + map-weakly-constant-map = pr1 f + + is-weakly-constant-weakly-constant-map : + is-weakly-constant map-weakly-constant-map + is-weakly-constant-weakly-constant-map = pr2 f +``` + +## Properties + +### Being weakly constant is a property if the codomain is a set + +```agda module _ {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) where abstract - is-prop-is-weakly-constant-map-Set : is-prop (is-weakly-constant-map f) - is-prop-is-weakly-constant-map-Set = + is-prop-is-weakly-constant-Set : is-prop (is-weakly-constant f) + is-prop-is-weakly-constant-Set = is-prop-iterated-Π 2 (λ x y → is-set-type-Set B (f x) (f y)) - is-weakly-constant-map-Prop : Prop (l1 ⊔ l2) - pr1 is-weakly-constant-map-Prop = is-weakly-constant-map f - pr2 is-weakly-constant-map-Prop = is-prop-is-weakly-constant-map-Set + is-weakly-constant-prop-Set : Prop (l1 ⊔ l2) + pr1 is-weakly-constant-prop-Set = is-weakly-constant f + pr2 is-weakly-constant-prop-Set = is-prop-is-weakly-constant-Set +``` + +### The action on identifications of a weakly constant map is weakly constant + +This is Auxiliary Lemma 4.3 of {{#cite KECA17}}. + +```agda +module _ + {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : X → Y} + (W : is-weakly-constant f) + where + + compute-ap-is-weakly-constant : + {x y : X} (p : x ＝ y) → inv (W x x) ∙ W x y ＝ ap f p + compute-ap-is-weakly-constant {x} refl = left-inv (W x x) + + is-weakly-constant-ap : {x y : X} → is-weakly-constant (ap f {x} {y}) + is-weakly-constant-ap {x} {y} p q = + ( inv (compute-ap-is-weakly-constant p)) ∙ + ( compute-ap-is-weakly-constant q) + +module _ + {l1 l2 : Level} {X : UU l1} {Y : UU l2} + (f : weakly-constant-map X Y) + where + + ap-weakly-constant-map : + {x y : X} → + weakly-constant-map + ( x ＝ y) + ( map-weakly-constant-map f x ＝ map-weakly-constant-map f y) + ap-weakly-constant-map {x} {y} = + ( ap (map-weakly-constant-map f) {x} {y} , + is-weakly-constant-ap (is-weakly-constant-weakly-constant-map f)) ``` + +### The type of fixed points of a weakly constant endomap is a proposition + +This is Lemma 4.1 of {{#cite KECA17}}. We follow the second proof, due to +Christian Sattler. + +```agda +module _ + {l : Level} {A : UU l} {f : A → A} (W : is-weakly-constant f) + where + + is-proof-irrelevant-fixed-point-is-weakly-constant : + is-proof-irrelevant (fixed-point f) + is-proof-irrelevant-fixed-point-is-weakly-constant (x , p) = + is-contr-equiv + ( Σ A (λ z → f x ＝ z)) + ( equiv-tot (λ z → equiv-concat (W x z) z)) + ( is-torsorial-Id (f x)) + + is-prop-fixed-point-is-weakly-constant : is-prop (fixed-point f) + is-prop-fixed-point-is-weakly-constant = + is-prop-is-proof-irrelevant + ( is-proof-irrelevant-fixed-point-is-weakly-constant) +``` + +## References + +{{#bibliography}} {{#reference KECA17}} diff --git a/src/foundation/whiskering-homotopies-composition.lagda.md b/src/foundation/whiskering-homotopies-composition.lagda.md index 2715167d25..864abbcd6e 100644 --- a/src/foundation/whiskering-homotopies-composition.lagda.md +++ b/src/foundation/whiskering-homotopies-composition.lagda.md @@ -149,7 +149,7 @@ module _ where left-unit-law-left-whisker-comp : - {f f' : (x : A) → B x} → (H : f ~ f') → id ·l H ~ H + {f f' : (x : A) → B x} (H : f ~ f') → id ·l H ~ H left-unit-law-left-whisker-comp H x = ap-id (H x) module _ @@ -175,7 +175,7 @@ module _ where right-unit-law-right-whisker-comp : - {f f' : (x : A) → B x} → (H : f ~ f') → H ·r id ~ H + {f f' : (x : A) → B x} (H : f ~ f') → H ·r id ~ H right-unit-law-right-whisker-comp H = refl-htpy ``` @@ -200,6 +200,37 @@ module _ right-whisker-inv-htpy = refl-htpy ``` +### Inverse laws for whiskered homotopies + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} + {f f' : (x : A) → B x} (g : {x : A} → B x → C x) (H : f ~ f') + where + + left-inv-htpy-left-whisker : g ·l (inv-htpy H) ∙h g ·l H ~ refl-htpy + left-inv-htpy-left-whisker = + ( ap-concat-htpy' (g ·l H) (left-whisker-inv-htpy g H)) ∙h + ( left-inv-htpy (g ·l H)) + + right-inv-htpy-left-whisker : g ·l H ∙h g ·l (inv-htpy H) ~ refl-htpy + right-inv-htpy-left-whisker = + ( ap-concat-htpy (g ·l H) (left-whisker-inv-htpy g H)) ∙h + ( right-inv-htpy (g ·l H)) + +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3} + {g g' : {x : A} (y : B x) → C x y} (H : {x : A} → g {x} ~ g' {x}) + (f : (x : A) → B x) + where + + left-inv-htpy-right-whisker : (inv-htpy H) ·r f ∙h H ·r f ~ refl-htpy + left-inv-htpy-right-whisker = left-inv-htpy (H ·r f) + + right-inv-htpy-right-whisker : H ·r f ∙h (inv-htpy H) ·r f ~ refl-htpy + right-inv-htpy-right-whisker = right-inv-htpy (H ·r f) +``` + ### Distributivity of whiskering over concatenation of homotopies ```agda diff --git a/src/foundation/whiskering-homotopies-concatenation.lagda.md b/src/foundation/whiskering-homotopies-concatenation.lagda.md index dffb6ea28b..ef61dcad5c 100644 --- a/src/foundation/whiskering-homotopies-concatenation.lagda.md +++ b/src/foundation/whiskering-homotopies-concatenation.lagda.md @@ -11,7 +11,6 @@ open import foundation-core.whiskering-homotopies-concatenation public ```agda open import foundation.universe-levels open import foundation.whiskering-identifications-concatenation -open import foundation.whiskering-operations open import foundation-core.equivalences open import foundation-core.functoriality-dependent-function-types diff --git a/src/set-theory/cumulative-hierarchy.lagda.md b/src/set-theory/cumulative-hierarchy.lagda.md index 78520e6978..52ef6232b2 100644 --- a/src/set-theory/cumulative-hierarchy.lagda.md +++ b/src/set-theory/cumulative-hierarchy.lagda.md @@ -775,4 +775,4 @@ needed. ## References -{{#bibliography}} {{#reference UF13}} {{#reference JKFC23}} +{{#bibliography}} {{#reference UF13}} {{#reference dJKFC23}} diff --git a/src/synthetic-homotopy-theory/circle.lagda.md b/src/synthetic-homotopy-theory/circle.lagda.md index c478ba65a6..46751bef2e 100644 --- a/src/synthetic-homotopy-theory/circle.lagda.md +++ b/src/synthetic-homotopy-theory/circle.lagda.md @@ -58,15 +58,13 @@ postulate base-𝕊¹ : 𝕊¹ postulate - loop-𝕊¹ : Id base-𝕊¹ base-𝕊¹ + loop-𝕊¹ : base-𝕊¹ ＝ base-𝕊¹ free-loop-𝕊¹ : free-loop 𝕊¹ -pr1 free-loop-𝕊¹ = base-𝕊¹ -pr2 free-loop-𝕊¹ = loop-𝕊¹ +free-loop-𝕊¹ = base-𝕊¹ , loop-𝕊¹ 𝕊¹-Pointed-Type : Pointed-Type lzero -pr1 𝕊¹-Pointed-Type = 𝕊¹ -pr2 𝕊¹-Pointed-Type = base-𝕊¹ +𝕊¹-Pointed-Type = 𝕊¹ , base-𝕊¹ postulate ind-𝕊¹ : {l : Level} → induction-principle-circle l free-loop-𝕊¹ @@ -95,7 +93,7 @@ uniqueness-dependent-universal-property-𝕊¹ {l} {P} = dependent-universal-property-𝕊¹ module _ - {l : Level} (P : 𝕊¹ → UU l) (p0 : P base-𝕊¹) (α : Id (tr P loop-𝕊¹ p0) p0) + {l : Level} (P : 𝕊¹ → UU l) (p0 : P base-𝕊¹) (α : tr P loop-𝕊¹ p0 ＝ p0) where Π-𝕊¹ : UU l @@ -103,26 +101,25 @@ module _ Σ ( (x : 𝕊¹) → P x) ( λ h → Eq-free-dependent-loop free-loop-𝕊¹ P - ( ev-free-loop-Π free-loop-𝕊¹ P h) (pair p0 α)) + ( ev-free-loop-Π free-loop-𝕊¹ P h) (p0 , α)) apply-dependent-universal-property-𝕊¹ : Π-𝕊¹ apply-dependent-universal-property-𝕊¹ = - center (uniqueness-dependent-universal-property-𝕊¹ (pair p0 α)) + center (uniqueness-dependent-universal-property-𝕊¹ (p0 , α)) function-apply-dependent-universal-property-𝕊¹ : (x : 𝕊¹) → P x function-apply-dependent-universal-property-𝕊¹ = pr1 apply-dependent-universal-property-𝕊¹ base-dependent-universal-property-𝕊¹ : - Id (function-apply-dependent-universal-property-𝕊¹ base-𝕊¹) p0 + function-apply-dependent-universal-property-𝕊¹ base-𝕊¹ ＝ p0 base-dependent-universal-property-𝕊¹ = pr1 (pr2 apply-dependent-universal-property-𝕊¹) loop-dependent-universal-property-𝕊¹ : - Id - ( apd function-apply-dependent-universal-property-𝕊¹ loop-𝕊¹ ∙ - base-dependent-universal-property-𝕊¹) - ( ap (tr P loop-𝕊¹) base-dependent-universal-property-𝕊¹ ∙ α) + ( apd function-apply-dependent-universal-property-𝕊¹ loop-𝕊¹ ∙ + base-dependent-universal-property-𝕊¹) ＝ + ( ap (tr P loop-𝕊¹) base-dependent-universal-property-𝕊¹ ∙ α) loop-dependent-universal-property-𝕊¹ = pr2 (pr2 apply-dependent-universal-property-𝕊¹) ``` @@ -146,32 +143,30 @@ uniqueness-universal-property-𝕊¹ {l} {X} = uniqueness-universal-property-circle free-loop-𝕊¹ universal-property-𝕊¹ X module _ - {l : Level} {X : UU l} (x : X) (α : Id x x) + {l : Level} {X : UU l} (x : X) (α : x ＝ x) where Map-𝕊¹ : UU l Map-𝕊¹ = Σ ( 𝕊¹ → X) - ( λ h → Eq-free-loop (ev-free-loop free-loop-𝕊¹ X h) (pair x α)) + ( λ h → Eq-free-loop (ev-free-loop free-loop-𝕊¹ X h) (x , α)) apply-universal-property-𝕊¹ : Map-𝕊¹ apply-universal-property-𝕊¹ = - center (uniqueness-universal-property-𝕊¹ (pair x α)) + center (uniqueness-universal-property-𝕊¹ (x , α)) map-apply-universal-property-𝕊¹ : 𝕊¹ → X map-apply-universal-property-𝕊¹ = pr1 apply-universal-property-𝕊¹ base-universal-property-𝕊¹ : - Id (map-apply-universal-property-𝕊¹ base-𝕊¹) x + map-apply-universal-property-𝕊¹ base-𝕊¹ ＝ x base-universal-property-𝕊¹ = pr1 (pr2 apply-universal-property-𝕊¹) loop-universal-property-𝕊¹ : - Id - ( ap map-apply-universal-property-𝕊¹ loop-𝕊¹ ∙ - base-universal-property-𝕊¹) - ( base-universal-property-𝕊¹ ∙ α) + ap map-apply-universal-property-𝕊¹ loop-𝕊¹ ∙ base-universal-property-𝕊¹ ＝ + base-universal-property-𝕊¹ ∙ α loop-universal-property-𝕊¹ = pr2 (pr2 apply-universal-property-𝕊¹) ``` @@ -219,7 +214,7 @@ loop at `N`. The choice of which meridian to start with is arbitrary, but informs the rest of the construction hereafter. ```agda -north-sphere-1-loop : Id (north-sphere 1) (north-sphere 1) +north-sphere-1-loop : north-sphere 1 ＝ north-sphere 1 north-sphere-1-loop = ( meridian-sphere 0 (zero-Fin 1)) ∙ ( inv (meridian-sphere 0 (one-Fin 1))) @@ -229,12 +224,12 @@ sphere-1-circle = map-apply-universal-property-𝕊¹ (north-sphere 1) north-sphere-1-loop sphere-1-circle-base-𝕊¹-eq-north-sphere-1 : - Id (sphere-1-circle base-𝕊¹) (north-sphere 1) + sphere-1-circle base-𝕊¹ ＝ north-sphere 1 sphere-1-circle-base-𝕊¹-eq-north-sphere-1 = base-universal-property-𝕊¹ (north-sphere 1) north-sphere-1-loop sphere-1-circle-base-𝕊¹-eq-south-sphere-1 : - Id (sphere-1-circle base-𝕊¹) (south-sphere 1) + sphere-1-circle base-𝕊¹ ＝ south-sphere 1 sphere-1-circle-base-𝕊¹-eq-south-sphere-1 = ( sphere-1-circle-base-𝕊¹-eq-north-sphere-1) ∙ ( meridian-sphere 0 (one-Fin 1)) @@ -270,7 +265,7 @@ circle-sphere-1-north-sphere-1-eq-base-𝕊¹ = ( suspension-structure-sphere-0-𝕊¹) circle-sphere-1-south-sphere-1-eq-base-𝕊¹ : - Id (circle-sphere-1 (south-sphere 1)) base-𝕊¹ + circle-sphere-1 (south-sphere 1) ＝ base-𝕊¹ circle-sphere-1-south-sphere-1-eq-base-𝕊¹ = compute-south-cogap-suspension ( suspension-structure-sphere-0-𝕊¹) @@ -438,7 +433,7 @@ mapped to `w⁻¹∙ e` and then back to `refl⁻¹ ∙ loop = loop`. ```agda circle-sphere-1-circle-base-𝕊¹ : - Id (circle-sphere-1 (sphere-1-circle base-𝕊¹)) base-𝕊¹ + circle-sphere-1 (sphere-1-circle base-𝕊¹) ＝ base-𝕊¹ circle-sphere-1-circle-base-𝕊¹ = ( ap circle-sphere-1 sphere-1-circle-base-𝕊¹-eq-north-sphere-1) ∙ ( circle-sphere-1-north-sphere-1-eq-base-𝕊¹)