get the library working with Coq.Init.Tactics loaded

theories/Basics/Overture.v

@@ -70,10 +70,10 @@
 Notation "x * y" := (prod x y) : type_scope.
 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
 Notation "A /\ B" := (prod A B) (only parsing) : type_scope.
 Notation and := prod (only parsing).
 Notation conj := pair (only parsing).
 
 #[export] Hint Resolve pair inl inr : core.
 
 (** ** Type classes *)
 
@@ -139,7 +139,7 @@
 (** ** Basic definitions *)
 
 (** Define an alias for [Set], which is really [Type₀], the smallest universe. *)
 Notation Type0 := Set.
 
 (** ** Sigma types *)
 
@@ -186,8 +186,8 @@
 (** We bind [fibration_scope] with [sig] so that we are automatically in [fibration_scope] when we are passing an argument of type [sig]. *)
 Bind Scope fibration_scope with sig.
 
 Notation pr1 := proj1.
 Notation pr2 := proj2.
 
 (** The following notation is very convenient, although it unfortunately clashes with Proof General's "electric period".  We have added [format] specifiers in Notations.v so that it will display without an extra space, as [x.1] rather than as [x .1]. *)
 Notation "x .1" := (pr1 x) : fibration_scope.
@@ -196,7 +196,7 @@
 (** ** Functions *)
 
 (** We make the identity map a notation so we do not have to unfold it, or complicate matters with its type. *)
 Notation idmap := (fun x => x).
 
 Instance reflexive_fun : Reflexive (fun A B => A -> B)
   := fun _ => idmap.
@@ -282,6 +282,10 @@
 Register paths as core.identity.type.
 Register idpath as core.identity.refl.
 Register paths_rect as core.identity.ind.
+Register paths as core.eq.type.
+Register idpath as core.eq.refl.
+Register paths_ind as core.eq.ind.
+Register paths_rect as core.eq.rect.
 
 Notation "x = y :> A" := (@paths A x y) : type_scope.
 Notation "x = y" := (x = y :>_) : type_scope.
@@ -309,6 +313,11 @@
   exact u.
 Defined.
 
+Definition paths_rect_r := @paths_ind_r.
+
+Register paths_ind_r as core.eq.ind_r.
+Register paths_rect_r as core.eq.rect_r.
+
 Definition related_reflexive_path {A : Type} (R : Relation A) `{Reflexive A R}
   {a b : A} (p : a = b)
   : R a b.
@@ -328,6 +337,7 @@
   := match p with idpath => idpath end.
 
 Register inverse as core.identity.sym.
+Register inverse as core.eq.sym.
 
 (** Declaring this as [simpl nomatch] prevents the tactic [simpl] from expanding it out into [match] statements.  We only want [inverse] to simplify when applied to an identity path. *)
 Arguments inverse {A x y} p : simpl nomatch.
@@ -368,6 +378,7 @@
 Arguments transitive_paths / .
 
 Register concat as core.identity.trans.
+Register concat as core.eq.trans.
 
 (** Note that you can use the Coq tactics [reflexivity], [transitivity], [etransitivity], and [symmetry] when working with paths; we've redefined them above to use typeclasses and to unfold the instances so you get proof terms with [concat] and [inverse]. *)
 
@@ -395,10 +406,20 @@
 (** Transport is very common so it is worth introducing a parsing notation for it.  However, we do not use the notation for output because it hides the fibration, and so makes it very hard to read involved transport expression. *)
 Notation "p # u" := (transport _ p u) (only parsing) : path_scope.
 
+(** Functions act on paths: if [f : A -> B] and [p : x = y] is a path in [A], then [ap f p : f x = f y].  We typically pronounce [ap] as a single syllable, short for "application"; but it may also be considered as an acronym, "action on paths". *)
+
+Definition ap {A B : Type} (f : A -> B) {x y : A} (p : x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Global Arguments ap {A B}%_type_scope f%_function_scope {x y} p%_path_scope : simpl nomatch.
+
+Register ap as core.identity.congr.
+Register ap as core.eq.congr.
+
 (** The first time [rewrite] is used in each direction, it creates transport lemmas called [internal_paths_rew] and [internal_paths_rew_r].  See ../Tactics.v for how these compare to [transport].  We use [rewrite] here to trigger the creation of these lemmas.  This ensures that they are defined outside of sections, so they are not unnecessarily polymorphic.  The lemmas below are not used in the library. *)
 (** TODO: Since Coq 8.20 has PR#18299, once that is our minimum version we can instead register wrappers for [transport] to be used for rewriting.  See the comment by Dan Christensen in that PR for how to do this.  Then the tactics [internal_paths_rew_to_transport] and [rewrite_to_transport] can be removed from ../Tactics.v. *)
 Local Lemma define_internal_paths_rew A x y P (u : P x) (H : x = y :> A) : P y.
 Proof. rewrite <- H. exact u. Defined.
 
 Local Lemma define_internal_paths_rew_r A x y P (u : P y) (H : x = y :> A) : P x.
 Proof. rewrite -> H. exact u. Defined.
@@ -409,14 +430,7 @@
 
 (** Having defined transport, we can use it to talk about what a homotopy theorist might see as "paths in a fibration over paths in the base"; and what a type theorist might see as "heterogeneous equality in a dependent type".  We will first see this appearing in the type of [apD]. *)
 
-(** Functions act on paths: if [f : A -> B] and [p : x = y] is a path in [A], then [ap f p : f x = f y].  We typically pronounce [ap] as a single syllable, short for "application"; but it may also be considered as an acronym, "action on paths". *)
 
-Definition ap {A B : Type} (f : A -> B) {x y : A} (p : x = y) : f x = f y
-  := match p with idpath => idpath end.
-
-Global Arguments ap {A B}%_type_scope f%_function_scope {x y} p%_path_scope : simpl nomatch.
-
-Register ap as core.identity.congr.
 
 (** We introduce the convention that [apKN] denotes the application of a K-path between functions to an N-path between elements, where a 0-path is simply a function or an element. Thus, [ap] is a shorthand for [ap01]. *)
 Notation ap01 := ap (only parsing).

theories/Basics/PathGroupoids.v

@@ -808,6 +808,8 @@ Proof.
   exact q.
 Defined.
 
+Register ap011 as core.eq.congr2.
+
 Definition ap011_V {A B C} (f : A -> B -> C) {x x' y y'} (p : x = x') (q : y = y')
   : ap011 f p^ q^ = (ap011 f p q)^.
 Proof.