Quasi-inverses
Table of Contents
1 Quasi-inverses
module Lib.Data.QInv where
This file defines the notion of quasi-inverses, that is, map that have an inverse, and provides accessors to the data-structure.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Stdlib.Prelude import Lib.Data.Map
1.2 Definition
A map f : A → B has an inverse if there exists g : B → A such that f \circ g ~ id B and g \circ f ~ id A. As such, the type of a quasi-inverse is a triple (g, \alpha, \beta) where \alpha and \beta are the two homotopies verifying that g is indeed an inverse of f.
has-inverse (A B : U) (f : A → B) : U = Σ (B → A) (λg. (Htpy B (λ_. B) (map/comp B A B f g) (id B)) * (Htpy A (λ_. A) (map/comp A B A g f) (id A)))
1.3 Accessors
QInv/map (A B : U) (f : A → B) (i : has-inverse A B f) : B → A = i.1 QInv/right-htpy (A B : U) (f : A → B) (i : has-inverse A B f) : Htpy B (λ_. B) (map/comp B A B f (QInv/map A B f i)) (id B) = i.2.1 QInv/left-htpy (A B : U) (f : A → B) (i : has-inverse A B f) : Htpy A (λ_. A) (map/comp A B A (QInv/map A B f i) f) (id A) = i.2.2