Finitely coherent equivalences

Content created by Egbert Rijke and maybemabeline.

Created on 2024-02-23.
Last modified on 2024-02-23.

module foundation.finitely-coherent-equivalences where
open import elementary-number-theory.natural-numbers

open import foundation.identity-types
open import foundation.unit-type
open import foundation.universe-levels


The condition of being a finitely coherent equivalence is introduced by induction on the natural numbers. In the base case, we say that any map f : A → B is a 0-coherent equivalence. Recursively, we say that a map f : A → B is an n + 1-coherent equivalence if it comes equipped with a map g : B → A and a family of maps

  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 and transposition operations of identifications 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

  s x y : (x = g y) → (f x = y)

and for each p : f x = y and q : x = g y a map

  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

  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 for each n ≥ 2, and this proposition is equivalent to being an equivalence.


The predicate of being an n-coherent equivalence

    {l1 l2 : Level} {A : UU l1} {B : UU l2} :
    (n : ) (f : A  B)  UU (l1  l2)
  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

Recent changes