nLab strict inverse function



In dependent type theory, there are two notions of equality,

  1. strict or judgmental equality,

  2. weak or typal equality.

Accordingly there are two corresponding notions of the inverse function of a function f:ABf:A \to B:

  1. There are the various notions of weak inverse functions, such as quasi-inverse functions and coherent inverse functions, which is a function f 1:BAf^{-1}:B \to A with homotopies h: x:Af 1(f(x))= Axh:\prod_{x:A} f^{-1}(f(x)) =_A x and k: y:Bf(f 1(y))= Byk:\prod_{y:B} f(f^{-1}(y)) =_B y and possibly other conditions and structure.

  2. There is the notion of strict inverse function, which is a function f 1:BAf^{-1}:B \to A with judgmental equalities x:Af 1(f(x))x:Ax:A \vdash f^{-1}(f(x)) \equiv x:A and y:Bf(f 1(y))y:By:B \vdash f(f^{-1}(y)) \equiv y:B. The other structures are unimportant since non-trivial paths for weak inverse functions reduce to reflexivity for x:Ax:A or y:By:B for strict inverse functions.


See also

Created on September 17, 2023 at 17:59:40. See the history of this page for a list of all contributions to it.