From 18bc065f458e2182eef9b0616698b6d7ceffafa0 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Fri, 23 Feb 2024 11:43:06 +0100 Subject: [PATCH 1/4] Infinitely and finitely coherent equivalences and infinitely and finitely coherently invertible maps (#1028) This PR is part of the diploma project of @maybemabeline. We add some new definitions to the library, and we found some ways to express infinite coherence. --------- Co-authored-by: maybemabeline --- src/foundation-core/equivalences.lagda.md | 6 + src/foundation.lagda.md | 9 + src/foundation/equivalences.lagda.md | 6 + .../finitely-coherent-equivalences.lagda.md | 86 +++++ ...nitely-coherently-invertible-maps.lagda.md | 91 +++++ .../infinitely-coherent-equivalences.lagda.md | 362 ++++++++++++++++++ src/foundation/retractions.lagda.md | 58 --- src/foundation/sections.lagda.md | 57 --- ...tal-concatenation-identifications.lagda.md | 6 +- ...dentifications-along-equivalences.lagda.md | 4 + ...identifications-along-retractions.lagda.md | 111 ++++++ ...on-identifications-along-sections.lagda.md | 109 ++++++ src/group-theory/conjugation.lagda.md | 10 +- 13 files changed, 793 insertions(+), 122 deletions(-) create mode 100644 src/foundation/finitely-coherent-equivalences.lagda.md create mode 100644 src/foundation/finitely-coherently-invertible-maps.lagda.md create mode 100644 src/foundation/infinitely-coherent-equivalences.lagda.md create mode 100644 src/foundation/transposition-identifications-along-retractions.lagda.md create mode 100644 src/foundation/transposition-identifications-along-sections.lagda.md diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index 843b2ae090..7cbf23c397 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/src/foundation-core/equivalences.lagda.md @@ -748,6 +748,12 @@ syntax step-equivalence-reasoning e Z f = e ≃ Z by f [`foundation.contractible-maps`](foundation.contractible-maps.md). - For the notion of path-split maps see [`foundation.path-split-maps`](foundation.path-split-maps.md). +- For the notion of finitely coherent equivalence, see + [`foundation.finitely-coherent-equivalence`)(foundation.finitely-coherent-equivalence.md). +- For the notion of finitely coherently invertible map, see + [`foundation.finitely-coherently-invertible-map`)(foundation.finitely-coherently-invertible-map.md). +- For the notion of infinitely coherent equivalence, see + [`foundation.infinitely-coherent-equivalences`](foundation.infinitely-coherent-equivalences.md). ### Table of files about function types, composition, and equivalences diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 00cfe1d5a0..827eff16f9 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -1,5 +1,9 @@ # Foundation +```agda +{-# OPTIONS --guardedness #-} +``` + ## Files in the foundation folder ```agda @@ -161,6 +165,8 @@ open import foundation.fibered-equivalences public open import foundation.fibered-involutions public 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.full-subtypes public open import foundation.function-extensionality public open import foundation.function-types public @@ -195,6 +201,7 @@ open import foundation.implicit-function-types public open import foundation.impredicative-encodings public open import foundation.impredicative-universes public open import foundation.induction-principle-propositional-truncation public +open import foundation.infinitely-coherent-equivalences public open import foundation.inhabited-subtypes public open import foundation.inhabited-types public open import foundation.injective-maps public @@ -363,6 +370,8 @@ open import foundation.transport-along-homotopies public open import foundation.transport-along-identifications public open import foundation.transport-split-type-families public open import foundation.transposition-identifications-along-equivalences public +open import foundation.transposition-identifications-along-retractions public +open import foundation.transposition-identifications-along-sections public open import foundation.transposition-span-diagrams public open import foundation.trivial-relaxed-sigma-decompositions public open import foundation.trivial-sigma-decompositions public diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md index 9ebb42a77a..e589682754 100644 --- a/src/foundation/equivalences.lagda.md +++ b/src/foundation/equivalences.lagda.md @@ -615,6 +615,12 @@ module _ [`foundation.contractible-maps`](foundation.contractible-maps.md). - For the notion of path-split maps see [`foundation.path-split-maps`](foundation.path-split-maps.md). +- For the notion of finitely coherent equivalence, see + [`foundation.finitely-coherent-equivalence`)(foundation.finitely-coherent-equivalence.md). +- For the notion of finitely coherently invertible map, see + [`foundation.finitely-coherently-invertible-map`)(foundation.finitely-coherently-invertible-map.md). +- For the notion of infinitely coherent equivalence, see + [`foundation.infinitely-coherent-equivalences`](foundation.infinitely-coherent-equivalences.md). ### Table of files about function types, composition, and equivalences diff --git a/src/foundation/finitely-coherent-equivalences.lagda.md b/src/foundation/finitely-coherent-equivalences.lagda.md new file mode 100644 index 0000000000..ad8dcd5167 --- /dev/null +++ b/src/foundation/finitely-coherent-equivalences.lagda.md @@ -0,0 +1,86 @@ +# Finitely coherent equivalences + +```agda +module foundation.finitely-coherent-equivalences where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.identity-types +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +The condition of being a +{{#concept "finitely coherent equivalence" Agda=is-finitely-coherent-equivalence}} +is introduced by induction on the +[natural numbers](elementary-number-theory.natural-numbers.md). In the base +case, we say that any map `f : A → B` is a +{{#concept "`0`-coherent equivalence" Agda=is-finitely-coherent-equivalence}}. +Recursively, we say that a map `f : A → B` is an +{{#concept "`n + 1`-coherent equivalence" Agda=is-finitely-coherent-equivalence}} +if it comes equipped with a map `g : B → A` and a family of maps + +```text + r x y : (f x ＝ y) → (x ＝ g y) +``` + +indexed by `x : A` and `y : B`, such that each `r x y` is an `n`-coherent +equivalence. + +By the equivalence of [retracting homotopies](foundation-core.retractions.md) +and +[transposition operations of identifications](foundation.transposition-identifications-along-retractions.md) +it therefore follows that a `1`-coherent equivalence is equivalently described +as a map equipped with a retraction. A `2`-coherent equivalence is a map +`f : A → B` equipped with `g : B → A` and for each `x : A` and `y : B` a map +`r x y : (f x ＝ y) → (x ＝ g y)`, equipped with + +```text + s x y : (x ＝ g y) → (f x ＝ y) +``` + +and for each `p : f x ＝ y` and `q : x ＝ g y` a map + +```text + t p q : (r x y p ＝ q) → (p ＝ s x y q). +``` + +This data is equivalent to the data of a +[coherently invertible map](foundation-core.coherently-invertible-maps.md) + +```text + r : (x : A) → g (f x) ＝ x + s : (y : B) → f (g y) ＝ y + t : (x : A) → ap f (r x) ＝ s (f x). +``` + +The condition of being an `n`-coherent equivalence is a +[proposition](foundation-core.propositions.md) for each `n ≥ 2`, and this +proposition is equivalent to being an equivalence. + +## Definitions + +### The predicate of being an `n`-coherent equivalence + +```agda +data + is-finitely-coherent-equivalence + {l1 l2 : Level} {A : UU l1} {B : UU l2} : + (n : ℕ) (f : A → B) → UU (l1 ⊔ l2) + where + is-zero-coherent-equivalence : + (f : A → B) → is-finitely-coherent-equivalence 0 f + is-succ-coherent-equivalence : + (n : ℕ) + (f : A → B) (g : B → A) (H : (x : A) (y : B) → (f x ＝ y) → (x ＝ g y)) → + ((x : A) (y : B) → is-finitely-coherent-equivalence n (H x y)) → + is-finitely-coherent-equivalence (succ-ℕ n) f +``` diff --git a/src/foundation/finitely-coherently-invertible-maps.lagda.md b/src/foundation/finitely-coherently-invertible-maps.lagda.md new file mode 100644 index 0000000000..a48d827c1e --- /dev/null +++ b/src/foundation/finitely-coherently-invertible-maps.lagda.md @@ -0,0 +1,91 @@ +# Finitely coherently invertible maps + +```agda +module foundation.finitely-coherently-invertible-maps where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.identity-types +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +We introduce the concept of being a +{{#concept "finitely coherently invertible map" Agda=is-finitely-coherently-invertible}} +by induction on the +[natural numbers](elementary-number-theory.natural-numbers.md). In the base +case, we say that a map `f : A → B` is a +{{#concept "`0`-coherently invertible map" Agda=is-finitely-coherently-invertible}} +if it comes equipped with a map `g : B → A`. Recursively, we say that a map +`f : A → B` is an +{{#concept "`n + 1`-coherently invertible map" Agda=is-finitely-coherently-invertible}} +if it comes equipped with map `g : B → A` and a family of maps + +```text + r x y : (f x ＝ y) → (x ＝ g y) +``` + +indexed by `x : A` and `y : B`, such that each `r x y` is `n`-coherently +invertible. + +A `1`-coherently invertible map `f : A → B` is therefore equivalently described +as a map equipped with an inverse `g : B → A` which is simultaneously a +[retraction](foundation-core.retractions.md) and a +[section](foundation-core.sections.md) of `f`. In other words, a `1`-coherently +invertible map is just an [invertible map](foundation-core.invertible-maps.md). + +A `2`-coherently invertible map `f : A → B` comes equipped with `g : B → A` and +for each `x : A` and `y : B` two maps + +```text + r : (f x ＝ y) → (x ＝ g y) + s : (x ＝ g y) → (f x ＝ y) +``` + +and for each `p : f x ＝ y` and `q : x ＝ g y` a map + +```text + t p q : (r p ＝ q) → (p ＝ s q) + u p q : (p ＝ s q) → (r p ＝ q). +``` + +This data is equivalent to the data of + +```text + r : (x : A) → g (f x) ＝ x + s : (y : B) → f (g y) ＝ y + t : (x : A) → ap f (r x) ＝ s (f x) + u : (y : B) → ap g (s y) ＝ r (f y). +``` + +The condition of being a `n`-coherently invertible map is not a +[proposition](foundation-core.propositions.md) for any `n`. In fact, for `n ≥ 1` +the type of all `n`-coherently invertible maps in a universe `𝒰` is equivalent +to the type of maps `sphere (n + 1) → 𝒰` of `n + 1`-spheres in the universe `𝒰`. + +## Definitions + +### The predicate of being an `n`-coherently invertible map + +```agda +data + is-finitely-coherently-invertible + {l1 l2 : Level} {A : UU l1} {B : UU l2} : + (n : ℕ) (f : A → B) → UU (l1 ⊔ l2) + where + is-zero-coherently-invertible : + (f : A → B) → (B → A) → is-finitely-coherently-invertible 0 f + is-succ-coherently-invertible : + (n : ℕ) + (f : A → B) (g : B → A) (H : (x : A) (y : B) → (f x ＝ y) → (x ＝ g y)) → + ((x : A) (y : B) → is-finitely-coherently-invertible n (H x y)) → + is-finitely-coherently-invertible (succ-ℕ n) f +``` diff --git a/src/foundation/infinitely-coherent-equivalences.lagda.md b/src/foundation/infinitely-coherent-equivalences.lagda.md new file mode 100644 index 0000000000..a650beffa9 --- /dev/null +++ b/src/foundation/infinitely-coherent-equivalences.lagda.md @@ -0,0 +1,362 @@ +# Infinitely coherent equivalences + +```agda +{-# OPTIONS --guardedness --lossy-unification #-} + +module foundation.infinitely-coherent-equivalences where +``` + +
Imports + +```agda +open import foundation.commuting-triangles-of-maps +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.propositions +open import foundation.retractions +open import foundation.sections +open import foundation.transposition-identifications-along-equivalences +open import foundation.universe-levels +``` + +
+ +## Idea + +An {{#concept "infinitely coherent equivalence" Agda=_≃∞_}} `e : A ≃∞ B` from +`A` to `B` consists of maps + +```text + f : A → B + g : B → A +``` + +and for each `x : A` and `y : B` an infinitely coherent equivalence + +```text + ∞-equiv-transpose-eq-∞-equiv : (f x ＝ y) ≃∞ (x ＝ g y). +``` + +Since this definition is infinite, it follows that for any `x : A` and `y : B` +we have maps + +```text + f' : (f x ＝ y) → (x ＝ g y) + g' : (x ＝ g y) → (f x ＝ y) +``` + +and for each `p : f x ＝ y` and `q : g y ＝ x` an infinitely coherent +equivalence + +```text +∞-equiv-transpose-eq-∞-equiv : (f' p ＝ q) ≃∞ (p ＝ g' q). +``` + +In particular, we have identifications + +```text + inv (f' x (f x) refl) : x = g (f x) + g' y (g y) refl : f (g y) ＝ y, +``` + +which are the usual homotopies witnessing that `g` is a retraction and a section +of `f`. By infinitely imposing the structure of a coherent equivalence, we have +stated an infinite hierarchy of coherence conditions. In other words, the +infinite condition on infinitely coherent equivalences is a way of stating +infinite coherence for equivalences. + +Being an infinitely coherent equivalence is an inverse sequential limit of the +diagram + +```text + ... ---> is-finitely-coherent-equivalence 1 f ---> is-finitely-coherent-equivalence 0 f. +``` + +## Definitions + +### The predicate of being an infinitely coherent equivalence + +```agda +record is-∞-equiv + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) : UU (l1 ⊔ l2) + where + coinductive + field + map-inv-is-∞-equiv : B → A + map-transpose-is-∞-equiv : + (x : A) (y : B) → f x ＝ y → x ＝ map-inv-is-∞-equiv y + is-∞-equiv-map-transpose-is-∞-equiv : + (x : A) (y : B) → is-∞-equiv (map-transpose-is-∞-equiv x y) + +open is-∞-equiv public +``` + +### Infinitely coherent equivalences + +```agda +record + ∞-equiv + {l1 l2 : Level} (A : UU l1) (B : UU l2) : UU (l1 ⊔ l2) + where + coinductive + field + map-∞-equiv : A → B + map-inv-∞-equiv : B → A + ∞-equiv-transpose-eq-∞-equiv : + (x : A) (y : B) → ∞-equiv (map-∞-equiv x ＝ y) (x ＝ map-inv-∞-equiv y) + +open ∞-equiv public + +module _ + {l1 l2 : Level} (A : UU l1) (B : UU l2) + where + + infix 6 _≃∞_ + + _≃∞_ : UU (l1 ⊔ l2) + _≃∞_ = ∞-equiv A B + +∞-equiv-is-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} → is-∞-equiv f → A ≃∞ B +map-∞-equiv (∞-equiv-is-∞-equiv {f = f} H) = f +map-inv-∞-equiv (∞-equiv-is-∞-equiv H) = map-inv-is-∞-equiv H +∞-equiv-transpose-eq-∞-equiv (∞-equiv-is-∞-equiv H) x y = + ∞-equiv-is-∞-equiv (is-∞-equiv-map-transpose-is-∞-equiv H x y) + +map-transpose-eq-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃∞ B) → + (x : A) (y : B) → (map-∞-equiv e x ＝ y) → (x ＝ map-inv-∞-equiv e y) +map-transpose-eq-∞-equiv e x y = + map-∞-equiv (∞-equiv-transpose-eq-∞-equiv e x y) + +is-∞-equiv-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃∞ B) → + is-∞-equiv (map-∞-equiv e) +map-inv-is-∞-equiv (is-∞-equiv-∞-equiv e) = + map-inv-∞-equiv e +map-transpose-is-∞-equiv (is-∞-equiv-∞-equiv e) = + map-transpose-eq-∞-equiv e +is-∞-equiv-map-transpose-is-∞-equiv (is-∞-equiv-∞-equiv e) x y = + is-∞-equiv-∞-equiv (∞-equiv-transpose-eq-∞-equiv e x y) + +is-∞-equiv-map-transpose-eq-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃∞ B) (x : A) (y : B) → + is-∞-equiv (map-transpose-eq-∞-equiv e x y) +is-∞-equiv-map-transpose-eq-∞-equiv e x y = + is-∞-equiv-∞-equiv (∞-equiv-transpose-eq-∞-equiv e x y) +``` + +### Infinitely coherent identity equivalences + +```agda +is-∞-equiv-id : {l1 : Level} {A : UU l1} → is-∞-equiv (id {A = A}) +map-inv-is-∞-equiv is-∞-equiv-id = id +map-transpose-is-∞-equiv is-∞-equiv-id x y = id +is-∞-equiv-map-transpose-is-∞-equiv is-∞-equiv-id x y = is-∞-equiv-id + +id-∞-equiv : {l1 : Level} {A : UU l1} → A ≃∞ A +id-∞-equiv = ∞-equiv-is-∞-equiv is-∞-equiv-id +``` + +### Composition of infinitely coherent equivalences + +```agda +is-∞-equiv-comp : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} + {g : B → C} {f : A → B} + (G : is-∞-equiv g) + (F : is-∞-equiv f) → + is-∞-equiv (g ∘ f) +map-inv-is-∞-equiv (is-∞-equiv-comp G F) = + map-inv-is-∞-equiv F ∘ map-inv-is-∞-equiv G +map-transpose-is-∞-equiv (is-∞-equiv-comp G F) x z p = + map-transpose-is-∞-equiv F x _ (map-transpose-is-∞-equiv G _ z p) +is-∞-equiv-map-transpose-is-∞-equiv (is-∞-equiv-comp G F) x z = + is-∞-equiv-comp + ( is-∞-equiv-map-transpose-is-∞-equiv F x _) + ( is-∞-equiv-map-transpose-is-∞-equiv G _ z) + +comp-∞-equiv : + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} → + B ≃∞ C → A ≃∞ B → A ≃∞ C +comp-∞-equiv f e = + ∞-equiv-is-∞-equiv + ( is-∞-equiv-comp (is-∞-equiv-∞-equiv f) (is-∞-equiv-∞-equiv e)) +``` + +### Infinitely coherent equivalences obtained from equivalences + +Since +[transposing identifications along an equivalence](foundation.transposition-identifications-along-equivalences.md) +is an equivalence, it follows immediately that equivalences are infinitely +coherent equivalences. This argument does not require +[function extensionality](foundation.function-extensionality.md). + +```agda +is-∞-equiv-is-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} → + is-equiv f → is-∞-equiv f +map-inv-is-∞-equiv (is-∞-equiv-is-equiv H) = + map-inv-is-equiv H +map-transpose-is-∞-equiv (is-∞-equiv-is-equiv H) x y = + map-eq-transpose-equiv (_ , H) +is-∞-equiv-map-transpose-is-∞-equiv (is-∞-equiv-is-equiv H) x y = + is-∞-equiv-is-equiv (is-equiv-map-equiv (eq-transpose-equiv (_ , H) x y)) + +∞-equiv-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → A ≃ B → A ≃∞ B +∞-equiv-equiv e = + ∞-equiv-is-∞-equiv (is-∞-equiv-is-equiv (is-equiv-map-equiv e)) +``` + +## Properties + +### Any map homotopic to an infinitely coherent equivalence is an infinitely coherent equivalence + +```agda +is-∞-equiv-htpy : + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B} → + f ~ g → + is-∞-equiv f → is-∞-equiv g +map-inv-is-∞-equiv (is-∞-equiv-htpy H K) = + map-inv-is-∞-equiv K +map-transpose-is-∞-equiv (is-∞-equiv-htpy H K) x y = + map-transpose-is-∞-equiv K x y ∘ concat (H x) _ +is-∞-equiv-map-transpose-is-∞-equiv (is-∞-equiv-htpy H K) x y = + is-∞-equiv-comp + ( is-∞-equiv-map-transpose-is-∞-equiv K x y) + ( is-∞-equiv-is-equiv (is-equiv-concat (H x) _)) +``` + +### Homotopies of elements of type `is-∞-equiv f` + +Consider a map `f : A → B` and consider two elements + +```text + H K : is-∞-equiv f. +``` + +A {{#concept "homotopy of elments of type `is-∞-equiv`" Agda=htpy-is-∞-equiv}} +from `H := (h , s , H')` to `K := (k , t , K')` consists of a homotopy + +```text + α₀ : h ~ k, +``` + +for each `x : A` and `y : B` a homotopy `α₁` witnessing that the triangle + +```text + (f x = y) + / \ + s x y / \ t x y + / \ + ∨ ∨ + (x = h y) --------------> (x = k y) + p ↦ p ∙ α₀ y +``` + +commutes, and finally a homotopy of elements of type + +```text + is-infinitely-coherent-equivalence + ( is-∞-equiv-htpy α₁ + ( is-∞-equiv-comp + ( is-∞-equiv-is-equiv + ( is-equiv-concat' _ (α₀ y))) + ( H' x y)) + ( K' x y). +``` + +In other words, there are by the previous data two witnesses of the fact that +`t x y` is an infinitely coherent equivalence. The second (easiest) element is +the given element `K' x y`. The first element is from the homotopy witnessing +that the above triangle commutes. On the left we compose two infinitely coherent +equivalences, which results in an infinitely coherent equivalence, and the +element witnessing that the composite is an infinitely coherent equivalence +transports along the homotopy to a new element witnessing that `t x y` is an +infinitely coherent equivalence. + +```agda +record + htpy-is-∞-equiv + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + (H K : is-∞-equiv f) : UU (l1 ⊔ l2) + where + coinductive + field + htpy-map-inv-htpy-is-∞-equiv : + map-inv-is-∞-equiv H ~ map-inv-is-∞-equiv K + htpy-map-transpose-htpy-is-∞-equiv : + (x : A) (y : B) → + coherence-triangle-maps + ( map-transpose-is-∞-equiv K x y) + ( concat' _ (htpy-map-inv-htpy-is-∞-equiv y)) + ( map-transpose-is-∞-equiv H x y) + infinitely-htpy-htpy-is-∞-equiv : + (x : A) (y : B) → + htpy-is-∞-equiv + ( map-transpose-is-∞-equiv K x y) + ( is-∞-equiv-htpy + ( inv-htpy (htpy-map-transpose-htpy-is-∞-equiv x y)) + ( is-∞-equiv-comp + ( is-∞-equiv-is-equiv (is-equiv-concat' _ _)) + ( is-∞-equiv-map-transpose-is-∞-equiv H x y))) + ( is-∞-equiv-map-transpose-is-∞-equiv K x y) +``` + +### Being an infinitely coherent equivalence implies being an equivalence + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + is-equiv-is-∞-equiv : is-∞-equiv f → is-equiv f + is-equiv-is-∞-equiv H = + is-equiv-is-invertible + ( map-inv-is-∞-equiv H) + ( λ y → + map-inv-is-∞-equiv (is-∞-equiv-map-transpose-is-∞-equiv H _ y) refl) + ( λ x → inv (map-transpose-is-∞-equiv H x (f x) refl)) +``` + +### Computing the type `is-∞-equiv f` + +```agda +type-compute-is-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → UU (l1 ⊔ l2) +type-compute-is-∞-equiv {A = A} {B} f = + Σ (B → A) (λ g → (x : A) (y : B) → Σ ((f x ＝ y) → (x ＝ g y)) is-∞-equiv) + +map-compute-is-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → + type-compute-is-∞-equiv f → is-∞-equiv f +map-inv-is-∞-equiv (map-compute-is-∞-equiv f H) = + pr1 H +map-transpose-is-∞-equiv (map-compute-is-∞-equiv f H) x y = + pr1 (pr2 H x y) +is-∞-equiv-map-transpose-is-∞-equiv (map-compute-is-∞-equiv f H) x y = + pr2 (pr2 H x y) + +map-inv-compute-is-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → + is-∞-equiv f → type-compute-is-∞-equiv f +pr1 (map-inv-compute-is-∞-equiv f H) = + map-inv-is-∞-equiv H +pr1 (pr2 (map-inv-compute-is-∞-equiv f H) x y) = + map-transpose-is-∞-equiv H x y +pr2 (pr2 (map-inv-compute-is-∞-equiv f H) x y) = + is-∞-equiv-map-transpose-is-∞-equiv H x y +``` + +### Being an infinitely coherent equivalence is a property + +```text +is-prop-is-∞-equiv : + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) → + is-prop (is-∞-equiv f) +is-prop-is-∞-equiv = {!!} +``` diff --git a/src/foundation/retractions.lagda.md b/src/foundation/retractions.lagda.md index 3c51b23ceb..b412a82210 100644 --- a/src/foundation/retractions.lagda.md +++ b/src/foundation/retractions.lagda.md @@ -12,7 +12,6 @@ open import foundation-core.retractions public open import foundation.action-on-identifications-functions open import foundation.coslice open import foundation.dependent-pair-types -open import foundation.function-extensionality open import foundation.retracts-of-types open import foundation.universe-levels open import foundation.whiskering-homotopies-composition @@ -102,60 +101,3 @@ abstract retraction f → is-injective f is-injective-retraction f (h , H) {x} {y} p = inv (H x) ∙ (ap h p ∙ H y) ``` - -### Transposing identifications along retractions - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) - where - - transpose-eq-is-retraction : - g ∘ f ~ id → {x : B} {y : A} → x ＝ f y → g x ＝ y - transpose-eq-is-retraction H {x} {y} p = ap g p ∙ H y - - transpose-eq-is-retraction' : - g ∘ f ~ id → {x : A} {y : B} → f x ＝ y → x ＝ g y - transpose-eq-is-retraction' H {x} refl = inv (H x) - - is-retraction-transpose-eq : - ({x : B} {y : A} → x ＝ f y → g x ＝ y) → g ∘ f ~ id - is-retraction-transpose-eq H x = H refl - - is-retraction-transpose-eq' : - ({x : A} {y : B} → f x ＝ y → x ＝ g y) → g ∘ f ~ id - is-retraction-transpose-eq' H x = inv (H refl) - - is-retraction-is-retraction-transpose-eq : - is-retraction-transpose-eq ∘ transpose-eq-is-retraction ~ id - is-retraction-is-retraction-transpose-eq H = refl - - htpy-is-section-is-retraction-transpose-eq : - (H : {x : B} {y : A} → x ＝ f y → g x ＝ y) - (x : B) (y : A) → - transpose-eq-is-retraction (is-retraction-transpose-eq H) {x} {y} ~ - H {x} {y} - htpy-is-section-is-retraction-transpose-eq H x y refl = refl - - abstract - is-section-is-retraction-transpose-eq : - transpose-eq-is-retraction ∘ is-retraction-transpose-eq ~ id - is-section-is-retraction-transpose-eq H = - eq-htpy-implicit - ( λ x → - eq-htpy-implicit - ( λ y → eq-htpy (htpy-is-section-is-retraction-transpose-eq H x y))) - - is-equiv-transpose-eq-is-retraction : - is-equiv transpose-eq-is-retraction - is-equiv-transpose-eq-is-retraction = - is-equiv-is-invertible - ( is-retraction-transpose-eq) - ( is-section-is-retraction-transpose-eq) - ( is-retraction-is-retraction-transpose-eq) - - equiv-transpose-eq-is-retraction : - (g ∘ f ~ id) ≃ ({x : B} {y : A} → x ＝ f y → g x ＝ y) - equiv-transpose-eq-is-retraction = - (transpose-eq-is-retraction , is-equiv-transpose-eq-is-retraction) -``` diff --git a/src/foundation/sections.lagda.md b/src/foundation/sections.lagda.md index ca2ce02401..9a000d7e96 100644 --- a/src/foundation/sections.lagda.md +++ b/src/foundation/sections.lagda.md @@ -187,60 +187,3 @@ is-injective-map-section-family : is-injective (map-section-family b) is-injective-map-section-family b = ap pr1 ``` - -### Transposing identifications along sections - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) - where - - transpose-eq-is-section : - f ∘ g ~ id → {x : A} {y : B} → x ＝ g y → f x ＝ y - transpose-eq-is-section H {x} {y} p = ap f p ∙ H y - - transpose-eq-is-section' : - f ∘ g ~ id → {x : B} {y : A} → g x ＝ y → x ＝ f y - transpose-eq-is-section' H {x} refl = inv (H x) - - is-section-transpose-eq : - ({x : A} {y : B} → x ＝ g y → f x ＝ y) → f ∘ g ~ id - is-section-transpose-eq H x = H refl - - is-section-transpose-eq' : - ({x : B} {y : A} → g x ＝ y → x ＝ f y) → f ∘ g ~ id - is-section-transpose-eq' H x = inv (H refl) - - is-retraction-is-section-transpose-eq : - is-section-transpose-eq ∘ transpose-eq-is-section ~ id - is-retraction-is-section-transpose-eq H = refl - - htpy-is-section-is-section-transpose-eq : - (H : {x : A} {y : B} → x ＝ g y → f x ＝ y) → - (x : A) (y : B) → - transpose-eq-is-section (is-section-transpose-eq H) {x} {y} ~ H {x} {y} - htpy-is-section-is-section-transpose-eq H x y refl = refl - - abstract - is-section-is-section-transpose-eq : - transpose-eq-is-section ∘ is-section-transpose-eq ~ id - is-section-is-section-transpose-eq H = - eq-htpy-implicit - ( λ x → - eq-htpy-implicit - ( λ y → - eq-htpy (htpy-is-section-is-section-transpose-eq H x y))) - - is-equiv-transpose-eq-is-section : - is-equiv transpose-eq-is-section - is-equiv-transpose-eq-is-section = - is-equiv-is-invertible - ( is-section-transpose-eq) - ( is-section-is-section-transpose-eq) - ( is-retraction-is-section-transpose-eq) - - equiv-transpose-eq-is-section : - (f ∘ g ~ id) ≃ ({x : A} {y : B} → x ＝ g y → f x ＝ y) - equiv-transpose-eq-is-section = - (transpose-eq-is-section , is-equiv-transpose-eq-is-section) -``` diff --git a/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md b/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md index f3f4dce0d8..e28331de4b 100644 --- a/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md +++ b/src/foundation/strictly-right-unital-concatenation-identifications.lagda.md @@ -17,9 +17,9 @@ open import foundation-core.identity-types ## Idea -The -{{#concept "concatenation operation on identifications" Agda=_∙_ Agda=_∙'_ Agda=concat}} -is a family of binary operations +The concatenation operation on +[identifications](foundation-core.identity-types.md) is a family of binary +operations ```text _∙_ : x ＝ y → y ＝ z → x ＝ z diff --git a/src/foundation/transposition-identifications-along-equivalences.lagda.md b/src/foundation/transposition-identifications-along-equivalences.lagda.md index 2ed786e907..140374a3ff 100644 --- a/src/foundation/transposition-identifications-along-equivalences.lagda.md +++ b/src/foundation/transposition-identifications-along-equivalences.lagda.md @@ -109,6 +109,10 @@ It is sometimes useful to consider identifications `y ＝ e x` instead of `e x ＝ y`, so we include an inverted equivalence for that as well. ```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) + where + eq-transpose-equiv-inv : (x : A) (y : B) → (y ＝ map-equiv e x) ≃ (map-inv-equiv e y ＝ x) eq-transpose-equiv-inv x y = diff --git a/src/foundation/transposition-identifications-along-retractions.lagda.md b/src/foundation/transposition-identifications-along-retractions.lagda.md new file mode 100644 index 0000000000..2dfe11e3cb --- /dev/null +++ b/src/foundation/transposition-identifications-along-retractions.lagda.md @@ -0,0 +1,111 @@ +# Transposing identifications along retractions + +```agda +module foundation.transposition-identifications-along-retractions where +``` + +
+ +```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-core.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.retractions +``` + +
+ +## Idea + +Consider a map `f : A → B` and a map `g : B → A` in the converse direction. Then +there is an [equivalence](foundation-core.equivalences.md) + +```text + is-retraction f g ≃ ((x : A) (y : B) → (f x ＝ y) ≃ (x ＝ g y)) +``` + +In other words, any [retracting homotopy](foundation-core.retractions.md) +`g ∘ f ~ id` induces a unique family of +{{#concept "transposition" Disambiguation="identifications along retractions" Agda=eq-transpose-is-retraction}} +maps + +```text + f x ＝ y → x ＝ g y +``` + +indexed by `x : A` and `y : B`. + +## Definitions + +### Transposing identifications along retractions + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) + where + + eq-transpose-is-retraction : + is-retraction f g → {x : B} {y : A} → x ＝ f y → g x ＝ y + eq-transpose-is-retraction H {x} {y} p = ap g p ∙ H y + + eq-transpose-is-retraction' : + is-retraction f g → {x : A} {y : B} → f x ＝ y → x ＝ g y + eq-transpose-is-retraction' H {x} refl = inv (H x) +``` + +## Properties + +### The map that assings to each retracting homotopy a family of transposition functions of identifications is an equivalence + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) + where + + is-retraction-eq-transpose : + ({x : B} {y : A} → x ＝ f y → g x ＝ y) → is-retraction f g + is-retraction-eq-transpose H x = H refl + + is-retraction-eq-transpose' : + ({x : A} {y : B} → f x ＝ y → x ＝ g y) → is-retraction f g + is-retraction-eq-transpose' H x = inv (H refl) + + is-retraction-is-retraction-eq-transpose : + is-retraction-eq-transpose ∘ eq-transpose-is-retraction f g ~ id + is-retraction-is-retraction-eq-transpose H = refl + + htpy-is-section-is-retraction-eq-transpose : + (H : {x : B} {y : A} → x ＝ f y → g x ＝ y) + (x : B) (y : A) → + eq-transpose-is-retraction f g (is-retraction-eq-transpose H) {x} {y} ~ + H {x} {y} + htpy-is-section-is-retraction-eq-transpose H x y refl = refl + + abstract + is-section-is-retraction-eq-transpose : + eq-transpose-is-retraction f g ∘ is-retraction-eq-transpose ~ id + is-section-is-retraction-eq-transpose H = + eq-htpy-implicit + ( λ x → + eq-htpy-implicit + ( λ y → eq-htpy (htpy-is-section-is-retraction-eq-transpose H x y))) + + is-equiv-eq-transpose-is-retraction : + is-equiv (eq-transpose-is-retraction f g) + is-equiv-eq-transpose-is-retraction = + is-equiv-is-invertible + ( is-retraction-eq-transpose) + ( is-section-is-retraction-eq-transpose) + ( is-retraction-is-retraction-eq-transpose) + + equiv-eq-transpose-is-retraction : + is-retraction f g ≃ ({x : B} {y : A} → x ＝ f y → g x ＝ y) + equiv-eq-transpose-is-retraction = + ( eq-transpose-is-retraction f g , is-equiv-eq-transpose-is-retraction) +``` diff --git a/src/foundation/transposition-identifications-along-sections.lagda.md b/src/foundation/transposition-identifications-along-sections.lagda.md new file mode 100644 index 0000000000..9cffc6452a --- /dev/null +++ b/src/foundation/transposition-identifications-along-sections.lagda.md @@ -0,0 +1,109 @@ +# Transposing identifications along sections + +```agda +module foundation.transposition-identifications-along-sections where +``` + +
+ +```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-core.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.identity-types +open import foundation-core.sections +``` + +
+ +## Idea + +Consider a map `f : A → B` and a map `g : B → A` in the converse direction. Then +there is an [equivalence](foundation-core.equivalences.md) + +```text + is-section f g ≃ ((x : A) (y : B) → (x ＝ g y) ≃ (f x ＝ y)) +``` + +In other words, any [section homotopy](foundation-core.sections.md) `f ∘ g ~ id` +induces a unique family of +{{#concept "transposition" Disambiguation="identifications along sections" Agda=eq-transpose-is-section}} +maps + +```text + x ＝ g y → f x ＝ y +``` + +indexed by `x : A` and `y : B`. + +### Transposing identifications along sections + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) + where + + eq-transpose-is-section : + f ∘ g ~ id → {x : A} {y : B} → x ＝ g y → f x ＝ y + eq-transpose-is-section H {x} {y} p = ap f p ∙ H y + + eq-transpose-is-section' : + f ∘ g ~ id → {x : B} {y : A} → g x ＝ y → x ＝ f y + eq-transpose-is-section' H {x} refl = inv (H x) +``` + +## Properties + +### The map that assings to each section homotopy a family of transposition functions of identifications is an equivalence + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (g : B → A) + where + + is-section-eq-transpose : + ({x : A} {y : B} → x ＝ g y → f x ＝ y) → f ∘ g ~ id + is-section-eq-transpose H x = H refl + + is-section-eq-transpose' : + ({x : B} {y : A} → g x ＝ y → x ＝ f y) → f ∘ g ~ id + is-section-eq-transpose' H x = inv (H refl) + + is-retraction-is-section-eq-transpose : + is-section-eq-transpose ∘ eq-transpose-is-section f g ~ id + is-retraction-is-section-eq-transpose H = refl + + htpy-is-section-is-section-eq-transpose : + (H : {x : A} {y : B} → x ＝ g y → f x ＝ y) → + (x : A) (y : B) → + eq-transpose-is-section f g (is-section-eq-transpose H) {x} {y} ~ H {x} {y} + htpy-is-section-is-section-eq-transpose H x y refl = refl + + abstract + is-section-is-section-eq-transpose : + eq-transpose-is-section f g ∘ is-section-eq-transpose ~ id + is-section-is-section-eq-transpose H = + eq-htpy-implicit + ( λ x → + eq-htpy-implicit + ( λ y → + eq-htpy (htpy-is-section-is-section-eq-transpose H x y))) + + is-equiv-eq-transpose-is-section : + is-equiv (eq-transpose-is-section f g) + is-equiv-eq-transpose-is-section = + is-equiv-is-invertible + ( is-section-eq-transpose) + ( is-section-is-section-eq-transpose) + ( is-retraction-is-section-eq-transpose) + + equiv-eq-transpose-is-section : + (f ∘ g ~ id) ≃ ({x : A} {y : B} → x ＝ g y → f x ＝ y) + equiv-eq-transpose-is-section = + (eq-transpose-is-section f g , is-equiv-eq-transpose-is-section) +``` diff --git a/src/group-theory/conjugation.lagda.md b/src/group-theory/conjugation.lagda.md index 8ab1d3121c..e1534c847c 100644 --- a/src/group-theory/conjugation.lagda.md +++ b/src/group-theory/conjugation.lagda.md @@ -19,6 +19,8 @@ open import foundation.identity-types open import foundation.retractions open import foundation.sections open import foundation.subtypes +open import foundation.transposition-identifications-along-retractions +open import foundation.transposition-identifications-along-sections open import foundation.universe-levels open import group-theory.group-actions @@ -333,7 +335,7 @@ module _ {x y z : type-Group G} → y ＝ conjugation-Group G (inv-Group G x) z → conjugation-Group G x y ＝ z transpose-eq-conjugation-Group {x} {y} {z} = - transpose-eq-is-section + eq-transpose-is-section ( conjugation-Group G x) ( conjugation-Group G (inv-Group G x)) ( is-section-conjugation-inv-Group x) @@ -342,7 +344,7 @@ module _ {x y z : type-Group G} → conjugation-Group G (inv-Group G x) y ＝ z → y ＝ conjugation-Group G x z transpose-eq-conjugation-Group' {x} {y} {z} = - transpose-eq-is-section' + eq-transpose-is-section' ( conjugation-Group G x) ( conjugation-Group G (inv-Group G x)) ( is-section-conjugation-inv-Group x) @@ -351,7 +353,7 @@ module _ {x y z : type-Group G} → y ＝ conjugation-Group G x z → conjugation-Group G (inv-Group G x) y ＝ z transpose-eq-conjugation-inv-Group {x} {y} {z} = - transpose-eq-is-retraction + eq-transpose-is-retraction ( conjugation-Group G x) ( conjugation-Group G (inv-Group G x)) ( is-retraction-conjugation-inv-Group x) @@ -360,7 +362,7 @@ module _ {x y z : type-Group G} → conjugation-Group G x y ＝ z → y ＝ conjugation-Group G (inv-Group G x) z transpose-eq-conjugation-inv-Group' {x} {y} {z} = - transpose-eq-is-retraction' + eq-transpose-is-retraction' ( conjugation-Group G x) ( conjugation-Group G (inv-Group G x)) ( is-retraction-conjugation-inv-Group x) From b5ec17ab5587f14c3ce8656f9478bdfcb2c960f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20=C5=A0t=C4=9Bpan=C4=8D=C3=ADk?= Date: Tue, 27 Feb 2024 17:13:25 +0100 Subject: [PATCH 2/4] Add netlify environment variables to benchmark deployment action (#1044) This _should_ enable deployments of the benchmarking website --- .github/workflows/profiling.yaml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index 6f2beafcd0..5f265e1e34 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -74,5 +74,8 @@ jobs: echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json > benchmark-website/data.js - name: Deploy the new profiling website + env: + NETLIFY_SITE_ID: ${{ secrets.PERF_SITE_ID }} + NETLIFY_AUTH_TOKEN: ${{ secrets.PERF_SITE_KEY }} run: | - npx netlify-cli deploy --dir=benchmark-website + npx netlify-cli deploy --prod --dir=benchmark-website From d5f63de0ff6f01f6df97a4c1909aa1dd012f2553 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 27 Feb 2024 17:16:58 +0100 Subject: [PATCH 3/4] Track user analytics for website (#1035) This simple addition tracks some anonymous user data using GoatCounter. - [x] Create `agda-unimath` user at [GoatCounter](https://www.goatcounter.com/) - [x] Inject GoatCounter script Resolves #1029 --- theme/index.hbs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theme/index.hbs b/theme/index.hbs index 13935f31c1..fb365846a4 100644 --- a/theme/index.hbs +++ b/theme/index.hbs @@ -332,6 +332,8 @@ {{/if}} + + From b5985b52cb65fa9b2da4b961983ee1a1f5c4f6dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Vojt=C4=9Bch=20=C5=A0t=C4=9Bpan=C4=8D=C3=ADk?= Date: Tue, 27 Feb 2024 17:34:04 +0100 Subject: [PATCH 4/4] Fix benchmark deployment directory (#1045) --- .github/workflows/profiling.yaml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/profiling.yaml b/.github/workflows/profiling.yaml index 5f265e1e34..e153d46398 100644 --- a/.github/workflows/profiling.yaml +++ b/.github/workflows/profiling.yaml @@ -67,11 +67,10 @@ jobs: - name: Prepare new revision of the profiling website run: | - cd repo mkdir -p benchmark-website - cp website/benchmarks/index.html benchmark-website/ - cp ../benchmark-cache/data.* benchmark-website/ - echo 'window.BENCHMARK_DATA =' | cat - ../benchmark-cache/data.json > benchmark-website/data.js + cp repo/website/benchmarks/index.html benchmark-website/ + cp benchmark-cache/data.* benchmark-website/ + echo 'window.BENCHMARK_DATA =' | cat - benchmark-cache/data.json > benchmark-website/data.js - name: Deploy the new profiling website env: