Merge pull request #2334 from jdchristensen/diagram-chase-pr

move SetoidRewrite to main library and other changes in preparation for diagram chasing

Author: Alizter

test/WildCat/SetoidRewrite.v

@@ -0,0 +1,103 @@
+#[warnings="-deprecated-from-Coq"]
+From Coq Require Init.Tactics. (* TODO: Can remove this line and previous once Rocq 9.0 is our minimum. *)
+From HoTT Require Import Basics.Overture Basics.Tactics.
+From HoTT.WildCat Require Import Core NatTrans Equiv SetoidRewrite.
+
+(** * Examples and tests of setoid rewriting *)
+
+(** ** Examples of setoid rewriting *)
+
+(** See theories/WildCat/HomologicalAlgebra.v for many more examples of setoid rewriting. *)
+
+(** Rewriting works in hypotheses. *)
+Proposition epic_sectionof {A} `{Is1Cat A}
+  {a b : A} (f : a $-> b) :
+  SectionOf f -> Epic f.
+Proof.
+  intros [right_inverse is_section] c g h eq_gf_hf.
+  apply cat_prewhisker with (h:=right_inverse) in eq_gf_hf.
+  rewrite 2 cat_assoc, is_section, 2 cat_idr in eq_gf_hf.
+  exact eq_gf_hf.
+Defined.
+
+(** A different approach, working in the goal. *)
+Proposition monic_retractionof {A} `{Is1Cat A}
+  {b c : A} (f : b $-> c) :
+  RetractionOf f -> Monic f.
+Proof.
+  intros [left_inverse is_retraction] a g h eq_fg_fh.
+  rewrite <- (cat_idl g), <- (cat_idl h).
+  rewrite <- is_retraction.
+  rewrite 2 cat_assoc.
+  exact (_ $@L eq_fg_fh).
+Defined.
+
+Proposition faithful_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.
+Proof.
+  intros faithful_F x y f g eq_Gf_Gg.
+  apply faithful_F.
+  apply (cate_monic_equiv (tau y)).
+  rewrite 2 (isnat tau).
+  by apply cat_prewhisker.
+Defined.
+
+(** ** Tests of setoid rewriting *)
+
+Section SetoidRewriteTests.
+
+  Goal forall (A : Type) `(H : Is0Gpd A) (a b c : A),
+      a $== b -> b $== c -> a $== c.
+  Proof.
+    intros A ? ? ? a b c eq_ab eq_bc.
+    by rewrite eq_ab, <- eq_bc.
+  Defined.
+
+  Goal forall (A : Type) `(H : Is0Gpd A) (a b c : A),
+      a $== b -> b $== c -> a $== c.
+  Proof.
+    intros A ? ? ? a b c eq_ab eq_bc.
+    symmetry.
+    rewrite eq_ab, <- eq_bc.
+    rewrite eq_bc.
+    by rewrite <- eq_bc.
+  Defined.
+
+  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.
+  Proof.
+    do 17 intro.
+    intro eq_fg.
+    by rewrite eq_fg.
+  Defined.
+
+  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.
+  Proof.
+    do 11 intro.
+    intro eq.
+    rewrite <- eq.
+    by rewrite eq.
+  Defined.
+
+  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.
+  Proof.
+  do 11 intro.
+  intro eq.
+  rewrite <- eq.
+  rewrite eq.
+  by rewrite <- eq.
+  Defined.
+
+  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.
+  Proof.
+    do 12 intro.
+    intros eq_g eq_f.
+    rewrite eq_g.
+    rewrite <- eq_f.
+    rewrite eq_f.
+    by rewrite <- eq_g.
+  Defined.
+
+End SetoidRewriteTests.

theories/Algebra/AbGroups/AbHom.v

@@ -1,5 +1,6 @@
 From HoTT Require Import Basics Types.
-Require Import WildCat HSet Truncations.Core Modalities.ReflectiveSubuniverse.
+From HoTT.WildCat Require Import Core Opposite Bifunctor Square Equiv.
+Require Import HSet Truncations.Core Modalities.ReflectiveSubuniverse.
 Require Import Groups.Group Groups.QuotientGroup AbelianGroup Biproduct.
 
 (** * Homomorphisms from a group to an abelian group form an abelian group. *)

theories/Algebra/AbGroups/AbelianGroup.v

@@ -1,11 +1,11 @@
 From HoTT Require Import Basics Types.
