Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

+Commutative monads #402

Closed
wants to merge 1 commit into from
Closed

+Commutative monads #402

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 9 additions & 2 deletions src/Categories/Category/Product/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ module _ (C : Category o ℓ e) (D : Category o′ ℓ′ e′) where
※-distrib F G H = record
{ F⇒G = ntHelper record { η = λ _ → C×D.id ; commute = λ _ → MR.id-comm-sym C , MR.id-comm-sym D }
; F⇐G = ntHelper record { η = λ _ → C×D.id ; commute = λ _ → MR.id-comm-sym C , MR.id-comm-sym D }
; iso = λ X → record
; iso = λ _ → record
{ isoˡ = C.identityˡ , D.identityˡ
; isoʳ = C.identityʳ , D.identityʳ
}
Expand All @@ -102,5 +102,12 @@ module _ (C : Category o ℓ e) (D : Category o′ ℓ′ e′) where
※-distrib₂ F G = record
{ F⇒G = ntHelper record { η = λ X → C.id , D.id ; commute = λ _ → MR.id-comm-sym C , MR.id-comm-sym D }
; F⇐G = ntHelper record { η = λ X → C.id , D.id ; commute = λ _ → MR.id-comm-sym C , MR.id-comm-sym D }
; iso = λ X → record { isoˡ = C.identityˡ , D.identityʳ ; isoʳ = C.identityʳ , D.identityʳ }
; iso = λ _ → record { isoˡ = C.identityˡ , D.identityʳ ; isoʳ = C.identityʳ , D.identityʳ }
}

SwapFG≅FGSwap : {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ : Level} {A : Category o₁ ℓ₁ e₁} {B : Category o₂ ℓ₂ e₂}
→ (F : Functor B D) → (G : Functor A C) → Swap ∘F (F ⁂ G) ≃ (G ⁂ F) ∘F Swap

NaturalIsomorphism.F⇒G (SwapFG≅FGSwap F G) = ntHelper record { η = λ _ → C×D.id ; commute = λ _ → MR.id-comm-sym C×D}
NaturalIsomorphism.F⇐G (SwapFG≅FGSwap F G) = ntHelper record { η = λ _ → C×D.id ; commute = λ _ → MR.id-comm-sym C×D}
NaturalIsomorphism.iso (SwapFG≅FGSwap F G) = λ _ → record { isoˡ = C.identityˡ , D.identityˡ ; isoʳ = C.identityˡ , D.identityˡ }
36 changes: 36 additions & 0 deletions src/Categories/Monad/Commutative.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
{-# OPTIONS --without-K --safe #-}

open import Level
open import Data.Product using (_,_)

open import Categories.Category
open import Categories.Category.Monoidal
open import Categories.Monad
open import Categories.Monad.Strong
open import Categories.Category.Monoidal.Symmetric
open import Categories.Functor using (Functor; Endofunctor; _∘F_) renaming (id to idF)

open import Categories.NaturalTransformation using (NaturalTransformation)

module Categories.Monad.Commutative {o ℓ e} {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) (SM : StrongMonad S) where

private
module M = StrongMonad.M SM
module τ = StrongMonad.strengthen SM
module τ' = StrongMonad.strengthen' SM

open NaturalTransformation
open Category C
open Monoidal V

open NaturalTransformation M.η using (η)
open NaturalTransformation M.μ renaming (η to μ)

open M using (F)
open Functor F

record Commutative : Set (o ⊔ ℓ ⊔ e) where
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder if Commutative should be a simple property rather than a record ? There are certainly times where a one-field record is much nicer (both to help Agda with inference, and to get a nice projector name), I'm not sure here?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just copycatted /src/Categories/Monad/Idempotent.agda

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Which was the right thing to do. I didn't think of asking the question about that one - such are the vagaries of code reviews done by humans, you don't catch everything every time.

field
commutativity : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (τ'.η (A , B)) ∘ τ.η (F₀ A , B)
≈ μ (A ⊗₀ B) ∘ F₁ (τ.η (A , B)) ∘ τ'.η (A , F₀ B)

34 changes: 29 additions & 5 deletions src/Categories/Monad/Strong.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,27 +14,51 @@ open import Data.Product using (_,_)
open import Categories.Category
open import Categories.Functor renaming (id to idF)
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Symmetric
open import Categories.Category.Monoidal.Braided

open import Categories.Category.Product
open import Categories.Category.Product.Properties
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.NaturalIsomorphism renaming (associator to ∘-assoc)
open import Categories.Monad

private
variable
o ℓ e : Level

record Strength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where
record Strength {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't it the case that there are different concepts of Strength depending on whether the underlying category is Symmetric or not? So there should be two notions of Strength rather than requiring Symmetric V?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that was too crude. We can have left-strong monads over non-symmetric V.

open Category C
open Monoidal V

private
module M = Monad M

open M using (F)
open NaturalTransformation M.η using (η)
open NaturalTransformation M.μ renaming (η to μ)
open Functor F
open Symmetric S using (braided)
open NaturalIsomorphism using (F⇐G; F⇒G)

private
γ = Braided.braiding.F⇒G braided
γ⁻¹ = Braided.braiding.F⇐G braided

field
strengthen : NaturalTransformation (⊗ ∘F (idF ⁂ F)) (F ∘F ⊗)

module strengthen = NaturalTransformation strengthen
-- dual strength
strengthen' : NaturalTransformation (⊗ ∘F (F ⁂ idF)) (F ∘F ⊗)
strengthen' = (F ∘ˡ γ⁻¹) ∘ᵥ F⇒G (∘-assoc Swap ⊗ F) ∘ᵥ (strengthen ∘ʳ Swap) ∘ᵥ
F⇐G (∘-assoc Swap (idF ⁂ F) ⊗) ∘ᵥ
(⊗ ∘ˡ F⇒G (SwapFG≅FGSwap C C F idF)) ∘ᵥ
F⇒G (∘-assoc (F ⁂ idF) Swap ⊗) ∘ᵥ
(γ ∘ʳ (F ⁂ idF))

module strengthen = NaturalTransformation strengthen
module strengthen' = NaturalTransformation strengthen'

private
module t = strengthen

Expand All @@ -48,12 +72,12 @@ record Strength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o
≈ t.η (A , B) ∘ id ⊗₁ μ B
-- consecutive applications of strength commute (i.e. strength is associative)
strength-assoc : {A B C : Obj} → F₁ associator.from ∘ t.η (A ⊗₀ B , C)
≈ t.η (A , B ⊗₀ C) ∘ id ⊗₁ t.η (B , C) ∘ associator.from
≈ t.η (A , B ⊗₀ C) ∘ id ⊗₁ t.η (B , C) ∘ associator.from

record StrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where
record StrongMonad {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) : Set (o ⊔ ℓ ⊔ e) where
field
M : Monad C
strength : Strength V M
strength : Strength S M

module M = Monad M
open Strength strength public