(** * Typeclass instances to allow rewriting in wild categories *)

(** This file uses the setoid rewriting machinery from the Coq standard library to allow rewriting in wild-categories.  Examples are given in test/WildCat/SetoidRewrite.v and theories/WildCat/HomologicalAlgebra.v. *)

From HoTT Require Import Basics.Overture Basics.Tactics.
From Corelib Require Setoids.Setoid.
Import CMorphisms.ProperNotations.
From HoTT Require Import WildCat.Core.

#[export] Instance reflexive_proper_proxy {A : Type}
  {R : Relation A} `(Reflexive A R) (x : A)
  : CMorphisms.ProperProxy R x := reflexivity x.

(** forall (x y : A), x $== y -> forall (a b : A), a $== b -> y $== b -> x $==a *)
#[export] Instance IsProper_GpdHom_from {A : Type} `{Is0Gpd A}
  : CMorphisms.Proper
      (GpdHom ==>
         GpdHom ==>
         CRelationClasses.flip CRelationClasses.arrow) GpdHom.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
CMorphisms.Proper
  (GpdHom ==> GpdHom ==> CRelationClasses.flip CRelationClasses.arrow) GpdHom
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
CMorphisms.Proper
  (GpdHom ==> GpdHom ==> CRelationClasses.flip CRelationClasses.arrow) GpdHom
  (* Add the next line to the start of any proof to see what it means: *)
  unfold "==>", CMorphisms.Proper, CRelationClasses.arrow, CRelationClasses.flip in *.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
forall x y : A,
x $== y -> forall x0 y0 : A, x0 $== y0 -> y $== y0 -> x $== x0
  intros x y eq_xy a b eq_ab eq_yb.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
x, y: A
eq_xy: x $== y
a, b: A
eq_ab: a $== b
eq_yb: y $== b
x $== a
  exact (transitivity eq_xy (transitivity eq_yb
                              (symmetry _ _ eq_ab))).
  (* We could also just write:
    exact (eq_xy $@ eq_yb $@ eq_ab^$).
  The advantage of the above proof is that it works for other transitive and symmetric relations. *)
Defined.

(** forall (x y : A), x $== y -> forall (a b : A), a $== b -> x $== a -> y $== b *)
#[export] Instance IsProper_GpdHom_to {A : Type} `{Is0Gpd A}
  : CMorphisms.Proper
      (GpdHom ==>
         GpdHom ==>
         CRelationClasses.arrow) GpdHom.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
CMorphisms.Proper (GpdHom ==> GpdHom ==> CRelationClasses.arrow) GpdHom
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
CMorphisms.Proper (GpdHom ==> GpdHom ==> CRelationClasses.arrow) GpdHom
  intros x y eq_xy a b eq_ab eq_xa.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
x, y: A
eq_xy: x $== y
a, b: A
eq_ab: a $== b
eq_xa: x $== a
y $== b
  refine (transitivity _ eq_ab).
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
x, y: A
eq_xy: x $== y
a, b: A
eq_ab: a $== b
eq_xa: x $== a
y $== a
  refine (transitivity _ eq_xa).
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
x, y: A
eq_xy: x $== y
a, b: A
eq_ab: a $== b
eq_xa: x $== a
y $== x
  exact (symmetry _ _ eq_xy).
Defined.

(** forall a x y : A, x $== y -> a $== x -> a $== y *)
#[export] Instance IsProper_GpdHom_to_a {A : Type} `{Is0Gpd A}
  {a : A}
  : CMorphisms.Proper
      (GpdHom ==>
         CRelationClasses.arrow) (GpdHom a).
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
a: A
CMorphisms.Proper (GpdHom ==> CRelationClasses.arrow) (GpdHom a)
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
a: A
CMorphisms.Proper (GpdHom ==> CRelationClasses.arrow) (GpdHom a)
  intros x y eq_xy eq_ax.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
a, x, y: A
eq_xy: x $== y
eq_ax: a $== x
a $== y
  by transitivity x.
Defined.

(** forall a x y : A, x $== y -> a $== y -> a $== x *)
#[export] Instance IsProper_GpdHom_from_a {A : Type} `{Is0Gpd A}
  {a : A}
  : CMorphisms.Proper
      (GpdHom ==>
         CRelationClasses.flip CRelationClasses.arrow) (GpdHom a).
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
a: A
CMorphisms.Proper (GpdHom ==> CRelationClasses.flip CRelationClasses.arrow)
  (GpdHom a)
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
a: A
CMorphisms.Proper (GpdHom ==> CRelationClasses.flip CRelationClasses.arrow)
  (GpdHom a)
  intros x y eq_xy eq_ay.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
a, x, y: A
eq_xy: x $== y
eq_ay: a $== y
a $== x
  exact (transitivity eq_ay (symmetry _ _ eq_xy)).
Defined.

Open Scope signatureT_scope.

