# Finitely coherently invertible maps

Content created by Egbert Rijke and maybemabeline.

Created on 2024-02-23.

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