+From HoTT.WildCat Require Import Core Universe Equiv Induced PointedCat.
 Require Import Spaces.Nat.Core Spaces.Int.
 Require Export Classes.interfaces.canonical_names (Zero, zero, Plus, plus, Negate, negate, Involutive, involutive).
 Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative).
 Require Export Algebra.Groups.Group.
 Require Export Algebra.Groups.Subgroup.
 Require Import Algebra.Groups.QuotientGroup.
-Require Import WildCat.
 
 Local Set Polymorphic Inductive Cumulativity.
 

theories/Algebra/AbGroups/Abelianization.v

@@ -1,5 +1,6 @@
 From HoTT Require Import Basics Types Truncations.Core.
-Require Import Cubical.DPath WildCat.
+From HoTT.WildCat Require Import Core Equiv EquivGpd.
+Require Import Cubical.DPath.
 Require Import Colimits.Coeq.
 Require Import Algebra.AbGroups.AbelianGroup.
 Require Import Modalities.ReflectiveSubuniverse.

theories/Algebra/AbGroups/Biproduct.v

@@ -1,5 +1,5 @@
 From HoTT Require Import Basics Types Truncations.Core.
-Require Import WildCat.
+From HoTT.WildCat Require Import Core Equiv Bifunctor.
 Require Import HSet.
 Require Import AbelianGroup.
 Require Import Modalities.ReflectiveSubuniverse.

theories/Algebra/AbSES/BaerSum.v

@@ -1,5 +1,6 @@
 From HoTT Require Import Basics Types.
-Require Import WildCat Pointed.Core.
+From HoTT.WildCat Require Import Core Universe Opposite Bifunctor.
+Require Import Pointed.Core.
 Require Import AbGroups.AbelianGroup AbGroups.Biproduct AbGroups.AbHom.
 Require Import AbSES.Core AbSES.Pullback AbSES.Pushout AbSES.DirectSum.
 Require Import Homotopy.HSpace.Core.

theories/Algebra/AbSES/Core.v

@@ -1,5 +1,6 @@
 From HoTT Require Import Basics Types Truncations.Core.
-Require Import HSet WildCat Pointed.
+From HoTT.WildCat Require Import Core Equiv Induced NatTrans.
+Require Import HSet Pointed.Core Pointed.Loops.
 Require Import Groups.QuotientGroup Groups.ShortExactSequence.
 Require Import AbelianGroup AbGroups.Biproduct AbHom.
 Require Import Homotopy.ExactSequence.

theories/Algebra/AbSES/Ext.v

@@ -1,5 +1,6 @@
 From HoTT Require Import Basics Types Truncations.Core.
-Require Import Pointed WildCat.
+From HoTT.WildCat Require Import Core Universe Opposite Bifunctor.
+Require Import Pointed.Core Pointed.pTrunc.
 Require Import Truncations.SeparatedTrunc.
 Require Import AbelianGroup AbHom AbProjective.
 Require Import AbSES.Pullback AbSES.Pushout AbSES.BaerSum AbSES.Core.

theories/Algebra/AbSES/Pullback.v

@@ -1,6 +1,7 @@
 From HoTT Require Import Basics Types.
+From HoTT.WildCat Require Import Core NatTrans Universe Opposite.
 Require Import HSet Limits.Pullback.
-Require Import WildCat Pointed.Core Homotopy.ExactSequence.
+Require Import Pointed.Core Homotopy.ExactSequence.
 Require Import Modalities.ReflectiveSubuniverse.
 Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct.
 Require Import AbSES.Core AbSES.DirectSum.
@@ -483,7 +484,6 @@ Proof.
   - symmetry; apply abses_pullback_compose.
 Defined.
 
-
 Instance is0functor_abses10 `{Univalence} {A : AbGroup}
   : Is0Functor (fun B : AbGroup^op => AbSES B A).
 Proof.

theories/Algebra/AbSES/PullbackFiberSequence.v

@@ -1,5 +1,6 @@
 From HoTT Require Import Basics Types HSet HFiber Limits.Pullback.
-Require Import WildCat Pointed.Core Homotopy.ExactSequence.
+From HoTT.WildCat Require Import Core NatTrans.
+Require Import Pointed.Core Homotopy.ExactSequence.
 Require Import Groups.QuotientGroup.
 Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct.
 Require Import AbSES.Core AbSES.Pullback.