From 542fff561b0fb9a9a422adcdaa7b31625e24b036 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 May 2026 02:40:38 +1000
Subject: [PATCH 1/5] feat(CategoryTheory): add a grind propagator that
 normalizes morphism composition
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds a `grind` upward propagator on `CategoryTheory.CategoryStruct.comp`
that, every time `grind` internalizes a composition `f ≫ g`, pushes the
equality `f ≫ g = (right-associated form with syntactic identity factors
removed)` back into the e-graph.

The motivation is the Catalan blow-up of e-matching on `Category.assoc`: a
chain of length `n` lets e-matching generate all Catalan(n − 1)
parenthesizations as e-graph terms. Mathlib already has the runaway
documented at `CategoryTheory/Iso.lean:146`. The propagator commits to a
single canonical representative per fresh composition; the normalized form
is a fixed point, so it never re-fires on the form it produces — the
e-graph grows by O(1) terms per user-visible composition instead.

Notes:
- The `@[grind =]` / `@[grind _=_]` attributes are removed from
  `Category.id_comp`, `Category.comp_id`, `Category.assoc` because the
  propagator subsumes them and they would re-introduce the blow-up.
- `uliftCategory` in `Category/Basic.lean` now provides its three category
  axioms explicitly, since the `cat_disch` autoparam used to rely on the
  e-matching tags above and `Category/Basic.lean` runs before the
  propagator file is loaded.
- The propagator is registered via `initialize` calling
  `registerBuiltinUpwardPropagator` directly. The `builtin_grind_propagator`
  macro can't be used downstream in `module`-mode mathlib (see
  https://github.com/leanprover/lean4/issues/13805) and `grind_propagator`
  (the user-facing form) is not yet implemented in lean4 v4.30.0-rc2.
- The normalizer is hand-written rather than reusing `Meta.Simp.main`,
  which has no IR body and crashes the interpreter when invoked from a
  `module`-mode downstream file.

Tests in `MathlibTest/CategoryTheory/GrindCatNorm.lean` cover
associativity, identity removal, mixed cases, hypotheses flowing through
the normalizer, reducible-alias morphism types, and a long-chain heart-beat
guard.

🤖 Prepared with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 Mathlib.lean                                  |   1 +
 Mathlib/CategoryTheory/Category/Basic.lean    |   7 +-
 .../CategoryTheory/Tactic/GrindCatNorm.lean   | 194 ++++++++++++++++++
 MathlibTest/CategoryTheory/GrindCatNorm.lean  |  95 +++++++++
 4 files changed, 295 insertions(+), 2 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
 create mode 100644 MathlibTest/CategoryTheory/GrindCatNorm.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index d211bbdb619507..b710f4bccdbb30 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3433,6 +3433,7 @@ public import Mathlib.CategoryTheory.Subterminal
 public import Mathlib.CategoryTheory.Sums.Associator
 public import Mathlib.CategoryTheory.Sums.Basic
 public import Mathlib.CategoryTheory.Sums.Products
+public import Mathlib.CategoryTheory.Tactic.GrindCatNorm
 public import Mathlib.CategoryTheory.Thin
 public import Mathlib.CategoryTheory.Topos.Classifier
 public import Mathlib.CategoryTheory.Topos.Sheaf
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
index 1a55f91f20c3e1..ba3a4bc263027e 100644
--- a/Mathlib/CategoryTheory/Category/Basic.lean
+++ b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -240,8 +240,8 @@ class Category (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} ob
   assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h := by
     cat_disch
 
-attribute [to_dual existing (attr := simp, grind =) id_comp] Category.comp_id
-attribute [simp, grind _=_] Category.assoc
+attribute [to_dual existing (attr := simp) id_comp] Category.comp_id
+attribute [simp] Category.assoc
 
 initialize_simps_projections Category (-Hom)
 
@@ -402,6 +402,9 @@ def uliftCategory : Category.{v} (ULift.{u'} C) where
   Hom X Y := X.down ⟶ Y.down
   id X := 𝟙 X.down
   comp f g := f ≫ g
+  id_comp _ := Category.id_comp _
+  comp_id _ := Category.comp_id _
+  assoc _ _ _ := Category.assoc _ _ _
 
 attribute [local instance] uliftCategory in
 -- We verify that this previous instance can lift small categories to large categories.
diff --git a/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean b/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
new file mode 100644
index 00000000000000..c767b091a3d3de
--- /dev/null
+++ b/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
@@ -0,0 +1,194 @@
+/-
+Copyright (c) 2026 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+public import Mathlib.CategoryTheory.Category.Basic
+public import Lean.Meta.Tactic.Grind
+
+/-!
+# A `grind` propagator that normalizes morphism composition
+
+This file installs a `grind` upward propagator on
+`CategoryTheory.CategoryStruct.comp` that, every time `grind`
+internalizes a composition `f ≫ g`, pushes the equality
+`f ≫ g = (right-associated form with identity factors removed)`
+back into the e-graph.
+
+The reason this is a propagator rather than a set of `@[grind]`-tagged
+lemmas: tagging `Category.assoc`, `Category.id_comp`, `Category.comp_id`
+with `@[grind]` causes e-matching to instantiate `Category.assoc` once
+per parenthesization of every composition chain — for a chain of
+length `n` that is Catalan(n − 1) instantiations, each then attacked
+by `id_comp` / `comp_id`. The e-graph blows up. A propagator that
+commits to a single canonical representative per fresh composition
+avoids the blowup: the normalized form is a fixed point of itself, so
+the propagator only does work once per user-visible composition.
+
+We hand-write the normalizer (rather than using `Meta.Simp`) because
+`Simp.main` has no IR body, and crashes the interpreter when invoked
+from a `module`-mode downstream file.
+
+## Caveats
+
+- "Identity factors" are detected *syntactically* by head symbol
+  `CategoryStruct.id`. Opaque or reducible wrappers around `𝟙 _` are
+  treated as atoms and will not be stripped.
+- When a morphism's type does not `whnf` to a `Quiver.Hom` application
+  (e.g. an irreducible user-defined morphism type) the propagator
+  silently skips rather than throwing.
+-/
+
+@[expose] public section
+
+namespace Mathlib.Tactic.CategoryTheory.GrindCatNorm
+
+open Lean Meta
+
+initialize registerTraceClass `grind.catNorm
+
+/-- Returns `true` iff `e` is `𝟙 _`, i.e. `CategoryStruct.id _ _`. -/
+def isIdMorphism (e : Expr) : Bool :=
+  e.isAppOf ``CategoryTheory.CategoryStruct.id
+
+/-- Cheap structural check: `e` is a `≫` already in right-associated
+form with no identity factors.
+
+A right-associated comp tree has shape `f ≫ (g ≫ (h ≫ ...))`: every
+left argument is a non-comp non-identity. Identity-free means no leaf
+is `𝟙 _`. -/
+partial def isNormalizedComp (e : Expr) : Bool :=
+  if e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 then
+    let f := e.appFn!.appArg!
+    let g := e.appArg!
+    if f.isAppOf ``CategoryTheory.CategoryStruct.comp || isIdMorphism f then
+      false
+    else if g.isAppOf ``CategoryTheory.CategoryStruct.comp then
+      isNormalizedComp g
+    else
+      !isIdMorphism g
+  else
+    true
+
+/-- Reduce `t` to the canonical `@Quiver.Hom V _ X Y` shape and return
+`(X, Y)`. Returns `none` if `t` does not whnf to a `Quiver.Hom`
+application — e.g. because of a non-reducible user-defined morphism
+type, or because some implicit could not be elaborated. -/
+def extractHomEndpoints (t : Expr) : MetaM (Option (Expr × Expr)) := do
+  -- Reduce just far enough to expose a `Quiver.Hom` head — using default
+  -- transparency so ordinary `def`-aliases unfold, but stopping at
+  -- `Quiver.Hom` so we don't accidentally unfold the projection itself.
+  let some t ← withDefault <| whnfUntil t ``Quiver.Hom | return none
+  unless t.isAppOfArity ``Quiver.Hom 4 do return none
+  let args := t.getAppArgs
+  return some (args[2]!, args[3]!)
+
+/-- Build the term `f ≫ g` given the two morphism arguments and a
+"comp shell" `e0` from which we copy the `comp` head (with its
+universe levels, category, and category-struct instance).
+
+Returns `none` if the source/middle/target objects cannot be extracted
+from `f`'s and `g`'s types — i.e. if either type fails to whnf to a
+`Quiver.Hom` application. In that case the caller should skip rewriting. -/
+def mkCompFromShell (e0 : Expr) (f g : Expr) : MetaM (Option Expr) := do
+  let some (X', Y') ← extractHomEndpoints (← inferType f) | return none
+  let some (_, Z') ← extractHomEndpoints (← inferType g) | return none
+  let args := e0.getAppArgs
+  let C := args[0]!
+  let inst := args[1]!
+  -- Reuse the original `comp` head from `e0` to preserve maximal sharing.
+  return some (mkAppN e0.getAppFn #[C, inst, X', Y', Z', f, g])
+
+/-- Normalize a morphism expression to right-associated identity-free
+form. Returns `(e', proof?)` where:
+- `e' = e` (semantically)
+- `e'` is right-associated and identity-free
+- `proof?` is `some p` with `p : e = e'`, or `none` if `e = e'` syntactically.
+-/
+partial def normalizeComp (e : Expr) : MetaM (Expr × Option Expr) := do
+  unless e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 do
+    return (e, none)
+  -- e = a ≫ b
+  let a := e.appFn!.appArg!
+  let b := e.appArg!
+  -- recurse on children first
+  let (a', aProof?) ← normalizeComp a
+  let (b', bProof?) ← normalizeComp b
+  -- Build (potentially) an updated comp `a' ≫ b'` with proof e = a' ≫ b'.
+  let (e1, e1Proof?) ← do
+    if aProof?.isNone && bProof?.isNone then
+      pure (e, none)
+    else
+      let some e1 ← mkCompFromShell e a' b' | return (e, none)
+      -- proof: a ≫ b = a' ≫ b'
+      let aP := aProof?.getD (← mkEqRefl a)
+      let bP := bProof?.getD (← mkEqRefl b)
+      -- e = `comp C inst X Y Z f g`, so e.appFn!.appFn! = `comp C inst X Y Z`,
+      -- which is the binary function we are applying congruence to.
+      let proof ← mkCongrArg₂ e.appFn!.appFn! aP bP
+      pure (e1, some proof)
+  -- Now consider `a' ≫ b'` (which is e1). Apply local rewrites.
+  -- Identity left: 𝟙 X ≫ b' = b'
+  if isIdMorphism a' then
+    let p ← mkAppM ``CategoryTheory.Category.id_comp #[b']
+    let proof ← combineProofs e1Proof? p
+    return (b', some proof)
+  -- Identity right: a' ≫ 𝟙 Y = a'
+  if isIdMorphism b' then
+    let p ← mkAppM ``CategoryTheory.Category.comp_id #[a']
+    let proof ← combineProofs e1Proof? p
+    return (a', some proof)
+  -- Reassociation: (x ≫ y) ≫ b' = x ≫ (y ≫ b'), then recurse on x ≫ (y ≫ b')
+  if a'.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 then
+    let x := a'.appFn!.appArg!
+    let y := a'.appArg!
+    let p ← mkAppM ``CategoryTheory.Category.assoc #[x, y, b']
+    -- new shape: x ≫ (y ≫ b')
+    let some yb' ← mkCompFromShell e y b' | return (e1, e1Proof?)
+    let some new ← mkCompFromShell e x yb' | return (e1, e1Proof?)
+    -- now recursively normalize `new`
+    let (newNorm, newNormProof?) ← normalizeComp new
+    let combined ←
+      match e1Proof?, newNormProof? with
+      | none, none => pure p
+      | some e1p, none => mkAppM ``Eq.trans #[e1p, p]
+      | none, some np => mkAppM ``Eq.trans #[p, np]
+      | some e1p, some np => do
+        let t1 ← mkAppM ``Eq.trans #[e1p, p]
+        mkAppM ``Eq.trans #[t1, np]
+    return (newNorm, some combined)
+  -- Otherwise, a' is a leaf and b' is either a leaf or already normalized comp.
+  return (e1, e1Proof?)
+where
+  combineProofs (first : Option Expr) (second : Expr) : MetaM Expr := do
+    match first with
+    | none => return second
+    | some p => mkAppM ``Eq.trans #[p, second]
+  mkCongrArg₂ (f : Expr) (ha : Expr) (hb : Expr) : MetaM Expr := do
+    -- Build a proof that f a b = f a' b' given ha : a = a', hb : b = b'.
+    -- Use mkCongr: mkCongr (mkCongrArg f ha) hb gives f a b = f a' b'.
+    let step1 ← mkCongrArg f ha
+    mkCongr step1 hb
+
+/-- The propagator body. -/
+def catCompPropagatorImpl (e : Expr) : Grind.GoalM Unit := do
+  trace[grind.catNorm] "fire on: {e}"
+  unless e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 do return ()
+  if isNormalizedComp e then
+    trace[grind.catNorm] "  skip: already normalized"
+    return ()
+  let (e', proof?) ← normalizeComp e
+  let some proof := proof? | return ()
+  let e' ← Grind.shareCommon e'
+  trace[grind.catNorm] "  normalized to: {e'}"
+  let gen ← Grind.getGeneration e
+  Grind.internalize e' gen (some e)
+  Grind.pushEq e e' proof
+
+initialize
+  let name := ``CategoryTheory.CategoryStruct.comp
+  Lean.Meta.Grind.registerBuiltinUpwardPropagator name catCompPropagatorImpl
+
+end Mathlib.Tactic.CategoryTheory.GrindCatNorm
diff --git a/MathlibTest/CategoryTheory/GrindCatNorm.lean b/MathlibTest/CategoryTheory/GrindCatNorm.lean
new file mode 100644
index 00000000000000..42df94b8015034
--- /dev/null
+++ b/MathlibTest/CategoryTheory/GrindCatNorm.lean
@@ -0,0 +1,95 @@
+import Mathlib.CategoryTheory.Tactic.GrindCatNorm
+
+/-!
+# Regression tests for the `grind` category-composition normalizer
+
+The propagator pushes the equality `f ≫ g = (right-associated, identity-free
+form)` into grind's e-graph for each composition it sees. With the
+permanent `@[grind]` attributes on `Category.assoc` / `id_comp` /
+`comp_id` removed, these examples are not solvable by `grind` via
+e-matching alone; they only close because the propagator is loaded.
+-/
+
+open CategoryTheory
+
+universe v u
+
+variable {C : Type u} [Category.{v} C]
+
+section AssociativityOnly
+
+example {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) :
+    (f ≫ g) ≫ h = f ≫ (g ≫ h) := by grind
+
+example {X Y Z W V : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (k : W ⟶ V) :
+    ((f ≫ g) ≫ h) ≫ k = f ≫ g ≫ h ≫ k := by grind
+
+example {X Y Z W V : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (k : W ⟶ V) :
+    (f ≫ g) ≫ (h ≫ k) = f ≫ (g ≫ h) ≫ k := by grind
+
+example {X₁ X₂ X₃ X₄ X₅ X₆ : C}
+    (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : X₃ ⟶ X₄) (f₄ : X₄ ⟶ X₅) (f₅ : X₅ ⟶ X₆) :
+    ((f₁ ≫ f₂) ≫ f₃) ≫ (f₄ ≫ f₅) = f₁ ≫ (f₂ ≫ f₃ ≫ f₄) ≫ f₅ := by grind
+
+end AssociativityOnly
+
+section IdentityRemoval
+
+example {X Y : C} (f : X ⟶ Y) : 𝟙 X ≫ f = f := by grind
+example {X Y : C} (f : X ⟶ Y) : f ≫ 𝟙 Y = f := by grind
+example {X : C} : 𝟙 X ≫ 𝟙 X = 𝟙 X := by grind
+
+example {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    f ≫ 𝟙 Y ≫ g = f ≫ g := by grind
+
+example {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (𝟙 X ≫ f) ≫ (g ≫ 𝟙 Z) = f ≫ g := by grind
+
+end IdentityRemoval
+
+section Mixed
+
+example {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) :
+    (𝟙 X ≫ (f ≫ g)) ≫ h ≫ 𝟙 W = f ≫ g ≫ h := by grind
+
+example {X₁ X₂ X₃ X₄ X₅ : C}
+    (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : X₃ ⟶ X₄) (f₄ : X₄ ⟶ X₅) :
+    𝟙 X₁ ≫ ((f₁ ≫ 𝟙 X₂) ≫ f₂) ≫ (𝟙 X₃ ≫ f₃ ≫ 𝟙 X₄) ≫ f₄ ≫ 𝟙 X₅ =
+      f₁ ≫ f₂ ≫ f₃ ≫ f₄ := by grind
+
+end Mixed
+
+section WithHypotheses
+
+/-- Composition with a hypothesis that needs to flow through the normalizer. -/
+example {X Y Z W : C} (f₁ f₂ : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W)
+    (hfg : f₁ ≫ g = f₂ ≫ g) :
+    (f₁ ≫ g) ≫ h = (f₂ ≫ g) ≫ h := by grind
+
+end WithHypotheses
+
+section ReducibleAliases
+
+/-- A reducible alias for the morphism type, even with object arguments
+swapped, should still be handled. The propagator reduces the inferred
+type until it hits `Quiver.Hom` and extracts the endpoints from there. -/
+private def MorAlias (Y X : C) := X ⟶ Y
+
+example {X Y Z W : C} (f : MorAlias Y X) (g : MorAlias Z Y) (h : MorAlias W Z) :
+    (f ≫ g) ≫ h = f ≫ (g ≫ h) := by grind
+
+end ReducibleAliases
+
+section LongChain
+
+-- Performance guard: a 10-morphism left-associated chain should
+-- normalize in well under the default heart-beat budget. If this starts
+-- failing, the normalizer's per-prefix work has likely regressed.
+set_option maxHeartbeats 200000 in
+example {X₀ X₁ X₂ X₃ X₄ X₅ X₆ X₇ X₈ X₉ X₁₀ : C}
+    (f₁ : X₀ ⟶ X₁) (f₂ : X₁ ⟶ X₂) (f₃ : X₂ ⟶ X₃) (f₄ : X₃ ⟶ X₄) (f₅ : X₄ ⟶ X₅)
+    (f₆ : X₅ ⟶ X₆) (f₇ : X₆ ⟶ X₇) (f₈ : X₇ ⟶ X₈) (f₉ : X₈ ⟶ X₉) (f₁₀ : X₉ ⟶ X₁₀) :
+    ((((((((f₁ ≫ f₂) ≫ f₃) ≫ f₄) ≫ f₅) ≫ f₆) ≫ f₇) ≫ f₈) ≫ f₉) ≫ f₁₀ =
+      f₁ ≫ f₂ ≫ f₃ ≫ f₄ ≫ f₅ ≫ f₆ ≫ f₇ ≫ f₈ ≫ f₉ ≫ f₁₀ := by grind
+
+end LongChain

From 4238c4878acfcc9d74714f26af2942dd75f51d08 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 May 2026 03:02:13 +1000
Subject: [PATCH 2/5] refactor: use local grind attrs in Category.Basic; trim
 docstring
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Replace explicit `id_comp/comp_id/assoc` fields on `uliftCategory`
  with `attribute [local grind =] / [local grind _=_]` on the three
  lemmas. The `cat_disch` autoparam can use the e-matching tags
  locally without leaking them to downstream files.
- Drop the implementation note about `Simp.main` from the
  `GrindCatNorm.lean` module docstring.

🤖 Prepared with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 Mathlib/CategoryTheory/Category/Basic.lean      | 10 +++++++---
 Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean |  4 ----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
index ba3a4bc263027e..fefde4966e6d28 100644
--- a/Mathlib/CategoryTheory/Category/Basic.lean
+++ b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -394,6 +394,13 @@ variable [Category.{v} C]
 
 universe u'
 
+-- The propagator in `Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean` is loaded
+-- only *after* this file, so the `cat_disch` autoparam in `uliftCategory` below
+-- cannot rely on it. We make the relevant equational lemmas available to
+-- `grind` locally for the rest of this file.
+attribute [local grind =] Category.id_comp Category.comp_id
+attribute [local grind _=_] Category.assoc
+
 /-- The category structure on `ULift C` that is induced from the category
 structure on `C`. This is not made a global instance because of a diamond
 when `C` is a preordered type. -/
@@ -402,9 +409,6 @@ def uliftCategory : Category.{v} (ULift.{u'} C) where
   Hom X Y := X.down ⟶ Y.down
   id X := 𝟙 X.down
   comp f g := f ≫ g
-  id_comp _ := Category.id_comp _
-  comp_id _ := Category.comp_id _
-  assoc _ _ _ := Category.assoc _ _ _
 
 attribute [local instance] uliftCategory in
 -- We verify that this previous instance can lift small categories to large categories.
diff --git a/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean b/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
index c767b091a3d3de..aac9c5ba07599b 100644
--- a/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
+++ b/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
@@ -27,10 +27,6 @@ commits to a single canonical representative per fresh composition
 avoids the blowup: the normalized form is a fixed point of itself, so
 the propagator only does work once per user-visible composition.
 
-We hand-write the normalizer (rather than using `Meta.Simp`) because
-`Simp.main` has no IR body, and crashes the interpreter when invoked
-from a `module`-mode downstream file.
-
 ## Caveats
 
 - "Identity factors" are detected *syntactically* by head symbol

From 5216b55869b78a32fa6e498e726680b00e66241b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 May 2026 03:08:25 +1000
Subject: [PATCH 3/5] refactor(CategoryTheory): delegate the comp normaliser to
 simp
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Replaces the hand-written `normalizeComp` recursion (and supporting
`mkCompFromShell` / `extractHomEndpoints` helpers) with a single call
to `simpOnlyNames` on `Category.id_comp`, `Category.comp_id`,
`Category.assoc`. Simp already handles congruence, transitivity, and
maximal sharing, so the file shrinks from ~190 to ~110 lines.

The propagator still keeps the cheap `isNormalizedComp` structural
guard so that already-normal compositions don't pay the cost of
invoking simp. When simp fails (e.g. composition under a bare
`CategoryStruct` instance with no synthesizable `Category`), the
propagator silently skips that term rather than aborting `grind`.

Suggested by a second-opinion code review.

🤖 Prepared with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 .../CategoryTheory/Tactic/GrindCatNorm.lean   | 172 +++++-------------
 1 file changed, 47 insertions(+), 125 deletions(-)

diff --git a/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean b/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
index aac9c5ba07599b..62f611d07dc7f1 100644
--- a/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
+++ b/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.CategoryTheory.Category.Basic
 public import Lean.Meta.Tactic.Grind
+public import Mathlib.Lean.Meta.Simp
 
 /-!
 # A `grind` propagator that normalizes morphism composition
@@ -14,27 +15,34 @@ public import Lean.Meta.Tactic.Grind
 This file installs a `grind` upward propagator on
 `CategoryTheory.CategoryStruct.comp` that, every time `grind`
 internalizes a composition `f ≫ g`, pushes the equality
-`f ≫ g = (right-associated form with identity factors removed)`
+`f ≫ g = (right-associated form with syntactic identity factors removed)`
 back into the e-graph.
 
 The reason this is a propagator rather than a set of `@[grind]`-tagged
 lemmas: tagging `Category.assoc`, `Category.id_comp`, `Category.comp_id`
 with `@[grind]` causes e-matching to instantiate `Category.assoc` once
 per parenthesization of every composition chain — for a chain of
-length `n` that is Catalan(n − 1) instantiations, each then attacked
-by `id_comp` / `comp_id`. The e-graph blows up. A propagator that
-commits to a single canonical representative per fresh composition
-avoids the blowup: the normalized form is a fixed point of itself, so
-the propagator only does work once per user-visible composition.
+length `n` that is Catalan(n − 1) instantiations. The e-graph blows
+up. Mathlib already has the runaway documented at
+`Mathlib/CategoryTheory/Iso.lean:146`. A propagator that commits to a
+single canonical representative per fresh composition avoids the
+blowup: the normalized form is a fixed point of itself, so the
+propagator only does work once per user-visible composition.
+
+The rewrite itself is delegated to `simp` with a three-lemma simp
+set; we only contribute the structural shortcut that recognises
+already-normalised compositions and the glue that feeds the result
+back into `grind`'s e-graph.
 
 ## Caveats
 
-- "Identity factors" are detected *syntactically* by head symbol
+- Identity factors are detected *syntactically* by head symbol
   `CategoryStruct.id`. Opaque or reducible wrappers around `𝟙 _` are
-  treated as atoms and will not be stripped.
-- When a morphism's type does not `whnf` to a `Quiver.Hom` application
-  (e.g. an irreducible user-defined morphism type) the propagator
-  silently skips rather than throwing.
+  treated as atoms and will not be stripped at the shortcut layer
+  (though they may still be normalised by `simp` if it can unfold them).
+- If a composition's instance argument is `CategoryStruct` without a
+  matching `Category` instance, the lemma applications fail; we catch
+  this and silently skip the rewrite rather than aborting `grind`.
 -/
 
 @[expose] public section
@@ -47,15 +55,18 @@ initialize registerTraceClass `grind.catNorm
 
 /-- Returns `true` iff `e` is `𝟙 _`, i.e. `CategoryStruct.id _ _`. -/
 def isIdMorphism (e : Expr) : Bool :=
-  e.isAppOf ``CategoryTheory.CategoryStruct.id
+  e.consumeMData.isAppOf ``CategoryTheory.CategoryStruct.id
 
 /-- Cheap structural check: `e` is a `≫` already in right-associated
-form with no identity factors.
+form with no identity factors. We use this to short-circuit the
+propagator on terms that are already normalised, avoiding the cost of
+invoking `simp` on every internalised sub-composition.
 
-A right-associated comp tree has shape `f ≫ (g ≫ (h ≫ ...))`: every
-left argument is a non-comp non-identity. Identity-free means no leaf
-is `𝟙 _`. -/
+A right-associated identity-free comp tree has shape
+`f ≫ (g ≫ (h ≫ ...))`: every left argument is a non-comp non-identity,
+and the last right argument is a non-identity. -/
 partial def isNormalizedComp (e : Expr) : Bool :=
+  let e := e.consumeMData
   if e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 then
     let f := e.appFn!.appArg!
     let g := e.appArg!
@@ -68,117 +79,28 @@ partial def isNormalizedComp (e : Expr) : Bool :=
   else
     true
 
-/-- Reduce `t` to the canonical `@Quiver.Hom V _ X Y` shape and return
-`(X, Y)`. Returns `none` if `t` does not whnf to a `Quiver.Hom`
-application — e.g. because of a non-reducible user-defined morphism
-type, or because some implicit could not be elaborated. -/
-def extractHomEndpoints (t : Expr) : MetaM (Option (Expr × Expr)) := do
-  -- Reduce just far enough to expose a `Quiver.Hom` head — using default
-  -- transparency so ordinary `def`-aliases unfold, but stopping at
-  -- `Quiver.Hom` so we don't accidentally unfold the projection itself.
-  let some t ← withDefault <| whnfUntil t ``Quiver.Hom | return none
-  unless t.isAppOfArity ``Quiver.Hom 4 do return none
-  let args := t.getAppArgs
-  return some (args[2]!, args[3]!)
-
-/-- Build the term `f ≫ g` given the two morphism arguments and a
-"comp shell" `e0` from which we copy the `comp` head (with its
-universe levels, category, and category-struct instance).
-
-Returns `none` if the source/middle/target objects cannot be extracted
-from `f`'s and `g`'s types — i.e. if either type fails to whnf to a
-`Quiver.Hom` application. In that case the caller should skip rewriting. -/
-def mkCompFromShell (e0 : Expr) (f g : Expr) : MetaM (Option Expr) := do
-  let some (X', Y') ← extractHomEndpoints (← inferType f) | return none
-  let some (_, Z') ← extractHomEndpoints (← inferType g) | return none
-  let args := e0.getAppArgs
-  let C := args[0]!
-  let inst := args[1]!
-  -- Reuse the original `comp` head from `e0` to preserve maximal sharing.
-  return some (mkAppN e0.getAppFn #[C, inst, X', Y', Z', f, g])
-
-/-- Normalize a morphism expression to right-associated identity-free
-form. Returns `(e', proof?)` where:
-- `e' = e` (semantically)
-- `e'` is right-associated and identity-free
-- `proof?` is `some p` with `p : e = e'`, or `none` if `e = e'` syntactically.
--/
-partial def normalizeComp (e : Expr) : MetaM (Expr × Option Expr) := do
-  unless e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 do
-    return (e, none)
-  -- e = a ≫ b
-  let a := e.appFn!.appArg!
-  let b := e.appArg!
-  -- recurse on children first
-  let (a', aProof?) ← normalizeComp a
-  let (b', bProof?) ← normalizeComp b
-  -- Build (potentially) an updated comp `a' ≫ b'` with proof e = a' ≫ b'.
-  let (e1, e1Proof?) ← do
-    if aProof?.isNone && bProof?.isNone then
-      pure (e, none)
-    else
-      let some e1 ← mkCompFromShell e a' b' | return (e, none)
-      -- proof: a ≫ b = a' ≫ b'
-      let aP := aProof?.getD (← mkEqRefl a)
-      let bP := bProof?.getD (← mkEqRefl b)
-      -- e = `comp C inst X Y Z f g`, so e.appFn!.appFn! = `comp C inst X Y Z`,
-      -- which is the binary function we are applying congruence to.
-      let proof ← mkCongrArg₂ e.appFn!.appFn! aP bP
-      pure (e1, some proof)
-  -- Now consider `a' ≫ b'` (which is e1). Apply local rewrites.
-  -- Identity left: 𝟙 X ≫ b' = b'
-  if isIdMorphism a' then
-    let p ← mkAppM ``CategoryTheory.Category.id_comp #[b']
-    let proof ← combineProofs e1Proof? p
-    return (b', some proof)
-  -- Identity right: a' ≫ 𝟙 Y = a'
-  if isIdMorphism b' then
-    let p ← mkAppM ``CategoryTheory.Category.comp_id #[a']
-    let proof ← combineProofs e1Proof? p
-    return (a', some proof)
-  -- Reassociation: (x ≫ y) ≫ b' = x ≫ (y ≫ b'), then recurse on x ≫ (y ≫ b')
-  if a'.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 then
-    let x := a'.appFn!.appArg!
-    let y := a'.appArg!
-    let p ← mkAppM ``CategoryTheory.Category.assoc #[x, y, b']
-    -- new shape: x ≫ (y ≫ b')
-    let some yb' ← mkCompFromShell e y b' | return (e1, e1Proof?)
-    let some new ← mkCompFromShell e x yb' | return (e1, e1Proof?)
-    -- now recursively normalize `new`
-    let (newNorm, newNormProof?) ← normalizeComp new
-    let combined ←
-      match e1Proof?, newNormProof? with
-      | none, none => pure p
-      | some e1p, none => mkAppM ``Eq.trans #[e1p, p]
-      | none, some np => mkAppM ``Eq.trans #[p, np]
-      | some e1p, some np => do
-        let t1 ← mkAppM ``Eq.trans #[e1p, p]
-        mkAppM ``Eq.trans #[t1, np]
-    return (newNorm, some combined)
-  -- Otherwise, a' is a leaf and b' is either a leaf or already normalized comp.
-  return (e1, e1Proof?)
-where
-  combineProofs (first : Option Expr) (second : Expr) : MetaM Expr := do
-    match first with
-    | none => return second
-    | some p => mkAppM ``Eq.trans #[p, second]
-  mkCongrArg₂ (f : Expr) (ha : Expr) (hb : Expr) : MetaM Expr := do
-    -- Build a proof that f a b = f a' b' given ha : a = a', hb : b = b'.
-    -- Use mkCongr: mkCongr (mkCongrArg f ha) hb gives f a b = f a' b'.
-    let step1 ← mkCongrArg f ha
-    mkCongr step1 hb
-
-/-- The propagator body. -/
+/-- The propagator body. Fires on every `CategoryStruct.comp` term
+`grind` internalises; if `e` is not already in right-associated
+identity-free form, asks `simp` to normalise it and pushes the
+resulting equality into the e-graph. -/
 def catCompPropagatorImpl (e : Expr) : Grind.GoalM Unit := do
-  trace[grind.catNorm] "fire on: {e}"
   unless e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 do return ()
-  if isNormalizedComp e then
-    trace[grind.catNorm] "  skip: already normalized"
-    return ()
-  let (e', proof?) ← normalizeComp e
-  let some proof := proof? | return ()
-  let e' ← Grind.shareCommon e'
-  trace[grind.catNorm] "  normalized to: {e'}"
+  if isNormalizedComp e then return ()
+  trace[grind.catNorm] "normalising: {e}"
+  -- `simp` may fail if the necessary `Category` instance cannot be
+  -- synthesised (e.g. for a bare `CategoryStruct` term). In that case
+  -- we silently skip rather than aborting `grind`.
+  let r ← try
+    simpOnlyNames
+      [``CategoryTheory.Category.id_comp,
+       ``CategoryTheory.Category.comp_id,
+       ``CategoryTheory.Category.assoc] e
+      (config := { decide := false })
+  catch _ => return ()
+  if Lean.Meta.Sym.isSameExpr e r.expr then return ()
+  let e' ← Grind.shareCommon r.expr
+  let proof ← r.getProof' e
+  trace[grind.catNorm] "  ↦ {e'}"
   let gen ← Grind.getGeneration e
   Grind.internalize e' gen (some e)
   Grind.pushEq e e' proof

From 3a79cddc2069eb1fdcef0e881faac3d9e62ae8c8 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 May 2026 03:17:10 +1000
Subject: [PATCH 4/5] refactor(CategoryTheory): tighten the propagator file
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Drop helper `mkCompFromShell`/`extractHomEndpoints`/`combineProofs`
  bookkeeping; everything is one `simpOnlyNames` call.
- Inline `isIdMorphism` into the single structural check.
- Trim the docstring and remove the now-stale caveats section.

No behavioural change. 112 → 81 lines.

🤖 Prepared with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 .../CategoryTheory/Tactic/GrindCatNorm.lean   | 89 ++++++-------------
 1 file changed, 29 insertions(+), 60 deletions(-)

diff --git a/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean b/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
index 62f611d07dc7f1..083e09fa5fd444 100644
--- a/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
+++ b/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
@@ -12,37 +12,25 @@ public import Mathlib.Lean.Meta.Simp
 /-!
 # A `grind` propagator that normalizes morphism composition
 
-This file installs a `grind` upward propagator on
-`CategoryTheory.CategoryStruct.comp` that, every time `grind`
-internalizes a composition `f ≫ g`, pushes the equality
-`f ≫ g = (right-associated form with syntactic identity factors removed)`
+Installs a `grind` upward propagator on `CategoryTheory.CategoryStruct.comp`
+that, every time `grind` internalizes a composition `f ≫ g`, pushes the
+equality `f ≫ g = (right-associated form with identity factors removed)`
 back into the e-graph.
 
 The reason this is a propagator rather than a set of `@[grind]`-tagged
 lemmas: tagging `Category.assoc`, `Category.id_comp`, `Category.comp_id`
 with `@[grind]` causes e-matching to instantiate `Category.assoc` once
-per parenthesization of every composition chain — for a chain of
-length `n` that is Catalan(n − 1) instantiations. The e-graph blows
-up. Mathlib already has the runaway documented at
-`Mathlib/CategoryTheory/Iso.lean:146`. A propagator that commits to a
-single canonical representative per fresh composition avoids the
-blowup: the normalized form is a fixed point of itself, so the
-propagator only does work once per user-visible composition.
-
-The rewrite itself is delegated to `simp` with a three-lemma simp
-set; we only contribute the structural shortcut that recognises
-already-normalised compositions and the glue that feeds the result
-back into `grind`'s e-graph.
-
-## Caveats
-
-- Identity factors are detected *syntactically* by head symbol
-  `CategoryStruct.id`. Opaque or reducible wrappers around `𝟙 _` are
-  treated as atoms and will not be stripped at the shortcut layer
-  (though they may still be normalised by `simp` if it can unfold them).
-- If a composition's instance argument is `CategoryStruct` without a
-  matching `Category` instance, the lemma applications fail; we catch
-  this and silently skip the rewrite rather than aborting `grind`.
+per parenthesization of every composition chain — for a chain of length
+`n` that is Catalan(n − 1) instantiations. The e-graph blows up. (Mathlib
+already has the runaway documented at
+`Mathlib/CategoryTheory/Iso.lean:146`.) A propagator that commits to a
+single canonical representative per fresh composition avoids the blowup:
+the normalized form is a fixed point of itself, so the propagator only
+does work once per user-visible composition.
+
+The rewrite is delegated to `simp` with a three-lemma simp set
+(`Category.id_comp`, `Category.comp_id`, `Category.assoc`); we just feed
+simp's result back into `grind`'s e-graph.
 -/
 
 @[expose] public section
@@ -53,54 +41,35 @@ open Lean Meta
 
 initialize registerTraceClass `grind.catNorm
 
-/-- Returns `true` iff `e` is `𝟙 _`, i.e. `CategoryStruct.id _ _`. -/
-def isIdMorphism (e : Expr) : Bool :=
-  e.consumeMData.isAppOf ``CategoryTheory.CategoryStruct.id
-
-/-- Cheap structural check: `e` is a `≫` already in right-associated
-form with no identity factors. We use this to short-circuit the
-propagator on terms that are already normalised, avoiding the cost of
-invoking `simp` on every internalised sub-composition.
-
-A right-associated identity-free comp tree has shape
-`f ≫ (g ≫ (h ≫ ...))`: every left argument is a non-comp non-identity,
-and the last right argument is a non-identity. -/
-partial def isNormalizedComp (e : Expr) : Bool :=
-  let e := e.consumeMData
+/-- Cheap syntactic check: `e` is `f ≫ g` already in right-associated
+form with no `𝟙 _` factors. Used to short-circuit before invoking simp. -/
+partial def isNormal (e : Expr) : Bool :=
   if e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 then
-    let f := e.appFn!.appArg!
-    let g := e.appArg!
-    if f.isAppOf ``CategoryTheory.CategoryStruct.comp || isIdMorphism f then
-      false
-    else if g.isAppOf ``CategoryTheory.CategoryStruct.comp then
-      isNormalizedComp g
-    else
-      !isIdMorphism g
+    let l := e.appFn!.appArg!
+    let r := e.appArg!
+    !l.isAppOf ``CategoryTheory.CategoryStruct.comp &&
+    !l.isAppOf ``CategoryTheory.CategoryStruct.id &&
+    !r.isAppOf ``CategoryTheory.CategoryStruct.id &&
+    (!r.isAppOf ``CategoryTheory.CategoryStruct.comp || isNormal r)
   else
     true
 
-/-- The propagator body. Fires on every `CategoryStruct.comp` term
-`grind` internalises; if `e` is not already in right-associated
-identity-free form, asks `simp` to normalise it and pushes the
-resulting equality into the e-graph. -/
+/-- The propagator body. -/
 def catCompPropagatorImpl (e : Expr) : Grind.GoalM Unit := do
   unless e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 do return ()
-  if isNormalizedComp e then return ()
-  trace[grind.catNorm] "normalising: {e}"
-  -- `simp` may fail if the necessary `Category` instance cannot be
-  -- synthesised (e.g. for a bare `CategoryStruct` term). In that case
-  -- we silently skip rather than aborting `grind`.
+  if isNormal e then return ()
+  -- `simp` may throw if no `Category` instance is available for the
+  -- composition's `CategoryStruct`; we silently skip in that case.
   let r ← try
     simpOnlyNames
       [``CategoryTheory.Category.id_comp,
        ``CategoryTheory.Category.comp_id,
-       ``CategoryTheory.Category.assoc] e
-      (config := { decide := false })
+       ``CategoryTheory.Category.assoc] e (config := { decide := false })
   catch _ => return ()
   if Lean.Meta.Sym.isSameExpr e r.expr then return ()
+  trace[grind.catNorm] "{e} ↦ {r.expr}"
   let e' ← Grind.shareCommon r.expr
   let proof ← r.getProof' e
-  trace[grind.catNorm] "  ↦ {e'}"
   let gen ← Grind.getGeneration e
   Grind.internalize e' gen (some e)
   Grind.pushEq e e' proof

From 998032a1c160a8601834de7a83405115db68af97 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 21 May 2026 03:22:06 +1000
Subject: [PATCH 5/5] refactor: tidy up the grind cat-comp propagator
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Second-opinion review nits:
- `isNormal` now uses `match_expr` rather than `isAppOfArity` + positional
  `appFn!.appArg!`/`appArg!` accesses.
- The `catch _` around the `simp` call now logs the exception under
  `trace.grind.catNorm` so future failures aren't silently swallowed.
- Stale comment on the reducible-alias test ("reduces the inferred type
  until it hits Quiver.Hom" — that path no longer exists) replaced with
  a concise one-liner.

🤖 Prepared with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean | 15 ++++++++-------
 MathlibTest/CategoryTheory/GrindCatNorm.lean    |  5 ++---
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean b/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
index 083e09fa5fd444..6ca1db3844311f 100644
--- a/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
+++ b/Mathlib/CategoryTheory/Tactic/GrindCatNorm.lean
@@ -44,28 +44,29 @@ initialize registerTraceClass `grind.catNorm
 /-- Cheap syntactic check: `e` is `f ≫ g` already in right-associated
 form with no `𝟙 _` factors. Used to short-circuit before invoking simp. -/
 partial def isNormal (e : Expr) : Bool :=
-  if e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 then
-    let l := e.appFn!.appArg!
-    let r := e.appArg!
+  match_expr e with
+  | CategoryTheory.CategoryStruct.comp _ _ _ _ _ l r =>
     !l.isAppOf ``CategoryTheory.CategoryStruct.comp &&
     !l.isAppOf ``CategoryTheory.CategoryStruct.id &&
     !r.isAppOf ``CategoryTheory.CategoryStruct.id &&
     (!r.isAppOf ``CategoryTheory.CategoryStruct.comp || isNormal r)
-  else
-    true
+  | _ => true
 
 /-- The propagator body. -/
 def catCompPropagatorImpl (e : Expr) : Grind.GoalM Unit := do
   unless e.isAppOfArity ``CategoryTheory.CategoryStruct.comp 7 do return ()
   if isNormal e then return ()
   -- `simp` may throw if no `Category` instance is available for the
-  -- composition's `CategoryStruct`; we silently skip in that case.
+  -- composition's `CategoryStruct`; we silently skip in that case but
+  -- trace the exception so future regressions aren't invisible.
   let r ← try
     simpOnlyNames
       [``CategoryTheory.Category.id_comp,
        ``CategoryTheory.Category.comp_id,
        ``CategoryTheory.Category.assoc] e (config := { decide := false })
-  catch _ => return ()
+  catch ex =>
+    trace[grind.catNorm] "skipped: {ex.toMessageData}"
+    return ()
   if Lean.Meta.Sym.isSameExpr e r.expr then return ()
   trace[grind.catNorm] "{e} ↦ {r.expr}"
   let e' ← Grind.shareCommon r.expr
diff --git a/MathlibTest/CategoryTheory/GrindCatNorm.lean b/MathlibTest/CategoryTheory/GrindCatNorm.lean
index 42df94b8015034..c75ae8e0b118a2 100644
--- a/MathlibTest/CategoryTheory/GrindCatNorm.lean
+++ b/MathlibTest/CategoryTheory/GrindCatNorm.lean
@@ -70,9 +70,8 @@ end WithHypotheses
 
 section ReducibleAliases
 
-/-- A reducible alias for the morphism type, even with object arguments
-swapped, should still be handled. The propagator reduces the inferred
-type until it hits `Quiver.Hom` and extracts the endpoints from there. -/
+/-- A reducible alias for the morphism type should not hide the
+underlying composition head from the propagator. -/
 private def MorAlias (Y X : C) := X ⟶ Y
 
 example {X Y Z W : C} (f : MorAlias Y X) (g : MorAlias Z Y) (h : MorAlias W Z) :