(** If [R] is symmetric and [R x y -> R' (f x) (f y)], then [R y x -> R' (f x) (f y)]. *)
#[export] Instance symmetry_flip {A B : Type} {f : A -> B}
  {R : Relation A} {R' : Relation B} `{Symmetric _ R}
  (H0 : CMorphisms.Proper (R ++> R') f)
  : CMorphisms.Proper (R --> R') f.
A, B: Type
f: A -> B
R: Relation A
R': Relation B
H: Symmetric R
H0: CMorphisms.Proper (R ==> R') f
CMorphisms.Proper (R --> R') f
Proof.
A, B: Type
f: A -> B
R: Relation A
R': Relation B
H: Symmetric R
H0: CMorphisms.Proper (R ==> R') f
CMorphisms.Proper (R --> R') f
  intros a b Rba; unfold CRelationClasses.flip in Rba.
A, B: Type
f: A -> B
R: Relation A
R': Relation B
H: Symmetric R
H0: CMorphisms.Proper (R ==> R') f
a, b: A
Rba: R b a
R' (f a) (f b)
  apply H0.
A, B: Type
f: A -> B
R: Relation A
R': Relation B
H: Symmetric R
H0: CMorphisms.Proper (R ==> R') f
a, b: A
Rba: R b a
R a b symmetry.
A, B: Type
f: A -> B
R: Relation A
R': Relation B
H: Symmetric R
H0: CMorphisms.Proper (R ==> R') f
a, b: A
Rba: R b a
R b a exact Rba.
Defined.

(** If [R'] is symmetric and [R x y -> R' x' y' -> R'' (f x x') (f y y')], then [R x y -> R' y' x' -> R'' (f x x') (f y y')]. *)
#[export] Instance symmetric_flip_snd {A B C : Type} {R : Relation A}
  {R' : Relation B} {R'' : Relation C} `{Symmetric _ R'}
  (f : A -> B -> C) (H1 : CMorphisms.Proper (R ++> R' ++> R'') f)
  : CMorphisms.Proper (R ++> R' --> R'') f.
A, B, C: Type
R: Relation A
R': Relation B
R'': Relation C
H: Symmetric R'
f: A -> B -> C
H1: CMorphisms.Proper (R ==> R' ==> R'') f
CMorphisms.Proper (R ==> R' --> R'') f
Proof.
A, B, C: Type
R: Relation A
R': Relation B
R'': Relation C
H: Symmetric R'
f: A -> B -> C
H1: CMorphisms.Proper (R ==> R' ==> R'') f
CMorphisms.Proper (R ==> R' --> R'') f
  intros a b Rab x y R'yx.
A, B, C: Type
R: Relation A
R': Relation B
R'': Relation C
H: Symmetric R'
f: A -> B -> C
H1: CMorphisms.Proper (R ==> R' ==> R'') f
a, b: A
Rab: R a b
x, y: B
R'yx: CRelationClasses.flip R' x y
R'' (f a x) (f b y) apply H1; [ assumption | symmetry; assumption ].
Defined.

#[export] Instance IsProper_fmap {A B : Type}
  (F : A -> B) `{Is1Functor _ _ F} (a b : A)
  : CMorphisms.Proper (GpdHom ==> GpdHom) (@fmap _ _ _ _ F _ a b)
  := fun _ _ => fmap2 F.

#[export] Instance IsProper_catcomp_g {A : Type} `{Is1Cat A}
  {a b c : A} (g : b $-> c)
  : CMorphisms.Proper (GpdHom ==> GpdHom) (@cat_comp _ _ _ a b c g)
  := fun _ _ => cat_postwhisker g.

#[export] Instance IsProper_catcomp {A : Type} `{Is1Cat A}
  {a b c : A}
  : CMorphisms.Proper (GpdHom ==> GpdHom ==> GpdHom)
      (@cat_comp _ _ _ a b c).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
CMorphisms.Proper (GpdHom ==> GpdHom ==> GpdHom) cat_comp
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
CMorphisms.Proper (GpdHom ==> GpdHom ==> GpdHom) cat_comp
  intros g1 g2 eq_g f1 f2 eq_f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
g1, g2: b $-> c
eq_g: g1 $== g2
f1, f2: a $-> b
eq_f: f1 $== f2
g1 $o f1 $== g2 $o f2
  exact (cat_comp2 eq_f eq_g).
Defined.

#[export] Instance gpd_hom_to_hom_proper {A B : Type} `{Is0Gpd A}
  {R : Relation B} (F : A -> B)
  {H2 : CMorphisms.Proper (GpdHom ==> R) F}
  : CMorphisms.Proper (Hom ==> R) F.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
R: Relation B
F: A -> B
H2: CMorphisms.Proper (GpdHom ==> R) F
CMorphisms.Proper (Hom ==> R) F
Proof.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
R: Relation B
F: A -> B
H2: CMorphisms.Proper (GpdHom ==> R) F
CMorphisms.Proper (Hom ==> R) F
  intros a b eq_ab; apply H2; exact eq_ab.
Defined.

#[export] Instance IsProper_Hom {A : Type} `{Is0Gpd A}
  : CMorphisms.Proper
      (Hom ==> Hom ==> CRelationClasses.arrow) Hom.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
CMorphisms.Proper (Hom ==> Hom ==> CRelationClasses.arrow) Hom
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
CMorphisms.Proper (Hom ==> Hom ==> CRelationClasses.arrow) Hom
  intros x y eq_xy a b eq_ab f.
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
x, y: A
eq_xy: x $-> y
a, b: A
eq_ab: a $-> b
f: x $-> a
y $-> b
  refine (transitivity _ eq_ab).
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
x, y: A
eq_xy: x $-> y
a, b: A
eq_ab: a $-> b
f: x $-> a
y $-> a
  refine (transitivity _ f).
A: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
x, y: A
eq_xy: x $-> y
a, b: A
eq_ab: a $-> b
f: x $-> a
y $-> x
  symmetry; exact eq_xy.
Defined.

#[export] Instance transitive_hom {A : Type} `{Is01Cat A} {x : A}
  : CMorphisms.Proper
      (Hom ==> CRelationClasses.arrow) (Hom x)
  := fun y z => cat_comp.