##### https://github.com/jarlg/Yoneda-Ext
Tip revision: 0d8bfe8
EquivalenceRelation.v
``````From HoTT Require Import Basics Types Truncations.

(** The "fiber" of a map with respect to a relation. *)
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.

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.
``````