SetoidRewrite.v

(** * 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. *)

(** Init.Tactics contains the definition of the Coq stdlib typeclass_inferences database.  With Coq 8.x, it must be imported before Basics.Overture.  Otherwise, the typeclasses hintdb is cleared, breaking typeclass inference.  Because of this, this file also needs to be the first file Require'd in any file that uses it.  Moreover, if Foo Requires this file, then Foo must also be the first file Require'd in any file that Requires Foo, and so on.  Once we assume Rocq 9.0 as our minimum, these comments can be removed. *)

#[warnings="-deprecated-from-Coq"]
From Coq Require Init.Tactics.
From HoTT Require Import Basics.Overture Basics.Tactics.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
#[warnings="-deprecated-from-Coq"]
From Coq Require Setoids.Setoid.[Loading ML file tauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file cc_plugin.cmxs (using legacy method) ... done]
[Loading ML file firstorder_plugin.cmxs (using legacy method) ... done]
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.