From 10df4f9f7a64a24c2c74731f9dc49e2d6f008b18 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Mon, 3 Nov 2025 23:30:58 -0600 Subject: Remove unnecessary import --- Functor/Monoidal/Instance/Nat/Push.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Functor/Monoidal/Instance/Nat/Push.agda') 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) -- cgit v1.2.3