diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-10 17:21:14 -0700 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-07-10 17:21:14 -0700 |
| commit | a408cbee9abbe2dbeee09bd36afc678efe7b6557 (patch) | |
| tree | 22d6f05d6ce81357629fa2864305b81d68eed52e /Functor/Instance/Decorate.agda | |
| parent | 7875edd03cce586a8c9f0b95dedffb390bfdbd61 (diff) | |
Use latest agda-categories
Diffstat (limited to 'Functor/Instance/Decorate.agda')
| -rw-r--r-- | Functor/Instance/Decorate.agda | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/Functor/Instance/Decorate.agda b/Functor/Instance/Decorate.agda index fedddba..8d5aefb 100644 --- a/Functor/Instance/Decorate.agda +++ b/Functor/Instance/Decorate.agda @@ -23,7 +23,8 @@ import Categories.Morphism.Reasoning as ⇒-Reasoning import Category.Diagram.Cospan 𝒞 as Cospan open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) -open import Categories.Category.Cocartesian using (module CocartesianMonoidal) +open import Categories.Category.Monoidal using (module Monoidal) +open import Categories.Category.Cocartesian.Monoidal using (module CocartesianMonoidal) open import Categories.Category.Monoidal.Properties using (coherence-inv₃) open import Categories.Category.Monoidal.Utilities using (module Shorthands) open import Categories.Functor.Core using (Functor) @@ -39,7 +40,7 @@ module 𝒟 = SymmetricMonoidalCategory 𝒟 module F = SymmetricMonoidalFunctor F module Cospans = Category Cospans module DecoratedCospans = Category DecoratedCospans -module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian +module mc𝒞 = CocartesianMonoidal 𝒞.cocartesian -- For every cospan there exists a free decorated cospan -- i.e. the original cospan with the discrete decoration @@ -90,7 +91,7 @@ homomorphism {g} {f} = record open DiagramPushout 𝒞.U using (Pushout) open Pushout (pushout f₂ g₁) using (i₁; i₂) - open mc𝒞 using (unitorˡ) + open Monoidal mc𝒞.+-monoidal using (unitorˡ) open unitorˡ using () renaming (to to λ⇐′) same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ F.ε ≈ F₁ [ i₁ , i₂ ]′ ∘ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ @@ -147,7 +148,7 @@ Decorate-resp-⊗ {f} {g} = record open F.⊗-homo using () renaming (η to φ; commute to φ-commute) open F using (F₁; ε) open Shorthands monoidal - open mc𝒞 using (unitorˡ) + open Monoidal mc𝒞.+-monoidal using (unitorˡ) open unitorˡ using () renaming (to to λ⇐′) same-deco : F₁ 𝒞.id ∘ F₁ ¡ ∘ ε ≈ φ (N , M) ∘ (F₁ ¡ ∘ ε) ⊗₁ (F₁ ¡ ∘ ε) ∘ ρ⇐ |