Add missing import

agda · Feb 22, 2025 · 8952828 · 8952828
1 parent 2b8ae18
commit 8952828
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Categories/Diagram/End/Parameterized.agda b/src/Categories/Diagram/End/Parameterized.agda
@@ -9,6 +9,7 @@ open import Categories.Category
 open import Categories.Category.Construction.Functors
 open import Categories.Category.Product renaming (Product to _×ᶜ_)
 open import Categories.Diagram.End renaming (End to ∫)
+open import Categories.Diagram.End.Limit
 open import Categories.Diagram.End.Properties
 open import Categories.Diagram.Wedge
 open import Categories.Functor hiding (id)