Finitely coherently invertible maps

Content created by Egbert Rijke and maybemabeline.

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

module foundation.finitely-coherently-invertible-maps where
open import elementary-number-theory.natural-numbers

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


We introduce the concept of being a finitely coherently invertible map by induction on the natural numbers. In the base case, we say that a map f : A → B is a 0-coherently invertible map if it comes equipped with a map g : B → A. Recursively, we say that a map f : A → B is an n + 1-coherently invertible map if it comes equipped with 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 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 and a section of f. In other words, a 1-coherently invertible map is just an invertible map.

A 2-coherently invertible map f : A → B comes equipped with g : B → A and for each x : A and y : B two maps

  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

  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

  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 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 𝒰.


The predicate of being an n-coherently invertible map

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

Recent changes