From ae245028ba1c906a9dea04836fe8ee0863c8d6fc Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Sat, 23 Mar 2024 23:44:05 +0100 Subject: [PATCH] Deloopings and Eilenberg-Mac Lane spaces (#1079) In this pull request we add: - A definition of what it means for a pointed type to be deloopable - A definition of what it means for an H-space to be deloopable - A definition of Eilenberg-Mac Lane spaces There were some universe level questions that one can ask about the type of deloopings. One can show that the type of deloopings of `X` in universe `l2` is equivalent to the type of deloopings of `X` in the universe level of `X`. Showing the forward implication required me to do some work on smallness of pointed types and higher groups, which is included in this pull request. Furthermore, the file about morphisms of H-spaces has been revamped, for better formalization of the preservation of the coherence law. This was needed for the notion of equivalence of H-spaces, which was prerequisite to the notion of delooping of H-spaces. --- src/foundation-core/small-types.lagda.md | 7 + src/group-theory/groups.lagda.md | 13 + .../wild-representations-monoids.lagda.md | 2 +- src/higher-group-theory.lagda.md | 6 + .../deloopable-groups.lagda.md | 58 +++ .../deloopable-h-spaces.lagda.md | 68 +++ .../deloopable-types.lagda.md | 227 +++++++++ .../eilenberg-mac-lane-spaces.lagda.md | 139 ++++++ .../equivalences-higher-groups.lagda.md | 24 +- .../higher-groups.lagda.md | 82 +++- ...rated-deloopings-of-pointed-types.lagda.md | 64 +++ .../small-higher-groups.lagda.md | 308 ++++++++++++ ...ersal-property-lists-wild-monoids.lagda.md | 58 +-- src/structured-types.lagda.md | 2 + .../equivalences-h-spaces.lagda.md | 243 ++++++++++ src/structured-types/h-spaces.lagda.md | 16 + .../morphisms-h-spaces.lagda.md | 438 +++++++++++------- .../morphisms-wild-monoids.lagda.md | 36 +- .../pointed-equivalences.lagda.md | 155 +++++-- .../small-pointed-types.lagda.md | 156 +++++++ .../iterated-loop-spaces.lagda.md | 18 + .../loop-spaces.lagda.md | 12 +- 22 files changed, 1846 insertions(+), 286 deletions(-) create mode 100644 src/higher-group-theory/deloopable-groups.lagda.md create mode 100644 src/higher-group-theory/deloopable-h-spaces.lagda.md create mode 100644 src/higher-group-theory/deloopable-types.lagda.md create mode 100644 src/higher-group-theory/eilenberg-mac-lane-spaces.lagda.md create mode 100644 src/higher-group-theory/iterated-deloopings-of-pointed-types.lagda.md create mode 100644 src/higher-group-theory/small-higher-groups.lagda.md create mode 100644 src/structured-types/equivalences-h-spaces.lagda.md create mode 100644 src/structured-types/small-pointed-types.lagda.md diff --git a/src/foundation-core/small-types.lagda.md b/src/foundation-core/small-types.lagda.md index 107cf0fc1f..dd0762ef81 100644 --- a/src/foundation-core/small-types.lagda.md +++ b/src/foundation-core/small-types.lagda.md @@ -195,6 +195,13 @@ pr1 (is-small-is-contr l H) = raise-unit l pr2 (is-small-is-contr l H) = equiv-is-contr H is-contr-raise-unit ``` +### The unit type is small with respect to any universe + +```agda +is-small-unit : {l : Level} → is-small l unit +is-small-unit = is-small-is-contr _ is-contr-unit +``` + ### Small types are closed under dependent pair types ```agda diff --git a/src/group-theory/groups.lagda.md b/src/group-theory/groups.lagda.md index 3aa3bee992..12677cf0cf 100644 --- a/src/group-theory/groups.lagda.md +++ b/src/group-theory/groups.lagda.md @@ -34,6 +34,7 @@ open import group-theory.semigroups open import lists.concatenation-lists open import lists.lists +open import structured-types.h-spaces open import structured-types.pointed-types open import structured-types.pointed-types-equipped-with-automorphisms ``` @@ -158,10 +159,22 @@ module _ (x : type-Group) → Id (mul-Group x unit-Group) x right-unit-law-mul-Group = pr2 (pr2 is-unital-Group) + coherence-unit-laws-mul-Group : + left-unit-law-mul-Group unit-Group ＝ right-unit-law-mul-Group unit-Group + coherence-unit-laws-mul-Group = + eq-is-prop (is-set-type-Group _ _) + pointed-type-Group : Pointed-Type l pr1 pointed-type-Group = type-Group pr2 pointed-type-Group = unit-Group + h-space-Group : H-Space l + pr1 h-space-Group = pointed-type-Group + pr1 (pr2 h-space-Group) = mul-Group + pr1 (pr2 (pr2 h-space-Group)) = left-unit-law-mul-Group + pr1 (pr2 (pr2 (pr2 h-space-Group))) = right-unit-law-mul-Group + pr2 (pr2 (pr2 (pr2 h-space-Group))) = coherence-unit-laws-mul-Group + has-inverses-Group : is-group-is-unital-Semigroup semigroup-Group is-unital-Group has-inverses-Group = pr2 is-group-Group diff --git a/src/group-theory/wild-representations-monoids.lagda.md b/src/group-theory/wild-representations-monoids.lagda.md index 0e219abd51..153d5c80a5 100644 --- a/src/group-theory/wild-representations-monoids.lagda.md +++ b/src/group-theory/wild-representations-monoids.lagda.md @@ -69,7 +69,7 @@ module _ ( ( action-wild-representation-type-Monoid x) ∘ ( action-wild-representation-type-Monoid y)) preserves-mul-action-wild-representation-type-Monoid = - preserves-mul-map-hom-Wild-Monoid + preserves-mul-hom-Wild-Monoid ( wild-monoid-Monoid M) ( endo-Wild-Monoid type-wild-representation-type-Monoid) ( hom-action-wild-representation-type-Monoid) diff --git a/src/higher-group-theory.lagda.md b/src/higher-group-theory.lagda.md index e12c0a71f1..13e68733d8 100644 --- a/src/higher-group-theory.lagda.md +++ b/src/higher-group-theory.lagda.md @@ -8,6 +8,10 @@ module higher-group-theory where open import higher-group-theory.cartesian-products-higher-groups public open import higher-group-theory.conjugation public open import higher-group-theory.cyclic-higher-groups public +open import higher-group-theory.deloopable-groups public +open import higher-group-theory.deloopable-h-spaces public +open import higher-group-theory.deloopable-types public +open import higher-group-theory.eilenberg-mac-lane-spaces public open import higher-group-theory.equivalences-higher-groups public open import higher-group-theory.fixed-points-higher-group-actions public open import higher-group-theory.free-higher-group-actions public @@ -17,7 +21,9 @@ open import higher-group-theory.homomorphisms-higher-group-actions public open import higher-group-theory.homomorphisms-higher-groups public open import higher-group-theory.integers-higher-group public open import higher-group-theory.iterated-cartesian-products-higher-groups public +open import higher-group-theory.iterated-deloopings-of-pointed-types public open import higher-group-theory.orbits-higher-group-actions public +open import higher-group-theory.small-higher-groups public open import higher-group-theory.subgroups-higher-groups public open import higher-group-theory.symmetric-higher-groups public open import higher-group-theory.transitive-higher-group-actions public diff --git a/src/higher-group-theory/deloopable-groups.lagda.md b/src/higher-group-theory/deloopable-groups.lagda.md new file mode 100644 index 0000000000..45c31edf78 --- /dev/null +++ b/src/higher-group-theory/deloopable-groups.lagda.md @@ -0,0 +1,58 @@ +# Deloopable groups + +```agda +module higher-group-theory.deloopable-groups where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import group-theory.groups + +open import higher-group-theory.deloopable-h-spaces +``` + +
+ +## Idea + +A {{#concept "delooping" Disambiguation="group" Agda=delooping-Group}} of a +[group](group-theory.groups.md) `G` is a +[delooping](higher-group-theory.deloopable-h-spaces.md) of the underlying +[H-space](structured-types.h-spaces.md) of `G`. In other words, a delooping of a +group `G` consists of a [higher group](higher-group-theory.higher-groups.md) +`H`, which is defined to be a [pointed](structured-types.pointed-types.md) +[connected](foundation.0-connected-types.md) type, equipped with an +[equivalence of H-spaces](structured-types.equivalences-h-spaces.md) +`G ≃ h-space-∞-Group H` from `G` to the underlying H-space of `H`. + +## Definitions + +### Deloopings of groups of a given universe level + +```agda +module _ + {l1 : Level} (l2 : Level) (G : Group l1) + where + + delooping-Group-Level : UU (l1 ⊔ lsuc l2) + delooping-Group-Level = delooping-H-Space-Level l2 (h-space-Group G) +``` + +### Deloopings of groups + +```agda +module _ + {l1 : Level} (G : Group l1) + where + + delooping-Group : UU (lsuc l1) + delooping-Group = delooping-Group-Level l1 G +``` + +## See also + +- [Eilenberg-Mac Lane spaces](higher-group-theory.eilenberg-mac-lane-spaces.md) diff --git a/src/higher-group-theory/deloopable-h-spaces.lagda.md b/src/higher-group-theory/deloopable-h-spaces.lagda.md new file mode 100644 index 0000000000..90b0d90e0c --- /dev/null +++ b/src/higher-group-theory/deloopable-h-spaces.lagda.md @@ -0,0 +1,68 @@ +# Deloopable H-spaces + +```agda +module higher-group-theory.deloopable-h-spaces where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import higher-group-theory.higher-groups + +open import structured-types.equivalences-h-spaces +open import structured-types.h-spaces +``` + +
+ +## Idea + +Consider an [H-space](structured-types.h-spaces.md) with underlying +[pointed type](structured-types.pointed-types.md) `(X , *)` and with +multiplication `μ` satisfying + +```text + left-unit-law : (x : X) → μ * x ＝ x + right-unit-law : (x : X) → μ x * ＝ x + coh-unit-law : left-unit-law * ＝ right-unit-law *. +``` + +A {{#concept "delooping" Disambiguation="H-space" Agda=delooping-H-Space}} of +the H-space `X` consists of an [∞-group](higher-group-theory.higher-groups.md) +`G` and an [equivalence of H-spaces](structured-types.equivalences-h-spaces.md) + +```text + X ≃ h-space-∞-Group G. +``` + +## Definitions + +### Deloopings of H-spaces of a given universe level + +```agda +module _ + {l1 : Level} (l2 : Level) (A : H-Space l1) + where + + delooping-H-Space-Level : UU (l1 ⊔ lsuc l2) + delooping-H-Space-Level = + Σ (∞-Group l2) (λ G → equiv-H-Space A (h-space-∞-Group G)) +``` + +### Deloopings of H-spaces + +```agda +module _ + {l1 : Level} (A : H-Space l1) + where + + delooping-H-Space : UU (lsuc l1) + delooping-H-Space = delooping-H-Space-Level l1 A +``` + +## See also + +- [Deloopable groups](higher-group-theory.deloopable-groups.md) diff --git a/src/higher-group-theory/deloopable-types.lagda.md b/src/higher-group-theory/deloopable-types.lagda.md new file mode 100644 index 0000000000..23e7bac773 --- /dev/null +++ b/src/higher-group-theory/deloopable-types.lagda.md @@ -0,0 +1,227 @@ +# Deloopable types + +```agda +module higher-group-theory.deloopable-types where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.small-types +open import foundation.universe-levels + +open import higher-group-theory.equivalences-higher-groups +open import higher-group-theory.higher-groups +open import higher-group-theory.small-higher-groups + +open import structured-types.pointed-equivalences +open import structured-types.pointed-types +open import structured-types.small-pointed-types +``` + +
+ +## Idea + +Consider a [pointed type](structured-types.pointed-types.md) `X` and a pointed +[connected](foundation.0-connected-types.md) type `Y`. We say that `Y` is a +{{#concept "delooping" Disambiguation="pointed type" Agda=is-delooping}} of `X` +if we have a [pointed equivalence](structured-types.pointed-equivalences.md) + +```text + X ≃∗ Ω Y. +``` + +Recall that a pointed connected type is an +[∞-group](higher-group-theory.higher-groups.md). An ∞-group `G` is therefore a +delooping of `X` if its underlying pointed type is pointed equivalent to `X`. A +{{#concept "delooping" Disambiguation="pointed type" Agda=delooping}} of `X` +therefore consist of an ∞-group `G` and a pointed equivalence + +```text + X ≃∗ type-∞-Group G +``` + +In other words, the type of deloopings of `X` is defined to be + +```text + delooping X := Σ (Y : ∞-Group), X ≃∗ Ω Y. +``` + +### Relation to higher group structures + +A delooping of a pointed type `X` is, in quite a literal way, an +{{#concept "∞-group structure" Agda=delooping}} on `X`. In other words, the type +`delooping X` is the type of ∞-group structures on `X`. Indeed, the type of all +pointed types equipped with deloopings is +[equivalent](foundation-core.equivalences.md) to the type of ∞-groups, by +extensionality of the type of pointed types. + +Being deloopable is therefore a [structure](foundation.structure.md), and +usually not a [property](foundation-core.propositions.md). If there are multiple +distinct ways to equip a pointed type `X` with the structure of an ∞-group, or +even with the structure of a [group](group-theory.groups.md), then the type of +deloopings of `X` will not be a proposition. For instance, the +[standard `4`-element type](univalent-combinatorics.standard-finite-types.md) +`Fin 4` is deloopable in multiple distinct ways, by equipping it with the +[cyclic group structure](group-theory.cyclic-groups.md) of `ℤ₄` or by equipping +it with the group structure of `ℤ₂ × ℤ₂`. + +### Universe levels in the definition of being deloopable + +Note that there is a small question about universe levels in the definition of +being a deloopable type. We say that a type is deloopable in a universe `𝒰` if +there is an ∞-group `Y` in the universe `𝒰` that is a delooping of `X`. However, +by the [type theoretic replacement principle](foundation.replacement.md) it +follows that any delooping of `X` is always [small](foundation.small-types.md) +with respect to the universe of `X` itself. Therefore we simply say that `X` is +deloopable, i.e., without reference to any universes, if `X` is deloopable in +its own universe. + +## Definitions + +### The predicate of being a delooping + +```agda +module _ + {l1 l2 : Level} (X : Pointed-Type l1) + where + + is-delooping : (G : ∞-Group l2) → UU (l1 ⊔ l2) + is-delooping G = X ≃∗ pointed-type-∞-Group G +``` + +### The type of deloopings of a pointed type, in a given universe + +```agda +module _ + {l1 : Level} (X : Pointed-Type l1) + where + + delooping-Level : (l : Level) → UU (l1 ⊔ lsuc l) + delooping-Level l = Σ (∞-Group l) (is-delooping X) + + module _ + {l : Level} (Y : delooping-Level l) + where + + ∞-group-delooping-Level : ∞-Group l + ∞-group-delooping-Level = pr1 Y + + classifying-pointed-type-∞-group-delooping-Level : Pointed-Type l + classifying-pointed-type-∞-group-delooping-Level = + classifying-pointed-type-∞-Group ∞-group-delooping-Level + + classifying-type-∞-group-delooping-Level : UU l + classifying-type-∞-group-delooping-Level = + classifying-type-∞-Group ∞-group-delooping-Level + + is-delooping-delooping-Level : is-delooping X ∞-group-delooping-Level + is-delooping-delooping-Level = pr2 Y + + equiv-is-delooping-delooping-Level : + type-Pointed-Type X ≃ type-∞-Group ∞-group-delooping-Level + equiv-is-delooping-delooping-Level = + equiv-pointed-equiv is-delooping-delooping-Level +``` + +### The type of deloopings of a pointed type + +```agda +module _ + {l1 : Level} (X : Pointed-Type l1) + where + + delooping : UU (lsuc l1) + delooping = delooping-Level X l1 +``` + +## Properties + +### The delooping of a pointed type in a universe `𝒰` is a `𝒰`-small ∞-group + +```agda +module _ + {l1 l2 : Level} (X : Pointed-Type l1) (H : delooping-Level X l2) + where + + abstract + is-small-∞-group-delooping-Level : + is-small-∞-Group l1 (∞-group-delooping-Level X H) + pr1 is-small-∞-group-delooping-Level = type-Pointed-Type X + pr2 is-small-∞-group-delooping-Level = + inv-equiv (equiv-is-delooping-delooping-Level X H) + + abstract + is-small-classifying-type-∞-group-delooping-Level : + is-small l1 (classifying-type-∞-group-delooping-Level X H) + is-small-classifying-type-∞-group-delooping-Level = + is-small-classifying-type-is-small-∞-Group + ( ∞-group-delooping-Level X H) + ( is-small-∞-group-delooping-Level) + + abstract + is-pointed-small-classifying-pointed-type-∞-group-delooping-Level : + is-pointed-small-Pointed-Type l1 + ( classifying-pointed-type-∞-group-delooping-Level X H) + is-pointed-small-classifying-pointed-type-∞-group-delooping-Level = + is-pointed-small-is-small-Pointed-Type + ( classifying-pointed-type-∞-group-delooping-Level X H) + ( is-small-classifying-type-∞-group-delooping-Level) +``` + +### If a pointed type in universe `𝒰 l1` is deloopable in any universe, then it is deloopable in `𝒰 l1` + +Suppose `X` is a pointed type of universe level `l1`, which is deloopable in +universe level `l2`. Then there is an ∞-group `H` of universe level `l2` +equipped with a pointed equivalence + +```text + X ≃∗ type-∞-Group H. +``` + +This implies that the ∞-group `H` is `l1`-small, because its underlying type is +equivalent to the underlying type of `X`. Hence there is an ∞-group `K` equipped +with an +[equivalence of ∞-groups](higher-group-theory.equivalences-higher-groups.md) + +```text + H ≃ K. +``` + +```agda +module _ + {l1 l2 : Level} (X : Pointed-Type l1) (H : delooping-Level X l2) + where + + ∞-group-delooping-delooping-level : ∞-Group l1 + ∞-group-delooping-delooping-level = + ∞-group-is-small-∞-Group + ( ∞-group-delooping-Level X H) + ( type-Pointed-Type X , + equiv-inv-pointed-equiv (is-delooping-delooping-Level X H)) + + is-delooping-delooping-delooping-Level : + is-delooping X ∞-group-delooping-delooping-level + is-delooping-delooping-delooping-Level = + comp-pointed-equiv + ( pointed-equiv-equiv-∞-Group + ( ∞-group-delooping-Level X H) + ( ∞-group-delooping-delooping-level) + ( equiv-∞-group-is-small-∞-Group + ( ∞-group-delooping-Level X H) + ( type-Pointed-Type X , + equiv-inv-pointed-equiv (is-delooping-delooping-Level X H)))) + ( is-delooping-delooping-Level X H) + + delooping-delooping-Level : delooping X + pr1 delooping-delooping-Level = ∞-group-delooping-delooping-level + pr2 delooping-delooping-Level = is-delooping-delooping-delooping-Level +``` + +## See also + +- [Deloopable H-spaces](higher-group-theory.deloopable-h-spaces.md) +- [Deloopable groups](higher-group-theory.deloopable-groups.md) diff --git a/src/higher-group-theory/eilenberg-mac-lane-spaces.lagda.md b/src/higher-group-theory/eilenberg-mac-lane-spaces.lagda.md new file mode 100644 index 0000000000..13a8cf9fab --- /dev/null +++ b/src/higher-group-theory/eilenberg-mac-lane-spaces.lagda.md @@ -0,0 +1,139 @@ +# Eilenberg-Mac Lane spaces + +```agda +module higher-group-theory.eilenberg-mac-lane-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.0-connected-types +open import foundation.cartesian-product-types +open import foundation.connected-types +open import foundation.truncated-types +open import foundation.truncation-levels +open import foundation.universe-levels + +open import group-theory.abelian-groups +open import group-theory.groups + +open import structured-types.equivalences-h-spaces +open import structured-types.pointed-equivalences +open import structured-types.pointed-types + +open import synthetic-homotopy-theory.iterated-loop-spaces +open import synthetic-homotopy-theory.loop-spaces +``` + +
+ +## Idea + +There are many ways to say what an _Eilenberg-Mac Lane space_ is. The basic idea +is that a [pointed](structured-types.pointed-types.md) +[connected](foundation.0-connected-types.md) type `X` is an Eilenberg-Mac Lane +space if only one of its homotopy groups `π n X` is +[nontrivial](group-theory.nontrivial-groups.md). However, recall that the +condition of being [`n`-truncated](foundation-core.truncated-types.md) is +slightly stronger than the condition that the homotopy groups `π i X` are +[trivial](group-theory.trivial-groups.md) for all `i > n`. Indeed, unlike in the +setting of topological spaces or simplicial sets, univalent type theory allows +for the possibility of ∞-connected types, i.e., types of which all homotopy +groups are trivial. In order to avoid examples of Eilenberg-Mac Lane spaces +possibly involving nontrivial ∞-connected types, we will slightly strengthen the +definition of Eilenberg-Mac Lane spaces. We say that a pointed type `X`is an +{{#concept "Eilenberg-Mac Lane space"}} if`X`is`n-1`-connected and +`n`-truncated. Under this definition there is an +[equivalence](category-theory.equivalences-of-categories.md) between the +[category of groups](group-theory.category-of-groups.md), resp. the +[category of abelian groups](group-theory.category-of-abelian-groups.md), and +the category of Eilenberg-Mac Lane spaces of dimension `1`, resp. `n ≥ 2`. + +Consider a [group](group-theory.groups.md) `G` and a +[natural number](elementary-number-theory.natural-numbers.md) `n ≥ 1`. A pointed +type `X` is said to be an Eilenberg-Mac Lane space of type `K G n` if `X` is +[`(n-1)`-connected](foundation.connected-types.md) and +[`n`-truncated](foundation-core.truncated-types.md), and moreover the `n`-th +homotopy group `π n X` is [isomorphic](group-theory.isomorphisms-groups.md) to +`G`. + +There is also a recursive definition of what it means for a pointed type `X` to +be an $n$-th +{{#concept "Eilenberg-Mac Lane space" Agda=is-eilenberg-mac-lane-space-Group}}: + +- We say that `X` is a **first Eilenberg-Mac Lane space** if `X` is + `0`-connected and there is a + [pointed equivalence](structured-types.pointed-equivalences.md) + + ```text + Ω X ≃ G + ``` + + that maps concatenation in the + [loop space](synthetic-homotopy-theory.loop-spaces.md) `Ω X` to the group + operation on `G`. + +- We say that `X` is an `(n+1)`-st Eilenberg-Mac Lane space if `X` is + `0`-connected and `Ω X` is an `n`-th Eilenberg-Mac Lane space. + +## Definitions + +### Eilenberg-Mac Lane spaces + +We introduce the most general notion of an (unspecified) Eilenberg-Mac Lane +space to be a pointed `n`-connected `(n+1)`-truncated type. Eilenberg-Mac Lane +spaces in this definition aren't equipped with a group isomorphism from their +nontrivial homotopy group to a given group `G`, so in this sense they are +"unspecified". + +```agda +module _ + {l1 : Level} (k : 𝕋) (X : Pointed-Type l1) + where + + is-eilenberg-mac-lane-space-𝕋 : UU l1 + is-eilenberg-mac-lane-space-𝕋 = + is-connected k (type-Pointed-Type X) × + is-trunc (succ-𝕋 k) (type-Pointed-Type X) + +module _ + {l1 : Level} (n : ℕ) (X : Pointed-Type l1) + where + + is-eilenberg-mac-lane-space : UU l1 + is-eilenberg-mac-lane-space = + is-eilenberg-mac-lane-space-𝕋 + ( truncation-level-minus-one-ℕ n) + ( X) +``` + +### Eilenberg-Mac Lane spaces specified by groups + +```agda +module _ + {l1 l2 : Level} (G : Group l1) + where + + is-eilenberg-mac-lane-space-Group : + (n : ℕ) (X : Pointed-Type l2) → UU (l1 ⊔ l2) + is-eilenberg-mac-lane-space-Group 0 X = + pointed-type-Group G ≃∗ X + is-eilenberg-mac-lane-space-Group (succ-ℕ n) X = + is-connected (truncation-level-ℕ n) (type-Pointed-Type X) × + equiv-H-Space (h-space-Group G) (Ω-H-Space (iterated-loop-space n X)) +``` + +### Eilenberg-Mac Lane spaces specified by abelian groups + +```agda +module _ + {l1 l2 : Level} (A : Ab l1) + where + + is-eilenberg-mac-lane-space-Ab : + (n : ℕ) (X : Pointed-Type l2) → UU (l1 ⊔ l2) + is-eilenberg-mac-lane-space-Ab = + is-eilenberg-mac-lane-space-Group (group-Ab A) +``` diff --git a/src/higher-group-theory/equivalences-higher-groups.lagda.md b/src/higher-group-theory/equivalences-higher-groups.lagda.md index bc8cbe7ebe..c494c345cf 100644 --- a/src/higher-group-theory/equivalences-higher-groups.lagda.md +++ b/src/higher-group-theory/equivalences-higher-groups.lagda.md @@ -23,6 +23,8 @@ open import higher-group-theory.homomorphisms-higher-groups open import structured-types.pointed-equivalences open import structured-types.pointed-isomorphisms open import structured-types.pointed-types + +open import synthetic-homotopy-theory.functoriality-loop-spaces ``` @@ -40,12 +42,22 @@ module _ equiv-∞-Group = classifying-pointed-type-∞-Group G ≃∗ classifying-pointed-type-∞-Group H - hom-equiv-∞-Group : equiv-∞-Group → hom-∞-Group G H - hom-equiv-∞-Group = - pointed-map-pointed-equiv + module _ + (e : equiv-∞-Group) + where + + hom-equiv-∞-Group : hom-∞-Group G H + hom-equiv-∞-Group = pointed-map-pointed-equiv e + + map-equiv-∞-Group : type-∞-Group G → type-∞-Group H + map-equiv-∞-Group = map-hom-∞-Group G H hom-equiv-∞-Group + + pointed-equiv-equiv-∞-Group : + pointed-type-∞-Group G ≃∗ pointed-type-∞-Group H + pointed-equiv-equiv-∞-Group = pointed-equiv-Ω-pointed-equiv e - map-equiv-∞-Group : equiv-∞-Group → type-∞-Group G → type-∞-Group H - map-equiv-∞-Group = map-hom-∞-Group G H ∘ hom-equiv-∞-Group + equiv-equiv-∞-Group : type-∞-Group G ≃ type-∞-Group H + equiv-equiv-∞-Group = equiv-map-Ω-pointed-equiv e ``` ### The identity equivalence of higher groups @@ -77,7 +89,7 @@ is-torsorial-equiv-∞-Group : is-torsorial (λ (H : ∞-Group l1) → equiv-∞-Group G H) is-torsorial-equiv-∞-Group G = is-torsorial-Eq-subtype - ( is-torsorial-equiv-Pointed-Type (classifying-pointed-type-∞-Group G)) + ( is-torsorial-pointed-equiv (classifying-pointed-type-∞-Group G)) ( λ X → is-prop-is-0-connected (type-Pointed-Type X)) ( classifying-pointed-type-∞-Group G) ( id-pointed-equiv) diff --git a/src/higher-group-theory/higher-groups.lagda.md b/src/higher-group-theory/higher-groups.lagda.md index 96c9bca098..6102d85536 100644 --- a/src/higher-group-theory/higher-groups.lagda.md +++ b/src/higher-group-theory/higher-groups.lagda.md @@ -9,11 +9,17 @@ module higher-group-theory.higher-groups where ```agda open import foundation.0-connected-types open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.full-subtypes open import foundation.identity-types +open import foundation.images open import foundation.mere-equality +open import foundation.propositional-truncations open import foundation.propositions +open import foundation.unit-type open import foundation.universe-levels +open import structured-types.h-spaces open import structured-types.pointed-types open import synthetic-homotopy-theory.loop-spaces @@ -49,30 +55,58 @@ module _ shape-∞-Group = point-Pointed-Type classifying-pointed-type-∞-Group - is-0-connected-classifying-type-∞-Group : - is-0-connected classifying-type-∞-Group - is-0-connected-classifying-type-∞-Group = pr2 G - - mere-eq-classifying-type-∞-Group : - (X Y : classifying-type-∞-Group) → mere-eq X Y - mere-eq-classifying-type-∞-Group = - mere-eq-is-0-connected - is-0-connected-classifying-type-∞-Group - - elim-prop-classifying-type-∞-Group : - {l2 : Level} (P : classifying-type-∞-Group → Prop l2) → - type-Prop (P shape-∞-Group) → - ((X : classifying-type-∞-Group) → type-Prop (P X)) - elim-prop-classifying-type-∞-Group = - apply-dependent-universal-property-is-0-connected - shape-∞-Group - is-0-connected-classifying-type-∞-Group + point-∞-Group : unit → classifying-type-∞-Group + point-∞-Group = point shape-∞-Group + + abstract + is-0-connected-classifying-type-∞-Group : + is-0-connected classifying-type-∞-Group + is-0-connected-classifying-type-∞-Group = pr2 G + + abstract + mere-eq-classifying-type-∞-Group : + (X Y : classifying-type-∞-Group) → mere-eq X Y + mere-eq-classifying-type-∞-Group = + mere-eq-is-0-connected + is-0-connected-classifying-type-∞-Group + + abstract + is-full-subtype-im-point-∞-Group : + is-full-subtype (subtype-im point-∞-Group) + is-full-subtype-im-point-∞-Group x = + apply-universal-property-trunc-Prop + ( mere-eq-classifying-type-∞-Group shape-∞-Group x) + ( subtype-im point-∞-Group x) + ( λ where refl → unit-trunc-Prop (star , refl)) + + compute-im-point-∞-Group : + im point-∞-Group ≃ classifying-type-∞-Group + compute-im-point-∞-Group = + equiv-inclusion-is-full-subtype + ( subtype-im point-∞-Group) + ( is-full-subtype-im-point-∞-Group) + + abstract + elim-prop-classifying-type-∞-Group : + {l2 : Level} (P : classifying-type-∞-Group → Prop l2) → + type-Prop (P shape-∞-Group) → + ((X : classifying-type-∞-Group) → type-Prop (P X)) + elim-prop-classifying-type-∞-Group = + apply-dependent-universal-property-is-0-connected + shape-∞-Group + is-0-connected-classifying-type-∞-Group + + h-space-∞-Group : H-Space l + h-space-∞-Group = Ω-H-Space classifying-pointed-type-∞-Group + + pointed-type-∞-Group : Pointed-Type l + pointed-type-∞-Group = Ω classifying-pointed-type-∞-Group type-∞-Group : UU l - type-∞-Group = type-Ω classifying-pointed-type-∞-Group + type-∞-Group = type-Pointed-Type pointed-type-∞-Group unit-∞-Group : type-∞-Group - unit-∞-Group = refl-Ω classifying-pointed-type-∞-Group + unit-∞-Group = point-Pointed-Type pointed-type-∞-Group mul-∞-Group : (x y : type-∞-Group) → type-∞-Group mul-∞-Group = mul-Ω classifying-pointed-type-∞-Group @@ -95,10 +129,10 @@ module _ right-unit-law-mul-Ω classifying-pointed-type-∞-Group coherence-unit-laws-mul-∞-Group : - Id - ( left-unit-law-mul-∞-Group unit-∞-Group) - ( right-unit-law-mul-∞-Group unit-∞-Group) - coherence-unit-laws-mul-∞-Group = refl + left-unit-law-mul-∞-Group unit-∞-Group ＝ + right-unit-law-mul-∞-Group unit-∞-Group + coherence-unit-laws-mul-∞-Group = + coherence-unit-laws-mul-Ω classifying-pointed-type-∞-Group inv-∞-Group : type-∞-Group → type-∞-Group inv-∞-Group = inv-Ω classifying-pointed-type-∞-Group diff --git a/src/higher-group-theory/iterated-deloopings-of-pointed-types.lagda.md b/src/higher-group-theory/iterated-deloopings-of-pointed-types.lagda.md new file mode 100644 index 0000000000..d5f051b7fd --- /dev/null +++ b/src/higher-group-theory/iterated-deloopings-of-pointed-types.lagda.md @@ -0,0 +1,64 @@ +# Iterated deloopings of pointed types + +```agda +module higher-group-theory.iterated-deloopings-of-pointed-types where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.cartesian-product-types +open import foundation.connected-types +open import foundation.dependent-pair-types +open import foundation.truncation-levels +open import foundation.universe-levels + +open import structured-types.pointed-equivalences +open import structured-types.pointed-types + +open import synthetic-homotopy-theory.iterated-loop-spaces +``` + +
+ +## Idea + +The type of {{#concept "`n`-fold deloopings" Disambiguation="pointed type"}} of +a [pointed type](structured-types.pointed-types.md) `X` is the type + +```text + Σ (Y : Pointed-Type), is-connected (n-1) Y × (Ωⁿ X ≃∗ Y). +``` + +Here, the pointed type `Ωⁿ X` is the `n`-th +[iterated loop space](synthetic-homotopy-theory.iterated-loop-spaces.md) of `X`. + +## Definitions + +### The type of `n`-fold deloopings of a pointed type, with respect to a universe level + +```agda +module _ + {l1 : Level} (l2 : Level) (n : ℕ) (X : Pointed-Type l1) + where + + iterated-delooping-Level : UU (l1 ⊔ lsuc l2) + iterated-delooping-Level = + Σ ( Pointed-Type l2) + ( λ Y → + ( is-connected (truncation-level-minus-one-ℕ n) (type-Pointed-Type Y)) × + ( iterated-loop-space n X ≃∗ Y)) +``` + +### The type of `n`-fold deloopings of a pointed type + +```agda +module _ + {l1 : Level} (n : ℕ) (X : Pointed-Type l1) + where + + iterated-delooping : UU (lsuc l1) + iterated-delooping = iterated-delooping-Level l1 n X +``` diff --git a/src/higher-group-theory/small-higher-groups.lagda.md b/src/higher-group-theory/small-higher-groups.lagda.md new file mode 100644 index 0000000000..0252d1093d --- /dev/null +++ b/src/higher-group-theory/small-higher-groups.lagda.md @@ -0,0 +1,308 @@ +# Small ∞-groups + +```agda +module higher-group-theory.small-higher-groups where +``` + +
Imports + +```agda +open import foundation.0-connected-types +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.identity-types +open import foundation.images +open import foundation.locally-small-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.replacement +open import foundation.small-types +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.unit-type +open import foundation.universe-levels + +open import higher-group-theory.equivalences-higher-groups +open import higher-group-theory.higher-groups + +open import structured-types.pointed-equivalences +open import structured-types.pointed-types +open import structured-types.small-pointed-types +``` + +
+ +## Idea + +An [∞-group](higher-group-theory.higher-groups.md) `G` is said to be +{{#concept "small" Disambiguation="∞-group" Agda=is-small-∞-Group}} with respect +to a universe `𝒰` if its underlying type is `𝒰`-small. By the +[type theoretic replacement principle](foundation.replacement.md) it follows +that `G` is small if and only if its classifying type `BG` is small. This +observation implies that an ∞-group `G` is small if and only if it is +{{#concept "structurally small" Disambiguation="∞-group" Agda=is-structurally-small-∞-Group}} +in the sense that it comes equipped with an element of type + +```text + Σ (H : ∞-Group), G ≃ H, +``` + +where the type `G ≃ H` is the type of +[equivalences of ∞-groups](higher-group-theory.equivalences-higher-groups.md). + +Finally, we also introduce the notion of _pointed small ∞-group_. An ∞-group `G` +is said to be +{{#concept "pointed small" Disambiguation="∞-group" Agda=is-pointed-small-∞-Group}} +if its classifying [pointed type](structured-types.pointed-types.md) `BG` is +[pointed small](structured-types.small-pointed-types.md). + +## Definitions + +### The predicate of being a small ∞-group + +```agda +module _ + {l1 : Level} (l2 : Level) (G : ∞-Group l1) + where + + is-small-prop-∞-Group : Prop (l1 ⊔ lsuc l2) + is-small-prop-∞-Group = is-small-Prop l2 (type-∞-Group G) + + is-small-∞-Group : UU (l1 ⊔ lsuc l2) + is-small-∞-Group = is-small l2 (type-∞-Group G) + + is-prop-is-small-∞-Group : is-prop is-small-∞-Group + is-prop-is-small-∞-Group = is-prop-is-small l2 (type-∞-Group G) +``` + +### The predicate of being a structurally small ∞-group + +```agda +module _ + {l1 : Level} (l2 : Level) (G : ∞-Group l1) + where + + is-structurally-small-∞-Group : UU (l1 ⊔ lsuc l2) + is-structurally-small-∞-Group = + Σ (∞-Group l2) (equiv-∞-Group G) + + abstract + is-prop-is-structurally-small-∞-Group : + is-prop is-structurally-small-∞-Group + is-prop-is-structurally-small-∞-Group = + is-prop-equiv + ( equiv-right-swap-Σ) + ( is-prop-Σ + ( is-prop-is-pointed-small-Pointed-Type + ( classifying-pointed-type-∞-Group G)) + ( λ H → is-prop-is-0-connected _)) + + is-structurally-small-prop-∞-Group : Prop (l1 ⊔ lsuc l2) + pr1 is-structurally-small-prop-∞-Group = is-structurally-small-∞-Group + pr2 is-structurally-small-prop-∞-Group = is-prop-is-structurally-small-∞-Group + +module _ + {l1 l2 : Level} (G : ∞-Group l1) (H : is-structurally-small-∞-Group l2 G) + where + + ∞-group-is-structurally-small-∞-Group : ∞-Group l2 + ∞-group-is-structurally-small-∞-Group = pr1 H + + type-∞-group-is-structurally-small-∞-Group : UU l2 + type-∞-group-is-structurally-small-∞-Group = + type-∞-Group ∞-group-is-structurally-small-∞-Group + + equiv-∞-group-is-structurally-small-∞-Group : + equiv-∞-Group G ∞-group-is-structurally-small-∞-Group + equiv-∞-group-is-structurally-small-∞-Group = pr2 H + + equiv-is-structurally-small-∞-Group : + type-∞-Group G ≃ type-∞-group-is-structurally-small-∞-Group + equiv-is-structurally-small-∞-Group = + equiv-equiv-∞-Group G + ( ∞-group-is-structurally-small-∞-Group) + ( equiv-∞-group-is-structurally-small-∞-Group) +``` + +### The predicate of being a pointed small ∞-group + +```agda +module _ + {l1 : Level} (l2 : Level) (G : ∞-Group l1) + where + + is-pointed-small-prop-∞-Group : Prop (l1 ⊔ lsuc l2) + is-pointed-small-prop-∞-Group = + is-pointed-small-prop-Pointed-Type l2 (classifying-pointed-type-∞-Group G) + + is-pointed-small-∞-Group : UU (l1 ⊔ lsuc l2) + is-pointed-small-∞-Group = + is-pointed-small-Pointed-Type l2 (classifying-pointed-type-∞-Group G) + + is-prop-is-pointed-small-∞-Group : is-prop is-pointed-small-∞-Group + is-prop-is-pointed-small-∞-Group = + is-prop-is-pointed-small-Pointed-Type (classifying-pointed-type-∞-Group G) +``` + +## Properties + +### The classifying type of any small ∞-group is locally small + +```agda +module _ + {l1 l2 : Level} (G : ∞-Group l1) (H : is-small-∞-Group l2 G) + where + + abstract + is-locally-small-classifying-type-is-small-∞-Group' : + (x y : classifying-type-∞-Group G) → + shape-∞-Group G ＝ x → shape-∞-Group G ＝ y → + is-small l2 (x ＝ y) + is-locally-small-classifying-type-is-small-∞-Group' ._ ._ refl refl = H + + abstract + is-locally-small-classifying-type-is-small-∞-Group : + is-locally-small l2 (classifying-type-∞-Group G) + is-locally-small-classifying-type-is-small-∞-Group x y = + apply-twice-universal-property-trunc-Prop + ( mere-eq-classifying-type-∞-Group G (shape-∞-Group G) x) + ( mere-eq-classifying-type-∞-Group G (shape-∞-Group G) y) + ( is-small-Prop l2 (x ＝ y)) + ( is-locally-small-classifying-type-is-small-∞-Group' x y) +``` + +### An ∞-group is small if and only if its classifying type is small + +```agda +module _ + {l1 l2 : Level} (G : ∞-Group l1) + where + + abstract + is-small-classifying-type-is-small-∞-Group : + is-small-∞-Group l2 G → is-small l2 (classifying-type-∞-Group G) + is-small-classifying-type-is-small-∞-Group H = + is-small-equiv' + ( im (point-∞-Group G)) + ( compute-im-point-∞-Group G) + ( replacement + ( point-∞-Group G) + ( is-small-unit) + ( is-locally-small-classifying-type-is-small-∞-Group G H)) + + abstract + is-small-is-small-classifying-type-∞-Group : + is-small l2 (classifying-type-∞-Group G) → is-small-∞-Group l2 G + is-small-is-small-classifying-type-∞-Group H = + is-locally-small-is-small H (shape-∞-Group G) (shape-∞-Group G) +``` + +### An ∞-group is small if and only if it is pointed small + +```agda +module _ + {l1 l2 : Level} (G : ∞-Group l1) + where + + abstract + is-pointed-small-is-small-∞-Group : + is-small-∞-Group l2 G → is-pointed-small-∞-Group l2 G + is-pointed-small-is-small-∞-Group H = + is-pointed-small-is-small-Pointed-Type + ( classifying-pointed-type-∞-Group G) + ( is-small-classifying-type-is-small-∞-Group G H) +``` + +### An ∞-group is small if and only if it is structurally small + +```agda +module _ + {l1 l2 : Level} (G : ∞-Group l1) + where + + classifying-pointed-type-is-small-∞-Group : + is-small-∞-Group l2 G → Pointed-Type l2 + classifying-pointed-type-is-small-∞-Group H = + pointed-type-is-pointed-small-Pointed-Type + ( classifying-pointed-type-∞-Group G) + ( is-pointed-small-is-small-∞-Group G H) + + classifying-type-is-small-∞-Group : is-small-∞-Group l2 G → UU l2 + classifying-type-is-small-∞-Group H = + type-is-pointed-small-Pointed-Type + ( classifying-pointed-type-∞-Group G) + ( is-pointed-small-is-small-∞-Group G H) + + abstract + is-0-connected-classifying-type-is-small-∞-Group : + (H : is-small-∞-Group l2 G) → + is-0-connected (classifying-type-is-small-∞-Group H) + is-0-connected-classifying-type-is-small-∞-Group H = + is-0-connected-equiv' + ( equiv-is-pointed-small-Pointed-Type + ( classifying-pointed-type-∞-Group G) + ( is-pointed-small-is-small-∞-Group G H)) + ( is-0-connected-classifying-type-∞-Group G) + + ∞-group-is-small-∞-Group : is-small-∞-Group l2 G → ∞-Group l2 + pr1 (∞-group-is-small-∞-Group H) = + classifying-pointed-type-is-small-∞-Group H + pr2 (∞-group-is-small-∞-Group H) = + is-0-connected-classifying-type-is-small-∞-Group H + + pointed-type-∞-group-is-small-∞-Group : + is-small-∞-Group l2 G → Pointed-Type l2 + pointed-type-∞-group-is-small-∞-Group H = + pointed-type-∞-Group (∞-group-is-small-∞-Group H) + + type-∞-group-is-small-∞-Group : + is-small-∞-Group l2 G → UU l2 + type-∞-group-is-small-∞-Group H = + type-∞-Group (∞-group-is-small-∞-Group H) + + equiv-∞-group-is-small-∞-Group : + (H : is-small-∞-Group l2 G) → equiv-∞-Group G (∞-group-is-small-∞-Group H) + equiv-∞-group-is-small-∞-Group H = + pointed-equiv-is-pointed-small-Pointed-Type + ( classifying-pointed-type-∞-Group G) + ( is-pointed-small-is-small-∞-Group G H) + + pointed-equiv-equiv-∞-group-is-small-∞-Group : + (H : is-small-∞-Group l2 G) → + pointed-type-∞-Group G ≃∗ pointed-type-∞-group-is-small-∞-Group H + pointed-equiv-equiv-∞-group-is-small-∞-Group H = + pointed-equiv-equiv-∞-Group G + ( ∞-group-is-small-∞-Group H) + ( equiv-∞-group-is-small-∞-Group H) + + equiv-equiv-∞-group-is-small-∞-Group : + (H : is-small-∞-Group l2 G) → + type-∞-Group G ≃ type-∞-group-is-small-∞-Group H + equiv-equiv-∞-group-is-small-∞-Group H = + equiv-equiv-∞-Group G + ( ∞-group-is-small-∞-Group H) + ( equiv-∞-group-is-small-∞-Group H) + + abstract + is-structurally-small-is-small-∞-Group : + is-small-∞-Group l2 G → is-structurally-small-∞-Group l2 G + pr1 (is-structurally-small-is-small-∞-Group H) = + ∞-group-is-small-∞-Group H + pr2 (is-structurally-small-is-small-∞-Group H) = + equiv-∞-group-is-small-∞-Group H + + abstract + is-small-is-structurally-small-∞-Group : + is-structurally-small-∞-Group l2 G → is-small-∞-Group l2 G + pr1 (is-small-is-structurally-small-∞-Group H) = + type-∞-group-is-structurally-small-∞-Group G H + pr2 (is-small-is-structurally-small-∞-Group H) = + equiv-is-structurally-small-∞-Group G H + + abstract + is-small-∞-group-is-small-∞-Group : + (H : is-small-∞-Group l2 G) → + is-small-∞-Group l1 (∞-group-is-small-∞-Group H) + pr1 (is-small-∞-group-is-small-∞-Group H) = type-∞-Group G + pr2 (is-small-∞-group-is-small-∞-Group H) = + inv-equiv (equiv-equiv-∞-group-is-small-∞-Group H) +``` diff --git a/src/lists/universal-property-lists-wild-monoids.lagda.md b/src/lists/universal-property-lists-wild-monoids.lagda.md index 9192fc3733..67c4735fec 100644 --- a/src/lists/universal-property-lists-wild-monoids.lagda.md +++ b/src/lists/universal-property-lists-wild-monoids.lagda.md @@ -22,6 +22,8 @@ open import lists.lists open import structured-types.h-spaces open import structured-types.morphisms-h-spaces open import structured-types.morphisms-wild-monoids +open import structured-types.pointed-maps +open import structured-types.pointed-types open import structured-types.wild-monoids ``` @@ -34,19 +36,24 @@ map from `X` into it. ## Definition +### The pointed type of lists of elements of `X` + +```agda +list-pointed-type : {l : Level} → UU l → Pointed-Type l +pr1 (list-pointed-type X) = list X +pr2 (list-pointed-type X) = nil +``` + ### The H-space of lists of elements of `X` ```agda list-H-Space : {l : Level} (X : UU l) → H-Space l -list-H-Space X = - pair - ( pair (list X) nil) - ( pair - ( concat-list) - ( pair - ( left-unit-law-concat-list) - ( pair right-unit-law-concat-list refl))) +pr1 (list-H-Space X) = list-pointed-type X +pr1 (pr2 (list-H-Space X)) = concat-list +pr1 (pr2 (pr2 (list-H-Space X))) = left-unit-law-concat-list +pr1 (pr2 (pr2 (pr2 (list-H-Space X)))) = right-unit-law-concat-list +pr2 (pr2 (pr2 (pr2 (list-H-Space X)))) = refl ``` ### The wild monoid of lists of elements of `X` @@ -140,6 +147,13 @@ module _ Id (map-elim-list-Wild-Monoid nil) (unit-Wild-Monoid M) preserves-unit-map-elim-list-Wild-Monoid = refl + pointed-map-elim-list-Wild-Monoid : + list-pointed-type X →∗ pointed-type-Wild-Monoid M + pr1 pointed-map-elim-list-Wild-Monoid = + map-elim-list-Wild-Monoid + pr2 pointed-map-elim-list-Wild-Monoid = + preserves-unit-map-elim-list-Wild-Monoid + preserves-mul-map-elim-list-Wild-Monoid : preserves-mul' ( concat-list) @@ -157,14 +171,10 @@ module _ ( map-elim-list-Wild-Monoid y))) preserves-left-unit-law-map-elim-list-Wild-Monoid : - preserves-left-unit-law-mul - ( concat-list) - { nil} - ( left-unit-law-concat-list) - ( mul-Wild-Monoid M) - ( left-unit-law-mul-Wild-Monoid M) - ( map-elim-list-Wild-Monoid) - ( preserves-unit-map-elim-list-Wild-Monoid) + preserves-left-unit-law-mul-pointed-map-H-Space + ( list-H-Space X) + ( h-space-Wild-Monoid M) + ( pointed-map-elim-list-Wild-Monoid) ( λ {x} {y} → preserves-mul-map-elim-list-Wild-Monoid x y) preserves-left-unit-law-map-elim-list-Wild-Monoid x = inv @@ -172,14 +182,10 @@ module _ ( left-unit-law-mul-Wild-Monoid M (map-elim-list-Wild-Monoid x))) preserves-right-unit-law-map-elim-list-Wild-Monoid : - preserves-right-unit-law-mul - ( concat-list) - { nil} - ( right-unit-law-concat-list) - ( mul-Wild-Monoid M) - ( right-unit-law-mul-Wild-Monoid M) - ( map-elim-list-Wild-Monoid) - ( preserves-unit-map-elim-list-Wild-Monoid) + preserves-right-unit-law-mul-pointed-map-H-Space + ( list-H-Space X) + ( h-space-Wild-Monoid M) + ( pointed-map-elim-list-Wild-Monoid) ( λ {x} {y} → preserves-mul-map-elim-list-Wild-Monoid x y) preserves-right-unit-law-map-elim-list-Wild-Monoid nil = ( inv (left-inv (left-unit-law-mul-Wild-Monoid M (unit-Wild-Monoid M)))) ∙ @@ -270,10 +276,10 @@ module _ preserves-coh-unit-laws-map-elim-list-Wild-Monoid : {l1 l2 : Level} {X : UU l1} (M : Wild-Monoid l2) (f : X → type-Wild-Monoid M) → - preserves-coh-unit-laws-mul + preserves-coherence-unit-laws-mul-pointed-map-H-Space ( list-H-Space X) ( h-space-Wild-Monoid M) - ( pair (map-elim-list-Wild-Monoid M f) refl) + ( pointed-map-elim-list-Wild-Monoid M f) ( λ {x} {y} → preserves-mul-map-elim-list-Wild-Monoid M f x y) ( preserves-left-unit-law-map-elim-list-Wild-Monoid M f) ( preserves-right-unit-law-map-elim-list-Wild-Monoid M f) diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md index 278c465791..d93143905e 100644 --- a/src/structured-types.lagda.md +++ b/src/structured-types.lagda.md @@ -22,6 +22,7 @@ open import structured-types.dependent-products-h-spaces public open import structured-types.dependent-products-pointed-types public open import structured-types.dependent-products-wild-monoids public open import structured-types.dependent-types-equipped-with-automorphisms public +open import structured-types.equivalences-h-spaces public open import structured-types.equivalences-pointed-arrows public open import structured-types.equivalences-types-equipped-with-automorphisms public open import structured-types.equivalences-types-equipped-with-endomorphisms public @@ -74,6 +75,7 @@ open import structured-types.postcomposition-pointed-maps public open import structured-types.precomposition-pointed-maps public open import structured-types.reflexive-globular-types public open import structured-types.sets-equipped-with-automorphisms public +open import structured-types.small-pointed-types public open import structured-types.symmetric-elements-involutive-types public open import structured-types.symmetric-globular-types public open import structured-types.symmetric-h-spaces public diff --git a/src/structured-types/equivalences-h-spaces.lagda.md b/src/structured-types/equivalences-h-spaces.lagda.md new file mode 100644 index 0000000000..3a8285ea5c --- /dev/null +++ b/src/structured-types/equivalences-h-spaces.lagda.md @@ -0,0 +1,243 @@ +# Equivalences of H-spaces + +```agda +module structured-types.equivalences-h-spaces where +``` + +
Imports + +```agda +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.commuting-squares-of-identifications +open import foundation.commuting-triangles-of-identifications +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.path-algebra +open import foundation.universe-levels +open import foundation.whiskering-identifications-concatenation + +open import group-theory.homomorphisms-semigroups + +open import structured-types.h-spaces +open import structured-types.morphisms-h-spaces +open import structured-types.pointed-equivalences +open import structured-types.pointed-maps +open import structured-types.pointed-types +``` + +
+ +## Idea + +Consider two [H-spaces](structured-types.h-spaces.md) `X` and `Y`. An +{{#concept "equivalence of H-spaces" Agda=equiv-H-Space}} from `X` to `Y` +consists of a [pointed equivalence](structured-types.pointed-equivalences.md) +`e : X ≃∗ Y` that preserves the unital binary operation + +```text + α : (x x' : X) → e (μ x x') ＝ μ (e x) (e x') +``` + +and which furthermore comes equipped with the following structure, witnessing +that the unit laws are preserved: + +- For each `x' : X` an identification `α₁ x'` witnessing that the triangle + + ```text + α * x' + e (μ * x') -------> μ (e *) (e x') + \ / + \ / ap (μ - (e x')) e₁ + \ / + \ ∨ + ap e (left-unit-law x') \ μ * (e x') + \ / + \ / left-unit-law (e x') + \ / + ∨ ∨ + e x' + ``` + + commutes. + +- For each `x : X` an identification `α₂ x` witnessing that the triangle + + ```text + α x * + e (μ x *) --------> μ (e x) (e *) + \ / + \ / ap (μ (e x) -) e₁ + \ / + \ ∨ + ap e (right-unit-law x) \ μ (e x) * + \ / + \ / right-unit-law (e x) + \ / + ∨ ∨ + e x + ``` + + commutes. + +- An identification `α₃` witnessing that the square + + ```text + α₁ + α₀ * * ∙ (ap (μ - (e *)) e₁ ∙ left-unit-law *) ---> ap e (left-unit-law *) + | | + (α₀ * *) ·l β | | + ∨ ∨ + α₀ * * ∙ (ap (μ (e *) -) e₁ ∙ right-unit-law *) ---> ap e (right-unit-law *) + α₂ + ``` + + Here, the identification on the left is obtained by left whiskering the + identification witnessing that the square + + ```text + ap (μ (e *)) e₁ + μ (e *) (e *) -----------------> μ (e *) * + | | + ap (μ - (e *)) e₁ | β | right-unit-law (e *) + ∨ ∨ + μ * (e *) ----------------------> e * + left-unit-law (e *) + ``` + + commutes, with the identification `α * * : e (μ * *) ＝ μ (e *) (e *)`. The + quickest way to see that this square commutes is by identification elimination + on the identification `e₁ : e * ＝ *`, using the coherence + `left-unit-law * ＝ right-unit-law *`. Alternatively, note that all the + squares in the diagram + + ```text + ap (μ (e *)) e₁ + μ (e *) (e *) -----------------> μ (e *) * --------> e * + | | | + ap (μ - (e *)) e₁ | ap (μ - *) e₁ | | + ∨ ∨ ∨ + μ * (e *) ---------------------> μ * * ----------> * + | ap (μ *) e₁ | | + | | coh ·r refl | refl + ∨ ∨ ∨ + e * ---------------------------> * ------------> * + e₁ refl + ``` + + commute. Therefore we obtain an identification + + ```text + ap (μ - (e *)) e₁ ∙ (left-unit-law (e *) ∙ e₁) ＝ + ap (μ (e *) -) e₁ ∙ (right-unit-law (e *) ∙ e₁). + ``` + + By unwhiskering of commuting squares of identifications, i.e., by cancelling + out `e₁` on both sides, it follows that the asserted square commutes. + +## Definition + +### The predicate of preserving H-space structure on a pointed type + +```agda +module _ + {l1 l2 : Level} (M : H-Space l1) (N : H-Space l2) + where + + preserves-mul-pointed-equiv-H-Space : + (pointed-type-H-Space M ≃∗ pointed-type-H-Space N) → UU (l1 ⊔ l2) + preserves-mul-pointed-equiv-H-Space e = + preserves-mul-pointed-map-H-Space M N (pointed-map-pointed-equiv e) + + preserves-left-unit-law-mul-pointed-equiv-H-Space : + (e : pointed-type-H-Space M ≃∗ pointed-type-H-Space N) → + preserves-mul-pointed-equiv-H-Space e → UU (l1 ⊔ l2) + preserves-left-unit-law-mul-pointed-equiv-H-Space e = + preserves-left-unit-law-mul-pointed-map-H-Space M N + ( pointed-map-pointed-equiv e) + + preserves-right-unit-law-mul-pointed-equiv-H-Space : + (e : pointed-type-H-Space M ≃∗ pointed-type-H-Space N) → + preserves-mul-pointed-equiv-H-Space e → UU (l1 ⊔ l2) + preserves-right-unit-law-mul-pointed-equiv-H-Space e = + preserves-right-unit-law-mul-pointed-map-H-Space M N + ( pointed-map-pointed-equiv e) + + preserves-coherence-unit-laws-mul-pointed-equiv-H-Space : + (e : pointed-type-H-Space M ≃∗ pointed-type-H-Space N) → + (μ : preserves-mul-pointed-equiv-H-Space e) → + (ν : preserves-left-unit-law-mul-pointed-equiv-H-Space e μ) → + (ρ : preserves-right-unit-law-mul-pointed-equiv-H-Space e μ) → UU l2 + preserves-coherence-unit-laws-mul-pointed-equiv-H-Space e = + preserves-coherence-unit-laws-mul-pointed-map-H-Space M N + ( pointed-map-pointed-equiv e) + + preserves-unital-mul-pointed-equiv-H-Space : + (e : pointed-type-H-Space M ≃∗ pointed-type-H-Space N) → + UU (l1 ⊔ l2) + preserves-unital-mul-pointed-equiv-H-Space e = + preserves-unital-mul-pointed-map-H-Space M N (pointed-map-pointed-equiv e) +``` + +### Equivalences of H-spaces + +```agda +module _ + {l1 l2 : Level} (M : H-Space l1) (N : H-Space l2) + where + + equiv-H-Space : UU (l1 ⊔ l2) + equiv-H-Space = + Σ ( pointed-type-H-Space M ≃∗ pointed-type-H-Space N) + ( preserves-unital-mul-pointed-equiv-H-Space M N) + +module _ + {l1 l2 : Level} {M : H-Space l1} {N : H-Space l2} (e : equiv-H-Space M N) + where + + pointed-equiv-equiv-H-Space : pointed-type-H-Space M ≃∗ pointed-type-H-Space N + pointed-equiv-equiv-H-Space = pr1 e + + map-equiv-H-Space : type-H-Space M → type-H-Space N + map-equiv-H-Space = map-pointed-equiv pointed-equiv-equiv-H-Space + + preserves-unit-equiv-H-Space : + map-equiv-H-Space (unit-H-Space M) ＝ unit-H-Space N + preserves-unit-equiv-H-Space = + preserves-point-pointed-equiv pointed-equiv-equiv-H-Space + + preserves-unital-mul-equiv-H-Space : + preserves-unital-mul-pointed-equiv-H-Space M N pointed-equiv-equiv-H-Space + preserves-unital-mul-equiv-H-Space = pr2 e + + preserves-mul-equiv-H-Space : + preserves-mul-pointed-equiv-H-Space M N pointed-equiv-equiv-H-Space + preserves-mul-equiv-H-Space = + pr1 preserves-unital-mul-equiv-H-Space + + preserves-left-unit-law-mul-equiv-H-Space : + preserves-left-unit-law-mul-pointed-equiv-H-Space M N + ( pointed-equiv-equiv-H-Space) + ( preserves-mul-equiv-H-Space) + preserves-left-unit-law-mul-equiv-H-Space = + pr1 (pr2 preserves-unital-mul-equiv-H-Space) + + preserves-right-unit-law-mul-equiv-H-Space : + preserves-right-unit-law-mul-pointed-equiv-H-Space M N + ( pointed-equiv-equiv-H-Space) + ( preserves-mul-equiv-H-Space) + preserves-right-unit-law-mul-equiv-H-Space = + pr1 (pr2 (pr2 preserves-unital-mul-equiv-H-Space)) + + preserves-coherence-unit-laws-mul-equiv-H-Space : + preserves-coherence-unit-laws-mul-pointed-equiv-H-Space M N + ( pointed-equiv-equiv-H-Space) + ( preserves-mul-equiv-H-Space) + ( preserves-left-unit-law-mul-equiv-H-Space) + ( preserves-right-unit-law-mul-equiv-H-Space) + preserves-coherence-unit-laws-mul-equiv-H-Space = + pr2 (pr2 (pr2 preserves-unital-mul-equiv-H-Space)) +``` diff --git a/src/structured-types/h-spaces.lagda.md b/src/structured-types/h-spaces.lagda.md index ddb89b6c0a..be217b8539 100644 --- a/src/structured-types/h-spaces.lagda.md +++ b/src/structured-types/h-spaces.lagda.md @@ -60,11 +60,27 @@ coherent-unital-mul-Pointed-Type A = ### H-spaces +An H-space consists of a pointed type `X` and a coherent unital multiplication +on `X`. The entry `make-H-Space` is provided to break up the construction of an +H-space into two components: the construction of its underlying pointed type and +the construction of the coherently unital multiplication on this pointed type. +Furthermore, this definition suggests that any construction of an H-space should +be refactored by first defining its underlying pointed type, then defining its +coherently unital multiplication, and finally combining those two constructions +using `make-H-Space`. + ```agda H-Space : (l : Level) → UU (lsuc l) H-Space l = Σ ( Pointed-Type l) coherent-unital-mul-Pointed-Type +make-H-Space : + {l : Level} → + (X : Pointed-Type l) → coherent-unital-mul-Pointed-Type X → H-Space l +make-H-Space X μ = (X , μ) + +{-# INLINE make-H-Space #-} + module _ {l : Level} (M : H-Space l) where diff --git a/src/structured-types/morphisms-h-spaces.lagda.md b/src/structured-types/morphisms-h-spaces.lagda.md index 58402af847..15fe75ebf3 100644 --- a/src/structured-types/morphisms-h-spaces.lagda.md +++ b/src/structured-types/morphisms-h-spaces.lagda.md @@ -10,6 +10,8 @@ module structured-types.morphisms-h-spaces where 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.commuting-squares-of-identifications +open import foundation.commuting-triangles-of-identifications open import foundation.dependent-pair-types open import foundation.function-types open import foundation.homotopies @@ -22,195 +24,289 @@ open import group-theory.homomorphisms-semigroups open import structured-types.h-spaces open import structured-types.pointed-maps +open import structured-types.pointed-types ``` ## Idea -Morphisms of [H-spaces](structured-types.h-spaces.md) are -[pointed maps](structured-types.pointed-maps.md) that preserve the unital binary -operation, including its laws. +Consider two [H-spaces](structured-types.h-spaces.md) `X` and `Y`. A +{{#concept "morphism of H-spaces" Agda=hom-H-Space}} from `X` to `Y` consists of +a [pointed map](structured-types.pointed-maps.md) `f : X →∗ Y` that preserves +the unital binary operation + +```text + α : (x x' : X) → f (μ x x') ＝ μ (f x) (f x') +``` + +and which furthermore comes equipped with the following structure, witnessing +that the unit laws are preserved: + +- For each `x' : X` an identification `α₁ x'` witnessing that the triangle + + ```text + α * x' + f (μ * x') -------> μ (f *) (f x') + \ / + \ / ap (μ - (f x')) f₁ + \ / + \ ∨ + ap f (left-unit-law x') \ μ * (f x') + \ / + \ / left-unit-law (f x') + \ / + ∨ ∨ + f x' + ``` + + commutes. + +- For each `x : X` an identification `α₂ x` witnessing that the triangle + + ```text + α x * + f (μ x *) --------> μ (f x) (f *) + \ / + \ / ap (μ (f x) -) f₁ + \ / + \ ∨ + ap f (right-unit-law x) \ μ (f x) * + \ / + \ / right-unit-law (f x) + \ / + ∨ ∨ + f x + ``` + + commutes. + +- An identification `α₃` witnessing that the square + + ```text + α₁ + α₀ * * ∙ (ap (μ - (f *)) f₁ ∙ left-unit-law *) ---> ap f (left-unit-law *) + | | + (α₀ * *) ·l β | | + ∨ ∨ + α₀ * * ∙ (ap (μ (f *) -) f₁ ∙ right-unit-law *) ---> ap f (right-unit-law *) + α₂ + ``` + + Here, the identification on the left is obtained by left whiskering the + identification witnessing that the square + + ```text + ap (μ (f *)) f₁ + μ (f *) (f *) -----------------> μ (f *) * + | | + ap (μ - (f *)) f₁ | β | right-unit-law (f *) + ∨ ∨ + μ * (f *) ----------------------> f * + left-unit-law (f *) + ``` + + commutes, with the identification `α * * : f (μ * *) ＝ μ (f *) (f *)`. The + quickest way to see that this square commutes is by identification elimination + on the identification `f₁ : f * ＝ *`, using the coherence + `left-unit-law * ＝ right-unit-law *`. Alternatively, note that all the + squares in the diagram + + ```text + ap (μ (f *)) f₁ + μ (f *) (f *) -----------------> μ (f *) * --------> f * + | | | + ap (μ - (f *)) f₁ | ap (μ - *) f₁ | | + ∨ ∨ ∨ + μ * (f *) ---------------------> μ * * ----------> * + | ap (μ *) f₁ | | + | | coh ·r refl | refl + ∨ ∨ ∨ + f * ---------------------------> * ------------> * + f₁ refl + ``` + + commute. Therefore we obtain an identification + + ```text + ap (μ - (f *)) f₁ ∙ (left-unit-law (f *) ∙ f₁) ＝ + ap (μ (f *) -) f₁ ∙ (right-unit-law (f *) ∙ f₁). + ``` + + By unwhiskering of commuting squares of identifications, i.e., by cancelling + out `f₁` on both sides, it follows that the asserted square commutes. ## Definition -### Morphisms of H-spaces +### The predicate of preserving left and right unit laws ```agda -preserves-left-unit-law-mul : - {l1 l2 : Level} {A : UU l1} {B : UU l2} - (μ : A → A → A) {eA : A} → ((x : A) → Id (μ eA x) x) → - (ν : B → B → B) {eB : B} → ((y : B) → Id (ν eB y) y) → - (f : A → B) → Id (f eA) eB → preserves-mul μ ν f → UU (l1 ⊔ l2) -preserves-left-unit-law-mul {A = A} {B} μ {eA} lA ν {eB} lB f p μf = - (x : A) → Id (ap f (lA x)) (μf ∙ (ap (λ t → ν t (f x)) p ∙ lB (f x))) - -preserves-right-unit-law-mul : - {l1 l2 : Level} {A : UU l1} {B : UU l2} - (μ : A → A → A) {eA : A} → ((x : A) → Id (μ x eA) x) → - (ν : B → B → B) {eB : B} → ((y : B) → Id (ν y eB) y) → - (f : A → B) → Id (f eA) eB → preserves-mul μ ν f → UU (l1 ⊔ l2) -preserves-right-unit-law-mul {A = A} {B} μ {eA} rA ν {eB} rB f p μf = - (x : A) → Id (ap f (rA x)) (μf ∙ (ap (ν (f x)) p ∙ rB (f x))) - -preserves-coh-unit-laws-mul : - {l1 l2 : Level} (M : H-Space l1) (N : H-Space l2) → - ( f : pointed-type-H-Space M →∗ pointed-type-H-Space N) → - ( μf : - preserves-mul (mul-H-Space M) (mul-H-Space N) (pr1 f)) → - preserves-left-unit-law-mul - ( mul-H-Space M) - ( left-unit-law-mul-H-Space M) - ( mul-H-Space N) - ( left-unit-law-mul-H-Space N) - ( pr1 f) - ( pr2 f) - ( μf) → - preserves-right-unit-law-mul - ( mul-H-Space M) - ( right-unit-law-mul-H-Space M) - ( mul-H-Space N) - ( right-unit-law-mul-H-Space N) - ( pr1 f) - ( pr2 f) - ( μf) → - UU l2 -preserves-coh-unit-laws-mul M - (pair (pair N ._) μ) - (pair f refl) μf lf rf = - Id (ap² f cM ∙ rf eM) (lf eM ∙ ap (concat μf (f eM)) cN) +module _ + {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B) + (μ : (x y : type-Pointed-Type A) → type-Pointed-Type A) + (ν : (x y : type-Pointed-Type B) → type-Pointed-Type B) + (μf : preserves-mul μ ν (map-pointed-map f)) where - eM = unit-H-Space M - cM = coh-unit-laws-mul-H-Space M - cN = pr2 (pr2 (pr2 μ)) + + preserves-left-unit-law-mul : + ((x : type-Pointed-Type A) → μ (point-Pointed-Type A) x ＝ x) → + ((y : type-Pointed-Type B) → Id (ν (point-Pointed-Type B) y) y) → + UU (l1 ⊔ l2) + preserves-left-unit-law-mul lA lB = + (x : type-Pointed-Type A) → + coherence-triangle-identifications + ( ap (map-pointed-map f) (lA x)) + ( ( ap + ( λ t → ν t (map-pointed-map f x)) + ( preserves-point-pointed-map f)) ∙ + ( lB (map-pointed-map f x))) + ( μf) + + preserves-right-unit-law-mul : + ((x : type-Pointed-Type A) → μ x (point-Pointed-Type A) ＝ x) → + ((y : type-Pointed-Type B) → ν y (point-Pointed-Type B) ＝ y) → + UU (l1 ⊔ l2) + preserves-right-unit-law-mul rA rB = + (x : type-Pointed-Type A) → + coherence-triangle-identifications + ( ap (map-pointed-map f) (rA x)) + ( ( ap (ν (map-pointed-map f x)) (preserves-point-pointed-map f)) ∙ + ( rB (map-pointed-map f x))) + ( μf) ``` -### Second description of preservation of the coherent unit laws +### The predicate of preserving H-space structure on a pointed type ```agda -preserves-coh-unit-laws-mul' : - {l1 l2 : Level} (M : H-Space l1) (N : H-Space l2) → - ( f : pointed-type-H-Space M →∗ pointed-type-H-Space N) → - ( μf : - preserves-mul (mul-H-Space M) (mul-H-Space N) (pr1 f)) → - preserves-left-unit-law-mul - ( mul-H-Space M) - ( left-unit-law-mul-H-Space M) - ( mul-H-Space N) - ( left-unit-law-mul-H-Space N) - ( pr1 f) - ( pr2 f) - ( μf) → - preserves-right-unit-law-mul - ( mul-H-Space M) - ( right-unit-law-mul-H-Space M) - ( mul-H-Space N) - ( right-unit-law-mul-H-Space N) - ( pr1 f) - ( pr2 f) - ( μf) → - UU l2 -preserves-coh-unit-laws-mul' M N f μf lf rf = - Id - { A = - Id (ap (pr1 f) (lM eM) ∙ ef) ((μf ∙ ap-binary μN ef ef) ∙ rN eN)} - ( ( horizontal-concat-Id² (lf eM) (inv (ap-id ef))) ∙ - ( ( right-whisker-concat - ( inv - ( assoc - ( μf) - ( ap (mul-H-Space' N (pr1 f eM)) ef) - ( lN (pr1 f eM)))) - ( ap id ef)) ∙ - ( ( assoc - ( μf ∙ ap (mul-H-Space' N (pr1 f eM)) ef) - ( lN (pr1 f eM)) - ( ap id ef)) ∙ - ( ( left-whisker-concat - ( μf ∙ ap (mul-H-Space' N (pr1 f eM)) ef) - ( nat-htpy lN ef)) ∙ - ( ( inv - ( assoc - ( μf ∙ ap (mul-H-Space' N (pr1 f eM)) ef) - ( ap (μN eN) ef) - ( lN eN))) ∙ - ( ( ap - ( λ t → t ∙ lN eN) - ( assoc - ( μf) - ( ap (mul-H-Space' N (pr1 f eM)) ef) - ( ap (μN eN) ef))) ∙ - ( horizontal-concat-Id² - ( left-whisker-concat - ( μf) - ( inv (triangle-ap-binary μN ef ef))) - ( cN)))))))) - ( ( right-whisker-concat (ap² (pr1 f) cM) ef) ∙ - ( ( horizontal-concat-Id² (rf eM) (inv (ap-id ef))) ∙ - ( ( right-whisker-concat - ( inv - ( assoc - ( μf) (ap (μN (pr1 f eM)) ef) (rN (pr1 f eM)))) - ( ap id ef)) ∙ - ( ( assoc - ( μf ∙ ap (μN (pr1 f eM)) ef) - ( rN (pr1 f eM)) - ( ap id ef)) ∙ - ( ( left-whisker-concat - ( μf ∙ ap (μN (pr1 f eM)) ef) - ( nat-htpy rN ef)) ∙ - ( ( inv - ( assoc - ( μf ∙ ap (μN (pr1 f eM)) ef) - ( ap (mul-H-Space' N eN) ef) - ( rN eN))) ∙ - ( ap - ( λ t → t ∙ rN eN) - ( ( assoc - ( μf) - ( ap (μN (pr1 f eM)) ef) - ( ap (mul-H-Space' N eN) ef)) ∙ - ( left-whisker-concat - ( μf) - ( inv (triangle-ap-binary' μN ef ef))))))))))) +module _ + {l1 l2 : Level} (M : H-Space l1) (N : H-Space l2) where - eM = unit-H-Space M - μM = mul-H-Space M - lM = left-unit-law-mul-H-Space M - rM = right-unit-law-mul-H-Space M - cM = coh-unit-laws-mul-H-Space M - eN = unit-H-Space N - μN = mul-H-Space N - lN = left-unit-law-mul-H-Space N - rN = right-unit-law-mul-H-Space N - cN = coh-unit-laws-mul-H-Space N - ef = pr2 f - -preserves-unital-mul : - {l1 l2 : Level} (M : H-Space l1) (N : H-Space l2) → - (f : pointed-type-H-Space M →∗ pointed-type-H-Space N) → - UU (l1 ⊔ l2) -preserves-unital-mul M N f = - Σ ( preserves-mul μM μN (pr1 f)) - ( λ μ11 → - Σ ( preserves-left-unit-law-mul μM lM μN lN (pr1 f) (pr2 f) μ11) - ( λ μ01 → - Σ ( preserves-right-unit-law-mul μM rM μN rN (pr1 f) (pr2 f) μ11) - ( λ μ10 → preserves-coh-unit-laws-mul M N f μ11 μ01 μ10))) + + preserves-mul-pointed-map-H-Space : + (pointed-type-H-Space M →∗ pointed-type-H-Space N) → UU (l1 ⊔ l2) + preserves-mul-pointed-map-H-Space f = + preserves-mul (mul-H-Space M) (mul-H-Space N) (map-pointed-map f) + + preserves-left-unit-law-mul-pointed-map-H-Space : + (f : pointed-type-H-Space M →∗ pointed-type-H-Space N) → + preserves-mul-pointed-map-H-Space f → UU (l1 ⊔ l2) + preserves-left-unit-law-mul-pointed-map-H-Space f μf = + preserves-left-unit-law-mul f + ( mul-H-Space M) + ( mul-H-Space N) + ( μf) + ( left-unit-law-mul-H-Space M) + ( left-unit-law-mul-H-Space N) + + preserves-right-unit-law-mul-pointed-map-H-Space : + (f : pointed-type-H-Space M →∗ pointed-type-H-Space N) → + preserves-mul-pointed-map-H-Space f → UU (l1 ⊔ l2) + preserves-right-unit-law-mul-pointed-map-H-Space f μf = + preserves-right-unit-law-mul f + ( mul-H-Space M) + ( mul-H-Space N) + ( μf) + ( right-unit-law-mul-H-Space M) + ( right-unit-law-mul-H-Space N) + + coherence-square-unit-laws-preserves-point-pointed-map-H-Space : + (f : pointed-type-H-Space M →∗ pointed-type-H-Space N) → + coherence-square-identifications + ( ap + ( mul-H-Space N (map-pointed-map f (unit-H-Space M))) + ( preserves-point-pointed-map f)) + ( ap + ( mul-H-Space' N (map-pointed-map f (unit-H-Space M))) + ( preserves-point-pointed-map f)) + ( right-unit-law-mul-H-Space N (map-pointed-map f (unit-H-Space M))) + ( left-unit-law-mul-H-Space N (map-pointed-map f (unit-H-Space M))) + coherence-square-unit-laws-preserves-point-pointed-map-H-Space (f , refl) = + coh-unit-laws-mul-H-Space N + + preserves-coherence-unit-laws-mul-pointed-map-H-Space : + (f : pointed-type-H-Space M →∗ pointed-type-H-Space N) → + (μ : preserves-mul-pointed-map-H-Space f) → + (ν : preserves-left-unit-law-mul-pointed-map-H-Space f μ) → + (ρ : preserves-right-unit-law-mul-pointed-map-H-Space f μ) → UU l2 + preserves-coherence-unit-laws-mul-pointed-map-H-Space f μ ν ρ = + coherence-square-identifications + ( ν (unit-H-Space M)) + ( ap² (map-pointed-map f) (coh-unit-laws-mul-H-Space M)) + ( left-whisker-concat + ( μ) + ( coherence-square-unit-laws-preserves-point-pointed-map-H-Space f)) + ( ρ (unit-H-Space M)) + + preserves-unital-mul-pointed-map-H-Space : + (f : pointed-type-H-Space M →∗ pointed-type-H-Space N) → + UU (l1 ⊔ l2) + preserves-unital-mul-pointed-map-H-Space f = + Σ ( preserves-mul-pointed-map-H-Space f) + ( λ μ → + Σ ( preserves-left-unit-law-mul-pointed-map-H-Space f μ) + ( λ ν → + Σ ( preserves-right-unit-law-mul-pointed-map-H-Space f μ) + ( preserves-coherence-unit-laws-mul-pointed-map-H-Space f μ ν))) +``` + +### Morphisms of H-spaces + +```agda +module _ + {l1 l2 : Level} (M : H-Space l1) (N : H-Space l2) where - μM = mul-H-Space M - lM = left-unit-law-mul-H-Space M - rM = right-unit-law-mul-H-Space M - μN = mul-H-Space N - lN = left-unit-law-mul-H-Space N - rN = right-unit-law-mul-H-Space N - -hom-H-Space : - {l1 l2 : Level} (M : H-Space l1) (N : H-Space l2) → - UU (l1 ⊔ l2) -hom-H-Space M N = - Σ ( pointed-type-H-Space M →∗ pointed-type-H-Space N) - ( preserves-unital-mul M N) + + hom-H-Space : UU (l1 ⊔ l2) + hom-H-Space = + Σ ( pointed-type-H-Space M →∗ pointed-type-H-Space N) + ( preserves-unital-mul-pointed-map-H-Space M N) + +module _ + {l1 l2 : Level} {M : H-Space l1} {N : H-Space l2} (f : hom-H-Space M N) + where + + pointed-map-hom-H-Space : pointed-type-H-Space M →∗ pointed-type-H-Space N + pointed-map-hom-H-Space = pr1 f + + map-hom-H-Space : type-H-Space M → type-H-Space N + map-hom-H-Space = map-pointed-map pointed-map-hom-H-Space + + preserves-unit-hom-H-Space : + map-hom-H-Space (unit-H-Space M) ＝ unit-H-Space N + preserves-unit-hom-H-Space = + preserves-point-pointed-map pointed-map-hom-H-Space + + preserves-unital-mul-hom-H-Space : + preserves-unital-mul-pointed-map-H-Space M N pointed-map-hom-H-Space + preserves-unital-mul-hom-H-Space = pr2 f + + preserves-mul-hom-H-Space : + preserves-mul-pointed-map-H-Space M N pointed-map-hom-H-Space + preserves-mul-hom-H-Space = + pr1 preserves-unital-mul-hom-H-Space + + preserves-left-unit-law-mul-hom-H-Space : + preserves-left-unit-law-mul-pointed-map-H-Space M N + ( pointed-map-hom-H-Space) + ( preserves-mul-hom-H-Space) + preserves-left-unit-law-mul-hom-H-Space = + pr1 (pr2 preserves-unital-mul-hom-H-Space) + + preserves-right-unit-law-mul-hom-H-Space : + preserves-right-unit-law-mul-pointed-map-H-Space M N + ( pointed-map-hom-H-Space) + ( preserves-mul-hom-H-Space) + preserves-right-unit-law-mul-hom-H-Space = + pr1 (pr2 (pr2 preserves-unital-mul-hom-H-Space)) + + preserves-coherence-unit-laws-mul-hom-H-Space : + preserves-coherence-unit-laws-mul-pointed-map-H-Space M N + ( pointed-map-hom-H-Space) + ( preserves-mul-hom-H-Space) + ( preserves-left-unit-law-mul-hom-H-Space) + ( preserves-right-unit-law-mul-hom-H-Space) + preserves-coherence-unit-laws-mul-hom-H-Space = + pr2 (pr2 (pr2 preserves-unital-mul-hom-H-Space)) ``` ### Homotopies of morphisms of H-spaces diff --git a/src/structured-types/morphisms-wild-monoids.lagda.md b/src/structured-types/morphisms-wild-monoids.lagda.md index 3253476d66..93df4f6dd1 100644 --- a/src/structured-types/morphisms-wild-monoids.lagda.md +++ b/src/structured-types/morphisms-wild-monoids.lagda.md @@ -59,53 +59,47 @@ module _ preserves-unital-mul-map-hom-Wild-Monoid : (f : hom-Wild-Monoid) → - preserves-unital-mul + preserves-unital-mul-pointed-map-H-Space ( h-space-Wild-Monoid M) ( h-space-Wild-Monoid N) ( pointed-map-hom-Wild-Monoid f) preserves-unital-mul-map-hom-Wild-Monoid f = pr2 f - preserves-mul-map-hom-Wild-Monoid : + preserves-mul-hom-Wild-Monoid : (f : hom-Wild-Monoid) → preserves-mul ( mul-Wild-Monoid M) ( mul-Wild-Monoid N) ( map-hom-Wild-Monoid f) - preserves-mul-map-hom-Wild-Monoid f = pr1 (pr2 f) + preserves-mul-hom-Wild-Monoid f = pr1 (pr2 f) preserves-left-unit-law-mul-map-hom-Wild-Monoid : ( f : hom-Wild-Monoid) → - preserves-left-unit-law-mul - ( mul-Wild-Monoid M) - ( left-unit-law-mul-Wild-Monoid M) - ( mul-Wild-Monoid N) - ( left-unit-law-mul-Wild-Monoid N) - ( map-hom-Wild-Monoid f) - ( preserves-unit-map-hom-Wild-Monoid f) - ( preserves-mul-map-hom-Wild-Monoid f) + preserves-left-unit-law-mul-pointed-map-H-Space + ( h-space-Wild-Monoid M) + ( h-space-Wild-Monoid N) + ( pointed-map-hom-Wild-Monoid f) + ( preserves-mul-hom-Wild-Monoid f) preserves-left-unit-law-mul-map-hom-Wild-Monoid f = pr1 (pr2 (pr2 f)) preserves-right-unit-law-mul-map-hom-Wild-Monoid : (f : hom-Wild-Monoid) → - preserves-right-unit-law-mul - ( mul-Wild-Monoid M) - ( right-unit-law-mul-Wild-Monoid M) - ( mul-Wild-Monoid N) - ( right-unit-law-mul-Wild-Monoid N) - ( map-hom-Wild-Monoid f) - ( preserves-unit-map-hom-Wild-Monoid f) - ( preserves-mul-map-hom-Wild-Monoid f) + preserves-right-unit-law-mul-pointed-map-H-Space + ( h-space-Wild-Monoid M) + ( h-space-Wild-Monoid N) + ( pointed-map-hom-Wild-Monoid f) + ( preserves-mul-hom-Wild-Monoid f) preserves-right-unit-law-mul-map-hom-Wild-Monoid f = pr1 (pr2 (pr2 (pr2 f))) preserves-coh-unit-laws-map-hom-Wild-Monoid : (f : hom-Wild-Monoid) → - preserves-coh-unit-laws-mul + preserves-coherence-unit-laws-mul-pointed-map-H-Space ( h-space-Wild-Monoid M) ( h-space-Wild-Monoid N) ( pointed-map-hom-Wild-Monoid f) - ( preserves-mul-map-hom-Wild-Monoid f) + ( preserves-mul-hom-Wild-Monoid f) ( preserves-left-unit-law-mul-map-hom-Wild-Monoid f) ( preserves-right-unit-law-mul-map-hom-Wild-Monoid f) preserves-coh-unit-laws-map-hom-Wild-Monoid f = diff --git a/src/structured-types/pointed-equivalences.lagda.md b/src/structured-types/pointed-equivalences.lagda.md index 0ec64334e1..0a852924d2 100644 --- a/src/structured-types/pointed-equivalences.lagda.md +++ b/src/structured-types/pointed-equivalences.lagda.md @@ -8,11 +8,13 @@ module structured-types.pointed-equivalences where ```agda open import foundation.action-on-identifications-functions +open import foundation.binary-equivalences open import foundation.cartesian-product-types open import foundation.commuting-squares-of-identifications open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types +open import foundation.embeddings open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-extensionality @@ -339,6 +341,32 @@ module _ ( pointed-map-pointed-equiv e) ``` +### Inverses of pointed equivalences + +```agda +module _ + {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} + (e : A ≃∗ B) + where + + abstract + is-pointed-equiv-inv-pointed-equiv : + is-pointed-equiv (pointed-map-inv-pointed-equiv e) + is-pointed-equiv-inv-pointed-equiv = + is-equiv-is-invertible + ( map-pointed-equiv e) + ( is-retraction-map-inv-pointed-equiv e) + ( is-section-map-inv-pointed-equiv e) + + equiv-inv-pointed-equiv : type-Pointed-Type B ≃ type-Pointed-Type A + pr1 equiv-inv-pointed-equiv = map-inv-pointed-equiv e + pr2 equiv-inv-pointed-equiv = is-pointed-equiv-inv-pointed-equiv + + inv-pointed-equiv : B ≃∗ A + pr1 inv-pointed-equiv = equiv-inv-pointed-equiv + pr2 inv-pointed-equiv = preserves-point-map-inv-pointed-equiv e +``` + ## Properties ### Extensionality of the universe of pointed types @@ -348,13 +376,14 @@ module _ {l1 : Level} (A : Pointed-Type l1) where - is-torsorial-equiv-Pointed-Type : - is-torsorial (λ B → A ≃∗ B) - is-torsorial-equiv-Pointed-Type = - is-torsorial-Eq-structure - ( is-torsorial-equiv (type-Pointed-Type A)) - ( type-Pointed-Type A , id-equiv) - ( is-torsorial-Id (point-Pointed-Type A)) + abstract + is-torsorial-pointed-equiv : + is-torsorial (λ (B : Pointed-Type l1) → A ≃∗ B) + is-torsorial-pointed-equiv = + is-torsorial-Eq-structure + ( is-torsorial-equiv (type-Pointed-Type A)) + ( type-Pointed-Type A , id-equiv) + ( is-torsorial-Id (point-Pointed-Type A)) extensionality-Pointed-Type : (B : Pointed-Type l1) → (A ＝ B) ≃ (A ≃∗ B) extensionality-Pointed-Type = @@ -441,12 +470,13 @@ module _ htpy-pointed-htpy ( is-pointed-section-pointed-map-inv-is-pointed-equiv-universal-property-pointed-equiv) - is-pointed-equiv-universal-property-pointed-equiv : is-pointed-equiv f - is-pointed-equiv-universal-property-pointed-equiv = - is-equiv-is-invertible - ( map-inv-is-pointed-equiv-universal-property-pointed-equiv) - ( is-section-map-inv-is-pointed-equiv-universal-property-pointed-equiv) - ( is-retraction-map-inv-is-pointed-equiv-universal-property-pointed-equiv) + abstract + is-pointed-equiv-universal-property-pointed-equiv : is-pointed-equiv f + is-pointed-equiv-universal-property-pointed-equiv = + is-equiv-is-invertible + ( map-inv-is-pointed-equiv-universal-property-pointed-equiv) + ( is-section-map-inv-is-pointed-equiv-universal-property-pointed-equiv) + ( is-retraction-map-inv-is-pointed-equiv-universal-property-pointed-equiv) ``` ### Any pointed equivalence satisfies the universal property of pointed equivalences @@ -528,13 +558,14 @@ module _ ( H) ( C) - universal-property-pointed-equiv-is-pointed-equiv : - is-pointed-equiv f → - universal-property-pointed-equiv f - pr1 (universal-property-pointed-equiv-is-pointed-equiv H C) = - section-universal-property-pointed-equiv-is-pointed-equiv H C - pr2 (universal-property-pointed-equiv-is-pointed-equiv H C) = - retraction-universal-property-pointed-equiv-is-pointed-equiv H C + abstract + universal-property-pointed-equiv-is-pointed-equiv : + is-pointed-equiv f → + universal-property-pointed-equiv f + pr1 (universal-property-pointed-equiv-is-pointed-equiv H C) = + section-universal-property-pointed-equiv-is-pointed-equiv H C + pr2 (universal-property-pointed-equiv-is-pointed-equiv H C) = + retraction-universal-property-pointed-equiv-is-pointed-equiv H C equiv-precomp-pointed-map : {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} @@ -631,12 +662,13 @@ module _ htpy-pointed-htpy ( is-pointed-retraction-pointed-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) - is-pointed-equiv-is-equiv-postcomp-pointed-map : is-pointed-equiv f - is-pointed-equiv-is-equiv-postcomp-pointed-map = - is-equiv-is-invertible - ( map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) - ( is-section-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) - ( is-retraction-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) + abstract + is-pointed-equiv-is-equiv-postcomp-pointed-map : is-pointed-equiv f + is-pointed-equiv-is-equiv-postcomp-pointed-map = + is-equiv-is-invertible + ( map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) + ( is-section-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) + ( is-retraction-map-inv-is-pointed-equiv-is-equiv-postcomp-pointed-map) ``` #### Any pointed equivalence is an equivalence by postcomposition @@ -695,10 +727,69 @@ module _ ( h)) ( left-unit-law-comp-pointed-map h))) - is-equiv-postcomp-is-pointed-equiv : is-equiv-postcomp-pointed-map f - is-equiv-postcomp-is-pointed-equiv X = - is-equiv-is-invertible - ( map-inv-is-equiv-postcomp-is-pointed-equiv X) - ( is-section-map-inv-is-equiv-postcomp-is-pointed-equiv X) - ( is-retraction-map-inv-is-equiv-postcomp-is-pointed-equiv X) + abstract + is-equiv-postcomp-is-pointed-equiv : is-equiv-postcomp-pointed-map f + is-equiv-postcomp-is-pointed-equiv X = + is-equiv-is-invertible + ( map-inv-is-equiv-postcomp-is-pointed-equiv X) + ( is-section-map-inv-is-equiv-postcomp-is-pointed-equiv X) + ( is-retraction-map-inv-is-equiv-postcomp-is-pointed-equiv X) + +equiv-postcomp-pointed-map : + {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} + (C : Pointed-Type l3) → (A ≃∗ B) → (C →∗ A) ≃ (C →∗ B) +pr1 (equiv-postcomp-pointed-map C e) = + postcomp-pointed-map (pointed-map-pointed-equiv e) C +pr2 (equiv-postcomp-pointed-map C e) = + is-equiv-postcomp-is-pointed-equiv + ( pointed-map-pointed-equiv e) + ( is-pointed-equiv-pointed-equiv e) + ( C) +``` + +### The composition operation on pointed equivalences is a binary equivalence + +```agda +module _ + {l1 l2 l3 : Level} + {A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3} + where + + abstract + is-equiv-comp-pointed-equiv : + (f : B ≃∗ C) → is-equiv (λ (e : A ≃∗ B) → comp-pointed-equiv f e) + is-equiv-comp-pointed-equiv f = + is-equiv-map-Σ _ + ( is-equiv-postcomp-equiv-equiv (equiv-pointed-equiv f)) + ( λ e → + is-equiv-comp _ + ( ap (map-pointed-equiv f)) + ( is-emb-is-equiv (is-equiv-map-pointed-equiv f) _ _) + ( is-equiv-concat' _ (preserves-point-pointed-equiv f))) + + equiv-comp-pointed-equiv : (f : B ≃∗ C) → (A ≃∗ B) ≃ (A ≃∗ C) + pr1 (equiv-comp-pointed-equiv f) = comp-pointed-equiv f + pr2 (equiv-comp-pointed-equiv f) = is-equiv-comp-pointed-equiv f + + abstract + is-equiv-comp-pointed-equiv' : + (e : A ≃∗ B) → is-equiv (λ (f : B ≃∗ C) → comp-pointed-equiv f e) + is-equiv-comp-pointed-equiv' e = + is-equiv-map-Σ _ + ( is-equiv-precomp-equiv-equiv (equiv-pointed-equiv e)) + ( λ f → + is-equiv-concat + ( ap (map-equiv f) (preserves-point-pointed-equiv e)) + ( _)) + + equiv-comp-pointed-equiv' : + (e : A ≃∗ B) → (B ≃∗ C) ≃ (A ≃∗ C) + pr1 (equiv-comp-pointed-equiv' e) f = comp-pointed-equiv f e + pr2 (equiv-comp-pointed-equiv' e) = is-equiv-comp-pointed-equiv' e + + abstract + is-binary-equiv-comp-pointed-equiv : + is-binary-equiv (λ (f : B ≃∗ C) (e : A ≃∗ B) → comp-pointed-equiv f e) + pr1 is-binary-equiv-comp-pointed-equiv = is-equiv-comp-pointed-equiv' + pr2 is-binary-equiv-comp-pointed-equiv = is-equiv-comp-pointed-equiv ``` diff --git a/src/structured-types/small-pointed-types.lagda.md b/src/structured-types/small-pointed-types.lagda.md new file mode 100644 index 0000000000..11bbfa1986 --- /dev/null +++ b/src/structured-types/small-pointed-types.lagda.md @@ -0,0 +1,156 @@ +# Small pointed types + +```agda +module structured-types.small-pointed-types where +``` + +
Imports + +```agda +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.functoriality-dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.small-types +open import foundation.universe-levels + +open import structured-types.pointed-equivalences +open import structured-types.pointed-types +``` + +
+ +## Idea + +A [pointed type](structured-types.pointed-types.md) is said to be +{{#concept "small" Disambiguation="pointed type" Agda=is-small-Pointed-Type}} is +its underlying type is [small](foundation.small-types.md). Equivalently, we say +that a pointed type is +{{#concept "pointed small" Agda=is-pointed-small-Pointed-Type}} if it comes +equipped with an element of type + +```text + Σ (Y : Pointed-Type l), X ≃∗ Y +``` + +The difference between small pointed types and pointed small pointed types is +that the notion of small pointed type is unpointed, and therefore potentially +easier to establish. It is immediate that a pointed small type is small. For the +converse, note that if `X` is small, and `Y : 𝒰` comes equipped with an +[equivalence](foundation-core.equivalences.md) `e : type-Pointed-Type X ≃ Y`, +then we take `e * : Y` to be the base point, and it is immediate that `e` is a +[pointed equivalence](structured-types.pointed-equivalences.md). + +## Definitions + +### Small pointed types + +```agda +module _ + {l1 : Level} (l2 : Level) (X : Pointed-Type l1) + where + + is-small-prop-Pointed-Type : Prop (l1 ⊔ lsuc l2) + is-small-prop-Pointed-Type = is-small-Prop l2 (type-Pointed-Type X) + + is-small-Pointed-Type : UU (l1 ⊔ lsuc l2) + is-small-Pointed-Type = is-small l2 (type-Pointed-Type X) + + is-prop-is-small-Pointed-Type : is-prop is-small-Pointed-Type + is-prop-is-small-Pointed-Type = is-prop-is-small l2 (type-Pointed-Type X) +``` + +### Pointedly small types + +```agda +module _ + {l1 : Level} (l2 : Level) (X : Pointed-Type l1) + where + + is-pointed-small-Pointed-Type : UU (l1 ⊔ lsuc l2) + is-pointed-small-Pointed-Type = + Σ (Pointed-Type l2) (λ Y → X ≃∗ Y) + +module _ + {l1 l2 : Level} (X : Pointed-Type l1) + (H : is-pointed-small-Pointed-Type l2 X) + where + + pointed-type-is-pointed-small-Pointed-Type : Pointed-Type l2 + pointed-type-is-pointed-small-Pointed-Type = pr1 H + + type-is-pointed-small-Pointed-Type : UU l2 + type-is-pointed-small-Pointed-Type = + type-Pointed-Type pointed-type-is-pointed-small-Pointed-Type + + point-is-pointed-small-Pointed-Type : + type-is-pointed-small-Pointed-Type + point-is-pointed-small-Pointed-Type = + point-Pointed-Type pointed-type-is-pointed-small-Pointed-Type + + pointed-equiv-is-pointed-small-Pointed-Type : + X ≃∗ pointed-type-is-pointed-small-Pointed-Type + pointed-equiv-is-pointed-small-Pointed-Type = pr2 H + + equiv-is-pointed-small-Pointed-Type : + type-Pointed-Type X ≃ type-is-pointed-small-Pointed-Type + equiv-is-pointed-small-Pointed-Type = + equiv-pointed-equiv pointed-equiv-is-pointed-small-Pointed-Type +``` + +## Properties + +### Being pointed small is a property + +```agda +module _ + {l1 l2 : Level} (X : Pointed-Type l1) + where + + is-prop-is-pointed-small-Pointed-Type : + is-prop (is-pointed-small-Pointed-Type l2 X) + is-prop-is-pointed-small-Pointed-Type = + is-prop-is-inhabited + ( λ (Y , e) → + is-prop-equiv' + ( equiv-tot (λ Z → equiv-comp-pointed-equiv' e)) + ( is-prop-is-contr (is-torsorial-pointed-equiv Y))) + +module _ + {l1 : Level} (l2 : Level) (X : Pointed-Type l1) + where + + is-pointed-small-prop-Pointed-Type : Prop (l1 ⊔ lsuc l2) + pr1 is-pointed-small-prop-Pointed-Type = + is-pointed-small-Pointed-Type l2 X + pr2 is-pointed-small-prop-Pointed-Type = + is-prop-is-pointed-small-Pointed-Type X +``` + +### A pointed type is small if and only if it is pointed small + +```agda +module _ + {l1 l2 : Level} (X : Pointed-Type l1) + where + + is-pointed-small-is-small-Pointed-Type : + is-small-Pointed-Type l2 X → is-pointed-small-Pointed-Type l2 X + pr1 (pr1 (is-pointed-small-is-small-Pointed-Type (Y , e))) = + Y + pr2 (pr1 (is-pointed-small-is-small-Pointed-Type (Y , e))) = + map-equiv e (point-Pointed-Type X) + pr1 (pr2 (is-pointed-small-is-small-Pointed-Type (Y , e))) = + e + pr2 (pr2 (is-pointed-small-is-small-Pointed-Type (Y , e))) = + refl + + is-small-is-pointed-small-Pointed-Type : + is-pointed-small-Pointed-Type l2 X → is-small-Pointed-Type l2 X + pr1 (is-small-is-pointed-small-Pointed-Type (Y , e)) = + type-Pointed-Type Y + pr2 (is-small-is-pointed-small-Pointed-Type (Y , e)) = + equiv-pointed-equiv e +``` diff --git a/src/synthetic-homotopy-theory/iterated-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/iterated-loop-spaces.lagda.md index b6d2d3f159..4a08e286e5 100644 --- a/src/synthetic-homotopy-theory/iterated-loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/iterated-loop-spaces.lagda.md @@ -12,6 +12,7 @@ open import elementary-number-theory.natural-numbers open import foundation.iterating-functions open import foundation.universe-levels +open import structured-types.h-spaces open import structured-types.pointed-types open import synthetic-homotopy-theory.loop-spaces @@ -27,6 +28,10 @@ An **iterated loop space** `Ωⁿ A` is the [loop space](synthetic-homotopy-theory.loop-spaces.md) functor `Ω : Pointed-Type → Pointed-Type`. +## Definitions + +### Iterated loop spaces + ```agda module _ {l : Level} @@ -36,6 +41,19 @@ module _ iterated-loop-space n = iterate n Ω ``` +### Iterated loop spaces of H-spaces + +```agda +module _ + {l : Level} + where + + iterated-loop-space-H-Space : ℕ → H-Space l → H-Space l + iterated-loop-space-H-Space zero-ℕ X = X + iterated-loop-space-H-Space (succ-ℕ n) X = + Ω-H-Space (iterated-loop-space n (pointed-type-H-Space X)) +``` + ## See also - [Double loop spaces](synthetic-homotopy-theory.double-loop-spaces.md) diff --git a/src/synthetic-homotopy-theory/loop-spaces.lagda.md b/src/synthetic-homotopy-theory/loop-spaces.lagda.md index 588e0065da..d150a83996 100644 --- a/src/synthetic-homotopy-theory/loop-spaces.lagda.md +++ b/src/synthetic-homotopy-theory/loop-spaces.lagda.md @@ -73,20 +73,22 @@ module _ {l : Level} (A : Pointed-Type l) where - left-unit-law-mul-Ω : - (x : type-Ω A) → Id (mul-Ω A (refl-Ω A) x) x + left-unit-law-mul-Ω : (x : type-Ω A) → mul-Ω A (refl-Ω A) x ＝ x left-unit-law-mul-Ω x = left-unit - right-unit-law-mul-Ω : - (x : type-Ω A) → Id (mul-Ω A x (refl-Ω A)) x + right-unit-law-mul-Ω : (x : type-Ω A) → mul-Ω A x (refl-Ω A) ＝ x right-unit-law-mul-Ω x = right-unit + coherence-unit-laws-mul-Ω : + left-unit-law-mul-Ω refl ＝ right-unit-law-mul-Ω refl + coherence-unit-laws-mul-Ω = refl + Ω-H-Space : H-Space l pr1 Ω-H-Space = Ω A pr1 (pr2 Ω-H-Space) = mul-Ω A pr1 (pr2 (pr2 Ω-H-Space)) = left-unit-law-mul-Ω pr1 (pr2 (pr2 (pr2 Ω-H-Space))) = right-unit-law-mul-Ω - pr2 (pr2 (pr2 (pr2 Ω-H-Space))) = refl + pr2 (pr2 (pr2 (pr2 Ω-H-Space))) = coherence-unit-laws-mul-Ω ``` ### The wild quasigroup of loops on a pointed space