blob: 25984483e4d669db80be193a65ad35f0310629c0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
(** * Isomorphisms *)
(** Following the category-theoretic definition, [f : A → B] is an
isomorphism when it has an inverse [f⁻¹ : B → A] which is both a
left and a right inverse. In the language of homotopy type
theory, we are formalizing quasi-invertibility; this notion of
isomorphism is not an hProp. The better notations of equivalence
(such that all proofs of [IsEquiv f] are equal when only assuming
function extensionality) are more complicated. Possibilities
include: *)
(** - Adjoint equivalence, the default of HoTT/HoTT: *)
(**
<<
Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
forall x : A, r (s x) = x.
Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
equiv_inv : B -> A ;
eisretr : Sect equiv_inv f;
eissect : Sect f equiv_inv;
eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
}.
>> *)
(** - Contractible fibers: [∀ y : B, Contr { x : A | f x = y }] where
[Contr T := { center : T | forall y, center = y }] *)
(** This is useful for classifying equalities in a theoretically nice
way. *)
Class IsIso {A B} (f : A -> B) :=
{ iso_inv : B -> A;
is_right_inv : forall x, f (iso_inv x) = x;
is_left_inv : forall x, iso_inv (f x) = x }.
Arguments iso_inv {_ _} _ {_} _.
Arguments is_right_inv {_ _} _ {_} _.
Arguments is_left_inv {_ _} _ {_} _.
|
