Infinitely and finitely coherent equivalences and infinitely and finitely coherently invertible maps

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

src/foundation/finitely-coherent-equivalences.lagda.md

@@ -0,0 +1,86 @@
+# Finitely coherent equivalences
+
+```agda
+module foundation.finitely-coherent-equivalences where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.identity-types
+open import foundation.unit-type
+open import foundation.universe-levels
+```
+
+</details>
+
+## 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](foundeation-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
+```

src/foundation/finitely-coherently-invertible-maps.lagda.md

@@ -0,0 +1,91 @@
+# Finitely coherently invertible maps
+
+```agda
+module foundation.finitely-coherently-invertible-maps where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.identity-types
+open import foundation.unit-type
+open import foundation.universe-levels
+```
+
+</details>
+
+## 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
+```