diff options
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) |