diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-11-03 23:30:58 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-11-03 23:30:58 -0600 |
| commit | 10df4f9f7a64a24c2c74731f9dc49e2d6f008b18 (patch) | |
| tree | 7de3ef4a2eb1d136402c8e8238cd071787341d3d /Functor/Monoidal/Instance | |
| parent | 298baf2b69620106e95b52206e02d58ad8cb9fc8 (diff) | |
Remove unnecessary import
Diffstat (limited to 'Functor/Monoidal/Instance')
| -rw-r--r-- | Functor/Monoidal/Instance/Nat/Push.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Functor/Monoidal/Instance/Nat/Push.agda b/Functor/Monoidal/Instance/Nat/Push.agda index 30ed745..667d68e 100644 --- a/Functor/Monoidal/Instance/Nat/Push.agda +++ b/Functor/Monoidal/Instance/Nat/Push.agda @@ -20,7 +20,7 @@ open import Categories.Category.Cartesian using (Cartesian) open Cartesian (Setoids-Cartesian {0ℓ} {0ℓ}) using (products) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) open import Categories.Category.Instance.Nat using (Nat-Cocartesian) -open import Categories.Category.Cocartesian using (Cocartesian; module BinaryCoproducts) +open import Categories.Category.Cocartesian using (Cocartesian) open import Categories.Category.Product using (_⁂_) open import Categories.Functor using () renaming (_∘F_ to _∘′_) open Cocartesian Nat-Cocartesian using (module Dual; i₁; i₂; -+-; _+₁_; +-assoc; +-assocʳ; +-assocˡ; +-comm; +-swap; +₁∘+-swap) |