Bi-invertible Maps
Table of Contents
1 Bi-invertible maps
module Lib.Data.BiInv where
This file defines accessors of bi-invertible maps.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Stdlib.Prelude import Lib.Data.Map
1.2 is-bi-inv accessors
1.2.1 Of the left & right inverses
is-bi-inv/right-inv (A B : U) (f : A → B) (b : is-bi-inv A B f) : B → A = b.1.1 is-bi-inv/left-inv (A B : U) (f : A → B) (b : is-bi-inv A B f) : B → A = b.2.1
1.2.2 Of the left & right homotopies
is-bi-inv/right-htpy (A B : U) (f : A → B) (b : is-bi-inv A B f) : Htpy B (λ_. B) (map/comp B A B f (is-bi-inv/right-inv A B f b)) (id B) = b.1.2 is-bi-inv/left-htpy (A B : U) (f : A → B) (b : is-bi-inv A B f) : Htpy A (λ_. A) (map/comp A B A (is-bi-inv/left-inv A B f b) f) (id A) = b.2.2
1.3 BiInv accessors
1.3.1 Of the underlying constructions
BiInv/map (A B : U) (b : BiInv A B) : A → B = b.1 BiInv/is-bi-inv (A B : U) (b : BiInv A B) : is-bi-inv A B (BiInv/map A B b) = b.2
1.3.2 Of the left & right inverses
BiInv/right-inv (A B : U) (b : BiInv A B) : B → A = is-bi-inv/right-inv A B (BiInv/map A B b) (BiInv/is-bi-inv A B b) BiInv/left-inv (A B : U) (b : BiInv A B) : B → A = is-bi-inv/left-inv A B (BiInv/map A B b) (BiInv/is-bi-inv A B b)
1.3.3 Of the left & right homotopies
BiInv/right-htpy (A B : U) (b : BiInv A B) : Htpy B (λ_. B) (map/comp B A B (BiInv/map A B b) (BiInv/right-inv A B b)) (id B) = is-bi-inv/right-htpy A B (BiInv/map A B b) (BiInv/is-bi-inv A B b) BiInv/left-htpy (A B : U) (b : BiInv A B) : Htpy A (λ_. A) (map/comp A B A (BiInv/left-inv A B b) (BiInv/map A B b)) (id A) = is-bi-inv/left-htpy A B (BiInv/map A B b) (BiInv/is-bi-inv A B b)