Skip to content

Commit 8952828

Browse files
committed
Add missing import
1 parent 2b8ae18 commit 8952828

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Categories/Diagram/End/Parameterized.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ open import Categories.Category
99
open import Categories.Category.Construction.Functors
1010
open import Categories.Category.Product renaming (Product to _×ᶜ_)
1111
open import Categories.Diagram.End renaming (End to ∫)
12+
open import Categories.Diagram.End.Limit
1213
open import Categories.Diagram.End.Properties
1314
open import Categories.Diagram.Wedge
1415
open import Categories.Functor hiding (id)

0 commit comments

Comments
 (0)