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

(* Typeclass instances to allow rewriting in categories. Examples are given later in the file. *)

(* Init.Tactics contains the definition of the Coq stdlib typeclass_inferences database. It must be imported before Basics.Overture. *)

(** Warning: This imports Coq.Setoids.Setoid from the standard library. Currently the setoid rewriting machinery requires this to work, it depends on this file explicitly. This imports the whole standard library into the namespace.

All files that import WildCat/SetoidRewrite.v will also recursively import the entire Coq.Init standard library.  *)

(** Because of this, this file needs to be the *first* file Require'd in any file that uses it.  Otherwise, the typeclasses hintdb is cleared, breaking typeclass inference.  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. In the long term it would be good if this could be avoided.*)

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]
From HoTT Require Import Types.Forall.
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
  WildCat.NatTrans WildCat.Equiv.

#[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
  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))).
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_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: x $== a
y $== b
  unshelve 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_yb: x $== a
y $== a
  unshelve refine (transitivity _ 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: x $== a
y $== x
  exact (symmetry _ _ eq_xy).
Defined.

(* forall a : 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
  now transitivity x.
Defined.

(* forall a : 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.

#[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 Rab.
A, B: Type
f: A -> B
R: Relation A
R': Relation B
H: Symmetric R
H0: CMorphisms.Proper (R ==> R') f
a, b: A
Rab: CRelationClasses.flip R a b
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
Rab: CRelationClasses.flip R a b
R a b unfold CRelationClasses.flip.
A, B: Type
f: A -> B
R: Relation A
R': Relation B
H: Symmetric R
H0: CMorphisms.Proper (R ==> R') f
a, b: A
Rab: CRelationClasses.flip R a b
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
Rab: CRelationClasses.flip R a b
R b a exact Rab.
Defined.

#[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} `{Is1Cat A}
  `{Is1Cat A} (F : A -> B) `{Is1Functor _ _ F} (a b : A)
  : CMorphisms.Proper (GpdHom ==> GpdHom) (@fmap _ _ _ _ F _ a b) := fun _ _ eq => fmap2 F eq.

#[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).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
g: b $-> c
CMorphisms.Proper (GpdHom ==> GpdHom) (cat_comp g)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
g: b $-> c
CMorphisms.Proper (GpdHom ==> GpdHom) (cat_comp g)
  intros f1 f2.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
g: b $-> c
f1, f2: a $-> b
f1 $== f2 -> g $o f1 $== g $o f2
  apply (is0functor_postcomp a b c g ).
Defined.

#[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
  rewrite 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 f2 $== g2 $o f2
  apply (is0functor_precomp a b c f2).
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 $-> g2
  exact eq_g.
Defined.

#[export] Instance gpd_hom_to_hom_proper {A B : Type} `{Is0Gpd A}
  {R : Relation B} (F : A -> B)
  `{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 gpd_hom_is_proper1 {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).
A: Type
H: IsGraph A
H0: Is01Cat A
x: A
CMorphisms.Proper (Hom ==> CRelationClasses.arrow)
  (Hom x)
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
x: A
CMorphisms.Proper (Hom ==> CRelationClasses.arrow)
  (Hom x)
  intros y z g f.
A: Type
H: IsGraph A
H0: Is01Cat A
x, y, z: A
g: y $-> z
f: x $-> y
x $-> z
  exact (g $o f).
Defined.

Proposition IsEpic_HasSection {A} `{Is1Cat A}
  {a b : A} (f : a $-> b) :
  SectionOf f -> Epic f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b: A
f: a $-> b
SectionOf f -> Epic f
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b: A
f: a $-> b
SectionOf f -> Epic f
  intros section c g h eq_gf_hf.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b: A
f: a $-> b
section: SectionOf f
c: A
g, h: b $-> c
eq_gf_hf: g $o f $== h $o f
g $== h
  destruct section as [right_inverse is_section].
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b: A
f: a $-> b
right_inverse: b $-> a
is_section: f $o right_inverse $== Id b
c: A
g, h: b $-> c
eq_gf_hf: g $o f $== h $o f
g $== h
  apply (is0functor_precomp _ _ _ right_inverse) in eq_gf_hf;
    unfold cat_precomp in eq_gf_hf.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b: A
f: a $-> b
right_inverse: b $-> a
is_section: f $o right_inverse $== Id b
c: A
g, h: b $-> c
eq_gf_hf: g $o f $o right_inverse $->
h $o f $o right_inverse
g $== h
  rewrite 2 cat_assoc, is_section, 2 cat_idr in eq_gf_hf.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b: A
f: a $-> b
right_inverse: b $-> a
is_section: f $o right_inverse $== Id b
c: A
g, h: b $-> c
eq_gf_hf: g $-> h
g $== h
  exact eq_gf_hf.
Defined.

Proposition IsMonic_HasRetraction {A} `{Is1Cat A}
  {b c : A} (f : b $-> c) :
  RetractionOf f -> Monic f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
b, c: A
f: b $-> c
RetractionOf f -> Monic f
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
b, c: A
f: b $-> c
RetractionOf f -> Monic f
  intros retraction a g h eq_fg_fh.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
b, c: A
f: b $-> c
retraction: RetractionOf f
a: A
g, h: a $-> b
eq_fg_fh: f $o g $== f $o h
g $== h
  destruct retraction as [left_inverse is_retraction].
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
b, c: A
f: b $-> c
left_inverse: c $-> b
is_retraction: left_inverse $o f $== Id b
a: A
g, h: a $-> b
eq_fg_fh: f $o g $== f $o h
g $== h
  apply (is0functor_postcomp _ _ _ left_inverse) in eq_fg_fh;
    unfold cat_postcomp in eq_fg_fh.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
b, c: A
f: b $-> c
left_inverse: c $-> b
is_retraction: left_inverse $o f $== Id b
a: A
g, h: a $-> b
eq_fg_fh: left_inverse $o (f $o g) $->
left_inverse $o (f $o h)
g $== h
  rewrite <- 2 cat_assoc, is_retraction, 2 cat_idl in eq_fg_fh.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
b, c: A
f: b $-> c
left_inverse: c $-> b
is_retraction: left_inverse $o f $== Id b
a: A
g, h: a $-> b
eq_fg_fh: g $-> h
g $== h
  assumption.
Defined.

Proposition nat_equiv_faithful {A B : Type}
  {F G : A -> B} `{Is1Functor _ _ F}
  `{!Is0Functor G, !Is1Functor G}
  `{!HasEquivs B} (tau : NatEquiv F G)
  : Faithful F -> Faithful G.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
Faithful F -> Faithful G
Proof.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
Faithful F -> Faithful G
  intros faithful_F x y f g eq_Gf_Gg.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: fmap G f $== fmap G g
f $== g
  apply (@fmap _ _ _ _ _ (is0functor_precomp _
       _ _ (cat_equiv_natequiv tau x))) in eq_Gf_Gg.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: cat_precomp (G y) (tau x) (fmap G f) $->
cat_precomp (G y) (tau x) (fmap G g)
f $== g
  cbn in eq_Gf_Gg.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: cat_precomp (G y) (tau x) (fmap G f) $->
cat_precomp (G y) (tau x) (fmap G g)
f $== g
  unfold cat_precomp in eq_Gf_Gg.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: fmap G f $o tau x $-> fmap G g $o tau x
f $== g
  rewrite <- is1natural_natequiv in eq_Gf_Gg.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> fmap G g $o tau x
f $== g
  rewrite <- is1natural_natequiv in eq_Gf_Gg.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
f $== g
  apply faithful_F.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
fmap F f $== fmap F g
  assert (X : RetractionOf (tau y)).
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
RetractionOf (tau y)
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
X: RetractionOf (tau y)
fmap F f $== fmap F g {
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
RetractionOf (tau y)
    unshelve eapply Build_RetractionOf.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
G y $-> F y
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
?comp_left_inverse $o tau y $== Id (F y)
    -
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
G y $-> F y exact ((tau y)^-1$).
    -
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
(tau y)^-1$ $o tau y $== Id (F y) exact (cate_issect _ ).
  }
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
X: RetractionOf (tau y)
fmap F f $== fmap F g
  apply IsMonic_HasRetraction in X.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: tau y $o fmap F f $-> tau y $o fmap F g
X: Monic (tau y)
fmap F f $== fmap F g
  apply X in eq_Gf_Gg.
A, B: Type
F, G: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor G
HasEquivs0: HasEquivs B
tau: NatEquiv F G
faithful_F: Faithful F
x, y: A
f, g: x $-> y
eq_Gf_Gg: fmap F f $== fmap F g
X: Monic (tau y)
fmap F f $== fmap F g assumption.
Defined.

Section SetoidRewriteTests.
  Goal forall (A : Type) `(H : Is0Gpd A) (a b c : A),
      a $== b -> b $== c -> a $== c.
forall (A : Type) (H0 : IsGraph A) (H1 : Is01Cat A)
(H : Is0Gpd A) (a b c : A),
a $== b -> b $== c -> a $== c
  Proof.
forall (A : Type) (H0 : IsGraph A) (H1 : Is01Cat A)
(H : Is0Gpd A) (a b c : A),
a $== b -> b $== c -> a $== c
    intros A ? ? ? a b c eq_ab eq_bc.
A: Type
H0: IsGraph A
H1: Is01Cat A
H: Is0Gpd A
a, b, c: A
eq_ab: a $== b
eq_bc: b $== c
a $== c
    rewrite eq_ab, <- eq_bc.
A: Type
H0: IsGraph A
H1: Is01Cat A
H: Is0Gpd A
a, b, c: A
eq_ab: a $== b
eq_bc: b $== c
b $== b
  Abort.
  Goal forall (A : Type) `(H : Is0Gpd A) (a b c : A),
      a $== b -> b $== c -> a $== c.
forall (A : Type) (H0 : IsGraph A) (H1 : Is01Cat A)
(H : Is0Gpd A) (a b c : A),
a $== b -> b $== c -> a $== c
  Proof.
forall (A : Type) (H0 : IsGraph A) (H1 : Is01Cat A)
(H : Is0Gpd A) (a b c : A),
a $== b -> b $== c -> a $== c
    intros A ? ? ? a b c eq_ab eq_bc.
A: Type
H0: IsGraph A
H1: Is01Cat A
H: Is0Gpd A
a, b, c: A
eq_ab: a $== b
eq_bc: b $== c
a $== c
    symmetry.
A: Type
H0: IsGraph A
H1: Is01Cat A
H: Is0Gpd A
a, b, c: A
eq_ab: a $== b
eq_bc: b $== c
c $== a
    rewrite eq_ab, <- eq_bc.
A: Type
H0: IsGraph A
H1: Is01Cat A
H: Is0Gpd A
a, b, c: A
eq_ab: a $== b
eq_bc: b $== c
b $== b
    rewrite eq_bc.
A: Type
H0: IsGraph A
H1: Is01Cat A
H: Is0Gpd A
a, b, c: A
eq_ab: a $== b
eq_bc: b $== c
c $== c
    rewrite <- eq_bc.
A: Type
H0: IsGraph A
H1: Is01Cat A
H: Is0Gpd A
a, b, c: A
eq_ab: a $== b
eq_bc: b $== c
b $== b
  Abort.

  Goal forall (A B : Type) (F : A -> B) `{Is1Functor _ _ F} (a b : A) (f g : a $-> b), f $== g -> fmap F f $== fmap F g.
forall (A B : Type) (F : A -> B)
(IsGraph0 : IsGraph A) (Is2Graph0 : Is2Graph A)
(Is01Cat0 : Is01Cat A) (H : Is1Cat A)
(IsGraph1 : IsGraph B) (Is2Graph1 : Is2Graph B)
(Is01Cat1 : Is01Cat B) (H0 : Is1Cat B)
(Is0Functor0 : Is0Functor F),
Is1Functor F ->
forall (a b : A) (f g : a $-> b),
f $== g -> fmap F f $== fmap F g
  Proof.
forall (A B : Type) (F : A -> B)
(IsGraph0 : IsGraph A) (Is2Graph0 : Is2Graph A)
(Is01Cat0 : Is01Cat A) (H : Is1Cat A)
(IsGraph1 : IsGraph B) (Is2Graph1 : Is2Graph B)
(Is01Cat1 : Is01Cat B) (H0 : Is1Cat B)
(Is0Functor0 : Is0Functor F),
Is1Functor F ->
forall (a b : A) (f g : a $-> b),
f $== g -> fmap F f $== fmap F g
    do 17 intro.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
a, b: A
f, g: a $-> b
f $== g -> fmap F f $== fmap F g
    intro eq_fg.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
a, b: A
f, g: a $-> b
eq_fg: f $== g
fmap F f $== fmap F g
    rewrite eq_fg.
A, B: Type
F: A -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
a, b: A
f, g: a $-> b
eq_fg: f $== g
fmap F g $== fmap F g
  Abort.

  Goal forall (A : Type) `{Is1Cat A} (a b c : A) (f1 f2 : a $-> b) (g : b $-> c), f1 $== f2 -> g $o f1 $== g $o f2.
forall (A : Type) (IsGraph0 : IsGraph A)
(Is2Graph0 : Is2Graph A) (Is01Cat0 : Is01Cat A)
(H : Is1Cat A) (a b c : A) (f1 f2 : a $-> b)
(g : b $-> c), f1 $== f2 -> g $o f1 $== g $o f2
  Proof.
forall (A : Type) (IsGraph0 : IsGraph A)
(Is2Graph0 : Is2Graph A) (Is01Cat0 : Is01Cat A)
(H : Is1Cat A) (a b c : A) (f1 f2 : a $-> b)
(g : b $-> c), f1 $== f2 -> g $o f1 $== g $o f2
    do 11 intro.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f1, f2: a $-> b
g: b $-> c
f1 $== f2 -> g $o f1 $== g $o f2
    intro eq.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f1, f2: a $-> b
g: b $-> c
eq: f1 $== f2
g $o f1 $== g $o f2
    rewrite <- eq.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f1, f2: a $-> b
g: b $-> c
eq: f1 $== f2
g $o f1 $== g $o f1
    rewrite eq.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f1, f2: a $-> b
g: b $-> c
eq: f1 $== f2
g $o f2 $== g $o f2
  Abort.

  Goal forall (A : Type) `{Is1Cat A} (a b c : A) (f : a $-> b) (g1 g2 : b $-> c), g1 $== g2 -> g1 $o f $== g2 $o f.
forall (A : Type) (IsGraph0 : IsGraph A)
(Is2Graph0 : Is2Graph A) (Is01Cat0 : Is01Cat A)
(H : Is1Cat A) (a b c : A) (f : a $-> b)
(g1 g2 : b $-> c), g1 $== g2 -> g1 $o f $== g2 $o f
  Proof.
forall (A : Type) (IsGraph0 : IsGraph A)
(Is2Graph0 : Is2Graph A) (Is01Cat0 : Is01Cat A)
(H : Is1Cat A) (a b c : A) (f : a $-> b)
(g1 g2 : b $-> c), g1 $== g2 -> g1 $o f $== g2 $o f
  do 11 intro.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f: a $-> b
g1, g2: b $-> c
g1 $== g2 -> g1 $o f $== g2 $o f
  intro eq.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f: a $-> b
g1, g2: b $-> c
eq: g1 $== g2
g1 $o f $== g2 $o f
  rewrite <- eq.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f: a $-> b
g1, g2: b $-> c
eq: g1 $== g2
g1 $o f $== g1 $o f
  rewrite eq.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f: a $-> b
g1, g2: b $-> c
eq: g1 $== g2
g2 $o f $== g2 $o f
  rewrite <- eq.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f: a $-> b
g1, g2: b $-> c
eq: g1 $== g2
g1 $o f $== g1 $o f
  Abort.

  Goal forall (A : Type) `{Is1Cat A} (a b c : A) (f1 f2 : a $-> b) (g1 g2 : b $-> c), g1 $== g2 -> f1 $== f2 -> g1 $o f1 $== g2 $o f2.
forall (A : Type) (IsGraph0 : IsGraph A)
(Is2Graph0 : Is2Graph A) (Is01Cat0 : Is01Cat A)
(H : Is1Cat A) (a b c : A) (f1 f2 : a $-> b)
(g1 g2 : b $-> c),
g1 $== g2 -> f1 $== f2 -> g1 $o f1 $== g2 $o f2
  Proof.
forall (A : Type) (IsGraph0 : IsGraph A)
(Is2Graph0 : Is2Graph A) (Is01Cat0 : Is01Cat A)
(H : Is1Cat A) (a b c : A) (f1 f2 : a $-> b)
(g1 g2 : b $-> c),
g1 $== g2 -> f1 $== f2 -> g1 $o f1 $== g2 $o f2
    do 12 intro.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f1, f2: a $-> b
g1, g2: b $-> c
g1 $== g2 -> f1 $== f2 -> g1 $o f1 $== g2 $o f2
    intros eq_g eq_f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f1, f2: a $-> b
g1, g2: b $-> c
eq_g: g1 $== g2
eq_f: f1 $== f2
g1 $o f1 $== g2 $o f2
    rewrite eq_g.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f1, f2: a $-> b
g1, g2: b $-> c
eq_g: g1 $== g2
eq_f: f1 $== f2
g2 $o f1 $== g2 $o f2
    rewrite <- eq_f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f1, f2: a $-> b
g1, g2: b $-> c
eq_g: g1 $== g2
eq_f: f1 $== f2
g2 $o f1 $== g2 $o f1
    rewrite eq_f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f1, f2: a $-> b
g1, g2: b $-> c
eq_g: g1 $== g2
eq_f: f1 $== f2
g2 $o f2 $== g2 $o f2
    rewrite <- eq_g.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f1, f2: a $-> b
g1, g2: b $-> c
eq_g: g1 $== g2
eq_f: f1 $== f2
g1 $o f2 $== g1 $o f2
  Abort.
End SetoidRewriteTests.