Update Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean

leanprover-community · Dec 26, 2024 · 6e71693 · 6e71693
1 parent b429049
commit 6e71693
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -256,6 +256,8 @@ variable {F G : Set.Iic j ⥤ C} (hobj : F.obj = G.obj)
 
 omit [OrderBot J] [SuccOrder J] [WellFoundedLT J]
 
+/-- Given two functors `Set.Iic j ⥤ C` that are equal on objects,
+this is the condition that they coincide on a given map. -/
 def MapEq (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j) : Prop :=
   F.map (homOfLE h₁₂ : ⟨i₁, h₁₂.trans h₂⟩ ⟶ ⟨i₂, h₂⟩) =
     eqToHom (by rw [hobj]) ≫