This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Finitely coherently invertible maps

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

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

Idea

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

Definitions

The predicate of being an n-coherently invertible map

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