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

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

@@ -0,0 +1,70 @@
+# 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
+
+Any map `f : A → B` is said to be a `0`-coherent equivalence.
+Furthermore, a map `f : A → B` is said to be a `n + 1`-coherent equivalence 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 an `n`-coherent equivalence.
+
+A `1`-coherent equivalence is therefore a map equipped with a [retraction](foundation-core.retractions.md). 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 equivalent 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-coherent-equivalence
+    {l1 l2 : Level}  {A : UU l1} {B : UU l2} :
+    (n : ℕ) (f : A → B) → UU (lsuc l1 ⊔ lsuc l2)
+  where
+  is-zero-coherent-equivalence :
+    (f : A → B) → is-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-coherent-equivalence n (H x y)) →
+    is-coherent-equivalence (succ-ℕ n) f
+```

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

@@ -0,0 +1,75 @@
+# 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
+
+Any map `f : A → B` is said to be `0`-coherently invertible if it comes equipped with a map `g : B → A`
+Furthermore, a map `f : A → B` is said to be `n + 1`-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 [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 (lsuc l1 ⊔ lsuc 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
+```