Merge branch 'master' into optimizations

.github/workflows/profiling.yaml

@@ -67,12 +67,14 @@ 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:
+          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

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
 

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/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
 

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](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
+```

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
+```