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

Require Import HoTT.Basics HoTT.Types.

Local Open Scope nat_scope.
Local Open Scope path_scope.

Generalizable Variables A B f.

Record RelEquiv A B :=
  { equiv_rel : A → B → Type;
    relequiv_contr_f : ∀ a, Contr { b : B & equiv_rel a b };
    relequiv_contr_g : ∀ b, Contr { a : A & equiv_rel a b } }.

Arguments equiv_rel {A B} _ _ _.
Global Existing Instance relequiv_contr_f.
Global Existing Instance relequiv_contr_g.

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

Definition relequiv_of_equiv {A B} (e : A <~> B) : RelEquiv A B.
Proof.
  refine {| equiv_rel a b := e a = b |}.

Defined.

Definition equiv_of_relequiv {A B} (e : RelEquiv A B) : A <~> B.
Proof.
  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.
  { refine (ap pr1 (contr _) : _.1 = (x; _).1).
    exact (center {a : A & equiv_rel e a x}).2. }
  { refine (ap pr1 (contr _) : _.1 = (x; _).1).
    exact (center {b : B & equiv_rel e x b}).2. }
Defined.

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

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.

Definition relequiv_idmap A : RelEquiv A A
  := {| equiv_rel a b := a = b |}.