Require Import HoTT.Basics HoTT.Types.Require Import HoTT.Basics HoTT.Types.

Local Open Scope nat_scope.
Local Open Scope path_scope.

Generalizable Variables A B f.

(** * Relational equivalences *)

(** This definition is due to Peter LeFanu Lumsdaine on the HoTT mailing list.  This definition gives more judgmental properties, though has the downside of jumping universe levels. *)

Record RelEquiv A B :=
  { equiv_rel : A -> B -> Type;
    relequiv_contr_f :: forall a, Contr { b : B & equiv_rel a b };
    relequiv_contr_g :: forall b, Contr { a : A & equiv_rel a b } }.

Arguments equiv_rel {A B} _ _ _.

Definition issig_relequiv {A B}
  : { equiv_rel : A -> B -> Type
    | { f : forall a, Contr { b : B & equiv_rel a b }
      | forall b, Contr { a : A & equiv_rel a b } } }
      <~> RelEquiv A B.
A, B: Type
{equiv_rel0 : A -> B -> Type &
{_ : forall a : A, Contr {b : B & equiv_rel0 a b} &
forall b : B, Contr {a : A & equiv_rel0 a b}}} <~> 
RelEquiv A B
Proof.
A, B: Type
{equiv_rel0 : A -> B -> Type &
{_ : forall a : A, Contr {b : B & equiv_rel0 a b} &
forall b : B, Contr {a : A & equiv_rel0 a b}}} <~> 
RelEquiv A B
  issig.
Defined.

Definition relequiv_of_equiv {A B} (e : A <~> B) : RelEquiv A B.
A, B: Type
e: A <~> B
RelEquiv A B
Proof.
A, B: Type
e: A <~> B
RelEquiv A B
  exact {| equiv_rel a b := e a = b |}.
  (** The rest is found by typeclass inference! *)
Defined.

Definition equiv_of_relequiv {A B} (e : RelEquiv A B) : A <~> B.
A, B: Type
e: RelEquiv A B
A <~> B
Proof.
A, B: Type
e: RelEquiv A B
A <~> B
  refine (equiv_adjointify
            (fun a => (center { b : B & equiv_rel e a b}).1)
            (fun b => (center { a : A & equiv_rel e a b}).1)
            _ _);
    intro x; cbn.
A, B: Type
e: RelEquiv A B
x: B
(center {b : B & equiv_rel e (center {a : A & equiv_rel e a x}).1 b}).1 = x
A, B: Type
e: RelEquiv A B
x: A
(center {a : A & equiv_rel e a (center {b : B & equiv_rel e x b}).1}).1 = x
  {
A, B: Type
e: RelEquiv A B
x: B
(center {b : B & equiv_rel e (center {a : A & equiv_rel e a x}).1 b}).1 = x refine (ap pr1 (contr _) : _.1 = (x; _).1).
A, B: Type
e: RelEquiv A B
x: B
equiv_rel e (center {a : A & equiv_rel e a x}).1 x
    exact (center {a : A & equiv_rel e a x}).2. }
A, B: Type
e: RelEquiv A B
x: A
(center {a : A & equiv_rel e a (center {b : B & equiv_rel e x b}).1}).1 = x
  {
A, B: Type
e: RelEquiv A B
x: A
(center {a : A & equiv_rel e a (center {b : B & equiv_rel e x b}).1}).1 = x refine (ap pr1 (contr _) : _.1 = (x; _).1).
A, B: Type
e: RelEquiv A B
x: A
equiv_rel e x (center {b : B & equiv_rel e x b}).1
    exact (center {b : B & equiv_rel e x b}).2. }
Defined.

Definition RelIsEquiv {A B} (f : A -> B)
  := { r : RelEquiv A B | forall x, (center { b : B & equiv_rel r x b }).1 = f x }.

(** TODO: Prove [ishprop_relisequiv `{Funext} {A B} f : IsHProp (@RelIsEquiv A B f)] *)

(** * Judgmental property *)
Definition inverse_relequiv {A B} (e : RelEquiv A B) : RelEquiv B A
  := {| equiv_rel a b := equiv_rel e b a |}.

Definition reinv_V {A B} (e : RelEquiv A B)
  : inverse_relequiv (inverse_relequiv e) = e
  := 1.

(** TODO: Is there a definition of this that makes [inverse_relequiv (relequiv_idmap A)] be [relequiv_idmap A], judgmentally? *)
Definition relequiv_idmap A : RelEquiv A A
  := {| equiv_rel a b := a = b |}.

(** TODO: Define composition; we probably need truncation to do this? *)