(* -*- mode: coq; mode: visual-line -*- *)

Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope path_scope.
Generalizable Variables A B f.

(** * Bi-invertible maps *)

(** A map is "bi-invertible" if it has both a section and a retraction, not necessarily the same.  This definition of equivalence was proposed by Andre Joyal. *)

Definition BiInv `(f : A -> B) : Type
  := {g : B -> A & g o f == idmap} * {h : B -> A & f o h == idmap}.

(** It seems that the easiest way to show that bi-invertibility is equivalent to being an equivalence is also to show that both are h-props and that they are logically equivalent. *)

Definition isequiv_biinv `(f : A -> B)
  : BiInv f -> IsEquiv f.
A, B: Type
f: A -> B
BiInv f -> IsEquiv f
Proof.
A, B: Type
f: A -> B
BiInv f -> IsEquiv f
  intros [[g s] [h r]].
A, B: Type
f: A -> B
g: B -> A
s: (fun x : A => g (f x)) == idmap
h: B -> A
r: (fun x : B => f (h x)) == idmap
IsEquiv f
  exact (isequiv_adjointify f g
    (fun x => ap f (ap g (r x)^ @ s (h x)) @ r x)
    s).
Defined.

Definition biinv_isequiv `(f : A -> B)
  : IsEquiv f -> BiInv f.
A, B: Type
f: A -> B
IsEquiv f -> BiInv f
Proof.
A, B: Type
f: A -> B
IsEquiv f -> BiInv f
  intros [g s r adj].
A, B: Type
f: A -> B
g: B -> A
s: (fun x : B => f (g x)) == idmap
r: (fun x : A => g (f x)) == idmap
adj: forall x : A, s (f x) = ap f (r x)
BiInv f
  exact ((g; r), (g; s)).
Defined.

Definition iff_biinv_isequiv `(f : A -> B)
  : BiInv f <-> IsEquiv f.
A, B: Type
f: A -> B
BiInv f <-> IsEquiv f
Proof.
A, B: Type
f: A -> B
BiInv f <-> IsEquiv f
  split.
A, B: Type
f: A -> B
BiInv f -> IsEquiv f
A, B: Type
f: A -> B
IsEquiv f -> BiInv f
  -
A, B: Type
f: A -> B
BiInv f -> IsEquiv f apply isequiv_biinv.
  -
A, B: Type
f: A -> B
IsEquiv f -> BiInv f apply biinv_isequiv.
Defined.

Global Instance ishprop_biinv `{Funext} `(f : A -> B) : IsHProp (BiInv f) | 0.
H: Funext
A, B: Type
f: A -> B
IsHProp (BiInv f)
Proof.
H: Funext
A, B: Type
f: A -> B
IsHProp (BiInv f)
  apply hprop_inhabited_contr.
H: Funext
A, B: Type
f: A -> B
BiInv f -> Contr (BiInv f)
  intros bif; pose (fe := isequiv_biinv f bif).
H: Funext
A, B: Type
f: A -> B
bif: BiInv f
fe:= isequiv_biinv f bif: IsEquiv f
Contr (BiInv f)
  apply @contr_prod.
H: Funext
A, B: Type
f: A -> B
bif: BiInv f
fe:= isequiv_biinv f bif: IsEquiv f
Contr {g : B -> A & (fun x : A => g (f x)) == idmap}
H: Funext
A, B: Type
f: A -> B
bif: BiInv f
fe:= isequiv_biinv f bif: IsEquiv f
Contr {h : B -> A & (fun x : B => f (h x)) == idmap}
  (* For this, we've done all the work already. *)
  -
H: Funext
A, B: Type
f: A -> B
bif: BiInv f
fe:= isequiv_biinv f bif: IsEquiv f
Contr {g : B -> A & (fun x : A => g (f x)) == idmap} by apply contr_retr_equiv.
  -
H: Funext
A, B: Type
f: A -> B
bif: BiInv f
fe:= isequiv_biinv f bif: IsEquiv f
Contr {h : B -> A & (fun x : B => f (h x)) == idmap} by apply contr_sect_equiv.
Defined.

Definition equiv_biinv_isequiv `{Funext} `(f : A -> B)
  : BiInv f <~> IsEquiv f.
H: Funext
A, B: Type
f: A -> B
BiInv f <~> IsEquiv f
Proof.
H: Funext
A, B: Type
f: A -> B
BiInv f <~> IsEquiv f
  apply equiv_iff_hprop_uncurried, iff_biinv_isequiv.
Defined.