Contents
Definition
In set theory
Given sets and and a function , the inverse function of (if it exists) is the function such that both composite functions and are identity functions. Note that has an inverse function if and only if is a bijection, in which case this inverse function is unique.
Inverse functions are inverse morphisms in the category Set of sets.
More generally, in any concrete category, the inverse of any isomorphism is given by the inverse of the corresponding function between underlying sets.
In type theory
In type theory, there are two different kinds of inverse functions, quasi-inverse functions, various kinds of more or less coherent quasi-inverse functions, and inverse functions.
For more on this see at equivalence in type theory.
Quasi-inverse functions
Given types and and a function , a quasi-inverse function of is a function such that is a retraction and a section of .
Equivalently, there are functions and for all and .
A function might have multiple quasi-inverse functions. The type of quasi-inverses of is given by
-quasi inverse functions
There are also variants of quasi-inverse functions where they are the inverse functions for -truncated types.
For example, every function is a (-1)-quasi inverse function, because it is an inverse function for h-propositions and .
A quasi-inverse function is a 0-quasi inverse function, because it is an inverse function for h-sets and .
A 1-quasi-inverse function is a quasi-inverse function with functions and for all and such that for all and , there are functions
This is an inverse function for h-groupoids and .
So on and so forth.
Inverse functions
Given types and and a function , an inverse function of is a function with a function for all and , such that for all identities , the fiber of at is contractible.
Coherent inverse functions
Given types and and a function , a coherent inverse function of is a quasi-inverse function with homotopies
which additionally has one of the two homotopies
The type of coherent inverse functions of is given by one of the following types
is called a half adjoint equivalence if it has a coherent inverse function.
Properties
Given functions and and homotopies and , there are elements
which satisfies the commutative squares for all elements and
Thus, there are functions
and
Every coherent inverse function is a quasi-inverse function by forgetting the additional coherence condition.
Theorem
If a function has a coherent inverse function, then for all elements the fiber of at is contractible.
Not really related
References