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

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.
+  Abort.
+
+  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.
+  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.
+  Proof.
+    do 17 intro.
+    intro eq_fg.
+    by rewrite eq_fg.
+  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.
+  Proof.
+    do 11 intro.
+    intro eq.
+    rewrite <- eq.
+    by rewrite eq.
+  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.
+  Proof.
+  do 11 intro.
+  intro eq.
+  rewrite <- eq.
+  rewrite eq.
+  by rewrite <- eq.
+  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.
+  Proof.
+    do 12 intro.
+    intros eq_g eq_f.
+    rewrite eq_g.
+    rewrite <- eq_f.
+    rewrite eq_f.
+    by rewrite <- eq_g.
+  Abort.
+
+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. 

theories/Algebra/AbSES/Pushout.v

@@ -1,5 +1,6 @@
 From HoTT Require Import Basics Types Truncations.Core.
-Require Import WildCat Pointed.Core Homotopy.ExactSequence HIT.epi.
+From HoTT.WildCat Require Import Core Universe Opposite NatTrans.
+Require Import Pointed.Core Homotopy.ExactSequence HIT.epi.
 Require Import Modalities.ReflectiveSubuniverse.
 Require Import AbelianGroup AbPushout AbHom AbGroups.Biproduct.
 Require Import AbSES.Core AbSES.DirectSum.

theories/Algebra/AbSES/SixTerm.v

@@ -1,7 +1,11 @@
-From HoTT Require Import Basics Types WildCat HSet Pointed.Core Pointed.pTrunc Pointed.pEquiv
+From HoTT Require Import Basics Types.
+From HoTT.WildCat Require Import Core Opposite Equiv Bifunctor.
+Require Import Pointed.Core Pointed.pTrunc Pointed.pEquiv
   Modalities.ReflectiveSubuniverse Truncations.Core Truncations.SeparatedTrunc
-  AbGroups Homotopy.ExactSequence Spaces.Int Spaces.FreeInt
-  AbSES.Core AbSES.Pullback AbSES.Pushout BaerSum Ext PullbackFiberSequence.
+  AbGroups Homotopy.ExactSequence Spaces.Int Spaces.FreeInt.
+From HoTT.Algebra.AbSES Require Import Core Pullback Pushout BaerSum
+  Ext PullbackFiberSequence.
+Require Import HSet.
 
 (** * The contravariant six-term sequence of Ext *)
 

theories/Algebra/Groups/Group.v

@@ -16,7 +16,7 @@ Require Export Classes.interfaces.abstract_algebra (IsGroup(..), group_monoid, i
     IsSemiGroupPreserving, preserves_sg_op, IsUnitPreserving, preserves_mon_unit).
 Require Export Classes.theory.groups.
 Require Import Pointed.Core.
-Require Import WildCat.
+From HoTT.WildCat Require Import Core Universe Equiv Induced PointedCat Products.
 Require Import Spaces.Nat.Core Spaces.Int.
 Require Import Truncations.Core.
 

theories/Algebra/Groups/Presentation.v

@@ -4,8 +4,7 @@ Require Import Algebra.Groups.Group.
 Require Import Algebra.Groups.FreeGroup.
 Require Import Algebra.Groups.GroupCoeq.
 Require Import Spaces.Finite Spaces.List.Core.
-Require Import WildCat.
-
+From HoTT.WildCat Require Import Core Equiv Yoneda.
 
 Local Open Scope mc_scope.
 Local Open Scope mc_mult_scope.

theories/Algebra/Groups/QuotientGroup.v

@@ -6,7 +6,7 @@ Require Import Algebra.Groups.Subgroup.
 Require Export Colimits.Quotient.
 Require Import HSet.
 Require Import Spaces.Finite.Finite.
-Require Import WildCat.
+From HoTT.WildCat Require Import Core Equiv.
 Require Import Modalities.Modality.
 
 (** * Quotient groups *)

theories/Algebra/Groups/ShortExactSequence.v

@@ -1,6 +1,6 @@
 From HoTT Require Import Basics Types.
 Require Import Truncations.Core.
-Require Import WildCat.Core Pointed.
+Require Import WildCat.Core Pointed.Core.
 Require Import Groups.Group Groups.Subgroup.
 Require Import Homotopy.ExactSequence Modalities.Identity.
 

theories/Algebra/Rings/CRing.v

