From HoTT Require Import Basics Types Truncations.

(** The "fiber" of a map with respect to a relation. *)
(** TODO remove? *)
Definition rfiber {X Y : Type} (R : Relation Y) (f : X -> Y) (y : Y) : Type
  := exists x, R (f x) y.

Definition lfiber {X Y : Type} (R : Relation Y) (f : X -> Y) (y : Y) : Type
  := exists x, R y (f x).

(** * The equivalence relation generated by a relation. *)

(** We model the equivalence relation generated by a relation using alternating zig-zags, and by throwing in reflexivity relations. It's easy to show that the resulting relation is an equivalence relation. *)

(** The 'zig' goes forward, and the 'zag' goes backward *)
Fixpoint zig_or_zag {X : Type} (R : Relation X) (n : nat) (x0 x1 : X) : Type
  := match n with
     | 0%nat => x0 = x1
     | S n => exists x, zig_or_zag R n x0 x * (R x x1 + R x1 x)
     end.

(** The equivalence relation generated by a relation [R]. *) 
Definition EqRel {X : Type} (R : Relation X) (x0 x1 : X) : Type
  := exists n, zig_or_zag R n x0 x1.

(** We can add ("cons") a zig or a zag at the end of a chain of such. *)

Definition zig_cons {X : Type} (R : Relation X) {x0 x1 x2 : X}
  (rho : EqRel R x0 x1) (zig : R x1 x2)
  : EqRel R x0 x2
  := (S rho.1; (x1; (rho.2, inl zig))).
                       
Definition zag_cons {X : Type} (R : Relation X) {x0 x1 x2 : X}
  (rho : EqRel R x0 x1) (zag : R x2 x1)
  : EqRel R x0 x2
  := (S rho.1; (x1; (rho.2, inr zag))).

Global Instance reflexive_eqrel {X : Type} (R : Relation X)
  : Reflexive (EqRel R) := fun _ => (0%nat; idpath).

Definition zig_to_eqrel {X : Type} (R : Relation X)
  {x0 x1 : X} (zig : R x0 x1) : EqRel R x0 x1
  := zig_cons R (reflexivity _) zig.

Definition zag_to_eqrel {X : Type} (R : Relation X)
  {x0 x1 : X} (zag : R x1 x0) : EqRel R x0 x1
  := zag_cons R (reflexivity _) zag.

(** ** [EqRel R] is an equivalence relation. We saw reflexivity above. *)

Global Instance transitive_eqrel {X : Type} (R : Relation X)
  : Transitive (EqRel R).
Proof.
  intros x0 x1 x2 rho01 [m zzs].
  revert x1 x2 rho01 zzs.
  induction m as [|m IH]; intros.
  - by induction zzs.
  - destruct zzs as [x [zzs [zig|zag]]].
    + exact (zig_cons R (IH _ _ rho01 zzs) zig).
    + exact (zag_cons R (IH _ _ rho01 zzs) zag).
Defined.

Global Instance symmetric_eqrel {X : Type} (R : Relation X)
  : Symmetric (EqRel R).
Proof.
  intros x0 x1 [n zzs]; revert x0 x1 zzs.
  induction n as [|n IH].
  - intros ? ? p; exact (0%nat; p^).
  - intros ? ? [x [zzs zorz]].
    transitivity x.
    2: by apply IH.
    destruct zorz as [zig|zag].
    + exact (zag_to_eqrel R zig).
    + exact (zig_to_eqrel R zag).
Defined.

(** To check whether a map respects [EqRel R], we just need to check that it respects [R]. *)
Definition eqrel_generator {X Y : Type}
  (R : Relation X) (Q : Relation Y) (f : X -> Y)
  : (forall x0 x1, R x0 x1 -> Q (f x0) (f x1))
    -> (forall x0 x1, EqRel R x0 x1 -> EqRel Q (f x0) (f x1)).
Proof.
  intros f_resp x0 x1 [n zz].
  (* we need a free endpoint before inducting on [n] *)
  revert dependent x1.
  induction n as [|n IH].
  1: intros; by induction zz.
  intros x1 [x [zz [zig|zag]]].
  - exact (zig_cons _ (IH _ zz) (f_resp _ _ zig)).
  - exact (zag_cons _ (IH _ zz) (f_resp _ _ zag)).
Defined.

(** TODO do we use this? *)

Definition MEqRel {X : Type} (R : Relation X) (x0 x1 : X) : Type
  := merely (EqRel R x0 x1).

Definition zig_to_meqrel {X : Type} (R : Relation X)
  : forall x0 x1, R x0 x1 -> MEqRel R x0 x1
  := fun _ _ rho => tr (zig_to_eqrel R rho).

Definition zag_to_meqrel {X : Type} (R : Relation X) {x0 x1 : X}
  (zag : R x1 x0) : MEqRel R x0 x1
  := tr (zag_to_eqrel R zag).

Global Instance reflexive_meqrel {X : Type} (R : Relation X)
  : Reflexive (MEqRel R) := fun _ => tr (0%nat; idpath).

Global Instance transitive_meqrel {X : Type} (R : Relation X)
  : Transitive (MEqRel R).
Proof.
Proof.
  intros x0 x1 x2 rho01 rho12; strip_truncations.
  destruct rho12 as [m zzs].
  revert x1 x2 rho01 zzs.
  induction m as [|m IH]; intros.
  - induction zzs.
    exact (tr rho01).
  - destruct zzs as [x [zzs [zig|zag]]];
      pose proof (IHz := IH _ _ rho01 zzs); strip_truncations.
    + exact (tr (zig_cons R IHz zig)).
    + exact (tr (zag_cons R IHz zag)).
Defined.

Global Instance symmetric_meqrel {X : Type} (R : Relation X)
  : Symmetric (MEqRel R).
Proof.
  intros x0 x1; apply Trunc_rec; intros [n zzs].
  revert x0 x1 zzs.
  induction n as [|n IH].
  - intros ? ? p; exact (tr (0%nat; p^)).
  - intros ? ? [x [zzs zorz]].
    transitivity x.
    2: by apply IH.
    destruct zorz as [zig|zag].
    + exact (tr (zag_to_eqrel R zig)).
    + exact (tr (zig_to_eqrel R zag)).
Defined.

(** todo: Now rewrite HigherExt.v to use this notion. *)