@@ -1,4 +1,4 @@
-Require Import WildCat.
+From HoTT.WildCat Require Import Core Equiv Induced.
 (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
 Require Import Classes.interfaces.abstract_algebra.
 Require Import Algebra.AbGroups.

theories/Algebra/Rings/ChineseRemainder.v

@@ -1,5 +1,5 @@
 Require Import Classes.interfaces.canonical_names.
-Require Import WildCat.
+From HoTT.WildCat Require Import Core Equiv.
 Require Import Modalities.ReflectiveSubuniverse.
 Require Import Algebra.AbGroups.
 Require Import Algebra.Rings.Ring.

theories/Algebra/Rings/Module.v

@@ -1,4 +1,4 @@
-Require Import WildCat.
+From HoTT.WildCat Require Import Core Equiv Induced Products.
 Require Import Spaces.Nat.Core.
 (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
 Require Import Classes.interfaces.canonical_names.

theories/Algebra/Rings/Ring.v

@@ -1,4 +1,4 @@
-Require Import WildCat.
+From HoTT.WildCat Require Import Core Universe Equiv Induced Products.
 Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic.
 (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
 Require Import Classes.interfaces.abstract_algebra.

theories/Algebra/ooGroup.v

@@ -1,9 +1,10 @@
 From HoTT Require Import Basics Types.
+From HoTT.WildCat Require Import Core Induced.
+Require Import Colimits.Quotient.
 Require Import Pointed.
 Require Import Truncations.Core Truncations.Connectedness.
 Require Import Homotopy.ClassifyingSpace.
-Require Import Algebra.Groups.
-Require Import WildCat.
+Require Import Algebra.Groups.Group.
 
 Local Open Scope trunc_scope.
 Local Open Scope path_scope.

theories/Homotopy/Bouquet.v

@@ -1,6 +1,7 @@
 From HoTT Require Import Basics Types.
-Require Import Pointed WildCat.
-Require Import Algebra.Groups.
+From HoTT.WildCat Require Import Core Universe Equiv NatTrans Yoneda.
+Require Import Pointed.
+From HoTT.Algebra.Groups Require Import Group FreeGroup.
 Require Import Modalities.ReflectiveSubuniverse Truncations.Core.
 Require Import Homotopy.Suspension.
 Require Import Homotopy.ClassifyingSpace.

theories/Homotopy/ClassifyingSpace.v

@@ -1,7 +1,8 @@
 From HoTT Require Import Basics Types.
-Require Import Pointed WildCat.
+From HoTT.WildCat Require Import Core Universe Equiv NatTrans Yoneda.
+Require Import Pointed.
 Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare.
-Require Import Algebra.AbGroups.
+Require Import Algebra.AbGroups.AbelianGroup.
 Require Import Homotopy.HSpace.Core.
 Require Import TruncType.
 Require Import Truncations.Core Truncations.Connectedness.

theories/Homotopy/EMSpace.v

@@ -1,14 +1,14 @@
 From HoTT Require Import Basics Types.
+From HoTT.WildCat Require Import Core Universe Equiv.
 Require Import Pointed.
 Require Import Cubical.DPath.
-Require Import Algebra.AbGroups.
+Require Import Algebra.AbGroups.AbelianGroup.
 Require Import Homotopy.Suspension.
 Require Import Homotopy.ClassifyingSpace.
 Require Import Homotopy.HSpace.Coherent.
 Require Import Homotopy.HomotopyGroup.
 Require Import Homotopy.Hopf.
 Require Import Truncations.Core Truncations.Connectedness.
-Require Import WildCat.
 
 (** * Eilenberg-Mac Lane spaces *)
 

theories/Homotopy/ExactSequence.v

@@ -1,7 +1,7 @@
 From HoTT Require Import Basics Types.
 Require Import SuccessorStructure.
-Require Import WildCat.
-Require Import Pointed.
+From HoTT.WildCat Require Import Core PointedCat Square Equiv.
+From HoTT.Pointed Require Import Core pMap pEquiv pFiber pTrunc Loops.
 Require Import Modalities.Identity Modalities.Descent.
 Require Import Truncations.
 Require Import HFiber.
@@ -439,7 +439,6 @@ Definition square_pfib_pequiv_cxfib {F X Y : pType}
   (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
   : pequiv_pmap_idmap o* i ==* pfib f o* pequiv_cxfib.
 Proof.
-  unfold Square.
   refine (pmap_postcompose_idmap _ @* _).
   symmetry; apply pfib_cxfib.
 Defined.

theories/Homotopy/HomotopyGroup.v

@@ -1,8 +1,8 @@
 From HoTT Require Import Basics Types Pointed HSet.
 Require Import Modalities.Modality.
 Require Import Truncations.Core Truncations.SeparatedTrunc.
-Require Import Algebra.AbGroups.
-Require Import WildCat.
+Require Import Algebra.AbGroups.AbelianGroup.
+From HoTT.WildCat Require Import Core Universe Equiv.
 
 Local Open Scope nat_scope.
 Local Open Scope pointed_scope.

theories/Homotopy/Join/Core.v

@@ -5,7 +5,8 @@ Require Import Extensions.
 Require Import Colimits.Pushout.
 Require Import Truncations.Core Truncations.Connectedness.
 Require Import Pointed.Core.
-Require Import WildCat.
+From HoTT.WildCat Require Import Core Universe Equiv EquivGpd
+  ZeroGroupoid Yoneda FunctorCat NatTrans Bifunctor Monoidal.
 Require Import Spaces.Nat.Core.
 
 Local Open Scope pointed_scope.

theories/Homotopy/Join/JoinAssoc.v

@@ -1,4 +1,6 @@
-From HoTT Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.
+From HoTT Require Import Basics Types Join.Core Join.TriJoin Spaces.Nat.Core.
+From HoTT.WildCat Require Import Core Universe Equiv ZeroGroupoid
+  Yoneda FunctorCat NatTrans Monoidal.
 
 (** * The associativity of [Join]
 

theories/Homotopy/Join/JoinSusp.v

@@ -1,6 +1,6 @@
 From HoTT Require Import Basics Types.
 Require Import Join.Core Join.JoinAssoc Suspension Spaces.Spheres.
-Require Import WildCat.
+From HoTT.WildCat Require Import Core Universe Equiv.
 Require Import Spaces.Nat.Core.
 
 (** * [Join Bool A] is equivalent to [Susp A]