commit d7d6dda79811ccefdfb3cf54e0542db119bb8100 Author: Leon Vatthauer Date: Sun Jul 23 17:28:18 2023 +0200 initial commit diff --git a/Monads.agda b/Monads.agda new file mode 100644 index 0000000..b84c607 --- /dev/null +++ b/Monads.agda @@ -0,0 +1,203 @@ +module Monads where + +open import Level +open import Categories.Category +open import Categories.Monad +open import Categories.Object.Terminal +open import Categories.Object.Exponential +open import Categories.Functor renaming (id to idF) +open import Categories.Category.Cocartesian.Bundle +open import Categories.Category.CartesianClosed +open import Categories.Category.Cartesian +open import Categories.Category.BinaryProducts +open import Categories.Category.CartesianClosed.Bundle +open import Categories.NaturalTransformation renaming (id to idN) +open import Function using (_$_) + +module _ (o ℓ e : Level) where + + + --* + -- Exception monad TX = X + E + --* + + + ExceptionMonad : (C : CocartesianCategory o ℓ e) → CocartesianCategory.Obj C → Monad (CocartesianCategory.U C) + ExceptionMonad CC E = record + { F = F + ; η = η' + ; μ = μ' + ; assoc = assoc' + ; sym-assoc = λ {X} → sym assoc' + ; identityˡ = begin + [ id , i₂ ] ∘ (i₁ +₁ id) ≈⟨ []∘+₁ ⟩ + [ id ∘ i₁ , i₂ ∘ id ] ≈⟨ []-cong₂ identityˡ identityʳ ⟩ + [ i₁ , i₂ ] ≈⟨ +-η ⟩ + id ∎ + ; identityʳ = inject₁ + } + where + open CocartesianCategory CC renaming (U to C) + open HomReasoning + open Equiv + F : Endofunctor C + F = record + { F₀ = λ X → X + E + ; F₁ = λ f → f +₁ id + ; identity = λ {A} → begin + id +₁ id ≈⟨ sym identityˡ ⟩ + (id ∘ (id +₁ id)) ≈⟨ ∘-resp-≈ˡ (sym +-η) ⟩ + ([ i₁ , i₂ ] ∘ (id +₁ id)) ≈⟨ []∘+₁ ⟩ + [ i₁ ∘ id , i₂ ∘ id ] ≈⟨ []-cong₂ identityʳ identityʳ ⟩ + [ i₁ , i₂ ] ≈⟨ +-η ⟩ + id ∎ + ; homomorphism = λ {X} {Y} {Z} {f} {g} → begin + g ∘ f +₁ id ≈⟨ sym (+₁-cong₂ refl identity²) ⟩ + (g ∘ f +₁ id ∘ id) ≈⟨ sym +₁∘+₁ ⟩ + ((g +₁ id) ∘ (f +₁ id)) ∎ + ; F-resp-≈ = λ {A B f g} fg → +₁-cong₂ fg refl + } + open Functor F + η' : NaturalTransformation idF F + η' = ntHelper record + { η = λ X → i₁ + ; commute = λ {X Y} f → sym +₁∘i₁ + } + open NaturalTransformation η' + μ' : NaturalTransformation (F ∘F F) F + μ' = ntHelper record + { η = λ X → [ id , i₂ ] + ; commute = λ {X Y} f → begin + ([ id , i₂ ] ∘ ((f +₁ id) +₁ id)) ≈⟨ []∘+₁ ⟩ + [ id ∘ (f +₁ id) , i₂ ∘ id ] ≈⟨ []-cong₂ identityˡ identityʳ ⟩ + [ f +₁ id , i₂ ] ≈⟨ []-congˡ (sym identityʳ) ⟩ + [ f +₁ id , i₂ ∘ id ] ≈⟨ sym ([]-cong₂ identityʳ +₁∘i₂) ⟩ + [ (f +₁ id) ∘ id , (f +₁ id) ∘ i₂ ] ≈⟨ sym ∘[] ⟩ + ((f +₁ id) ∘ [ id , i₂ ]) ∎ + } + open NaturalTransformation μ' renaming (η to μ) + assoc' : ∀ {X : Obj} → μ X ∘ F₁ (μ X) ≈ μ X ∘ μ (F₀ X) + assoc' {X} = begin + [ id , i₂ ] ∘ ([ id , i₂ ] +₁ id) ≈⟨ []∘+₁ ⟩ + [ id ∘ [ id , i₂ ] , i₂ ∘ id ] ≈⟨ []-cong₂ identityˡ identityʳ ⟩ + [ [ id , i₂ ] , i₂ ] ≈⟨ sym ([]-cong₂ identityʳ inject₂) ⟩ + [ [ id , i₂ ] ∘ id , [ id , i₂ ] ∘ i₂ ] ≈⟨ sym (∘[]) ⟩ + [ id , i₂ ] ∘ [ id , i₂ ] ∎ + + -- Maybe monad as special case of exception monad + MaybeMonad : (C : CocartesianCategory o ℓ e) → Terminal (CocartesianCategory.U C) → Monad (CocartesianCategory.U C) + MaybeMonad C T = ExceptionMonad C (Terminal.⊤ T) + + + --* + -- Reader monad TX = X^S + --* + + + ReaderMonad : (CCC : CartesianClosedCategory o ℓ e) → CartesianClosedCategory.Obj CCC → Monad (CartesianClosedCategory.U CCC) + ReaderMonad CCC S = record + { F = F + ; η = η' + ; μ = μ' + ; assoc = assoc' + ; sym-assoc = λ {X} → sym assoc' + ; identityˡ = λ {X} → begin + (λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ (λg ((λg π₁) ∘ eval′)) ≈⟨ exp.subst product product ⟩ + λg ((eval′ ∘ ⟨ eval′ , π₂ ⟩) ∘ ((λg ((λg π₁) ∘ eval′)) ⁂ id)) ≈⟨ λ-cong assoc ⟩ + λg (eval′ ∘ (⟨ eval′ , π₂ ⟩ ∘ ((λg ((λg π₁) ∘ eval′)) ⁂ id))) ≈⟨ λ-cong (∘-resp-≈ʳ ⟨⟩∘) ⟩ + λg (eval′ ∘ (⟨ eval′ ∘ ((λg ((λg π₁) ∘ eval′)) ⁂ id) , π₂ ∘ ((λg ((λg π₁) ∘ eval′)) ⁂ id) ⟩)) ≈⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-cong₂ β′ π₂∘⁂)) ⟩ + λg (eval′ ∘ ⟨ (λg π₁) ∘ eval′ , id ∘ π₂ ⟩) ≈⟨ λ-cong (∘-resp-≈ʳ (sym ⁂∘⟨⟩)) ⟩ + λg (eval′ ∘ (((λg π₁) ⁂ id) ) ∘ ⟨ eval′ , π₂ ⟩) ≈⟨ λ-cong sym-assoc ⟩ + λg ((eval′ ∘ (((λg π₁) ⁂ id) )) ∘ ⟨ eval′ , π₂ ⟩) ≈⟨ λ-cong (∘-resp-≈ˡ β′) ⟩ + λg (π₁ ∘ ⟨ eval′ , π₂ ⟩) ≈⟨ λ-cong project₁ ⟩ + λg eval′ ≈⟨ η-id′ ⟩ + id ∎ + ; identityʳ = λ {X} → begin + (λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ λg π₁ ≈⟨ exp.subst product product ⟩ + λg ((eval′ ∘ ⟨ eval′ , π₂ ⟩) ∘ ((λg π₁) ⁂ id)) ≈⟨ λ-cong assoc ⟩ + λg (eval′ ∘ (⟨ eval′ , π₂ ⟩ ∘ ((λg π₁) ⁂ id))) ≈⟨ λ-cong (∘-resp-≈ʳ ⟨⟩∘) ⟩ + λg (eval′ ∘ ⟨ eval′ ∘ ((λg π₁) ⁂ id) , π₂ ∘ ((λg π₁) ⁂ id) ⟩) ≈⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-cong₂ β′ π₂∘⁂)) ⟩ + λg (eval′ ∘ ⟨ π₁ , id ∘ π₂ ⟩) ≈⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-congˡ identityˡ)) ⟩ + λg (eval′ ∘ ⟨ π₁ , π₂ ⟩) ≈⟨ λ-cong (∘-resp-≈ʳ p-η) ⟩ + λg (eval′ ∘ id) ≈⟨ λ-cong identityʳ ⟩ + λg eval′ ≈⟨ η-id′ ⟩ + id ∎ + } + where + open CartesianClosedCategory CCC renaming (U to C) + open CartesianClosed cartesianClosed + open Cartesian cartesian + open BinaryProducts products renaming (η to p-η) + open HomReasoning + open Equiv + F = record + { F₀ = λ X → X ^ S + ; F₁ = λ {A B} f → λg (f ∘ eval′) + ; identity = λ {A} → begin + λg (id ∘ eval′) ≈⟨ λ-cong identityˡ ⟩ + λg eval′ ≈⟨ η-id′ ⟩ + id ∎ + ; homomorphism = λ {X Y Z f g } → begin + λg ((g ∘ f) ∘ eval′) ≈⟨ λ-cong assoc ⟩ + λg (g ∘ (f ∘ eval′)) ≈⟨ sym (λ-cong (∘-resp-≈ʳ β′)) ⟩ + λg (g ∘ (eval′ ∘ ((λg (f ∘ eval′)) ⁂ id))) ≈⟨ sym (λ-cong assoc) ⟩ + λg ((g ∘ eval′) ∘ ((λg (f ∘ eval′)) ⁂ id)) ≈⟨ sym (exp.subst product product) ⟩ + (λg (g ∘ eval′)) ∘ (λg (f ∘ eval′)) ∎ + ; F-resp-≈ = λ {A B f g} fg → λ-cong (∘-resp-≈ˡ fg) + } + open Functor F + η' = ntHelper record + { η = λ X → λg π₁ + ; commute = λ {X Y} f → sym $ begin + (λg (f ∘ eval′)) ∘ λg π₁ ≈⟨ exp.subst product product ⟩ + λg ((f ∘ eval′) ∘ (λg π₁ ⁂ id)) ≈⟨ λ-cong assoc ⟩ + λg (f ∘ (eval′ ∘ (λg π₁ ⁂ id))) ≈⟨ λ-cong (∘-resp-≈ʳ β′) ⟩ + λg (f ∘ π₁) ≈⟨ sym (λ-cong π₁∘⁂) ⟩ + λg (π₁ ∘ (f ⁂ id)) ≈⟨ sym (exp.subst product product) ⟩ + λg π₁ ∘ f ∎ + } + open NaturalTransformation η' + μ' = ntHelper record + { η = λ X → λg (eval′ ∘ ⟨ eval′ , π₂ ⟩) + ; commute = λ {X Y} f → begin + (λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ (λg ((λg (f ∘ eval′)) ∘ eval′)) ≈⟨ ∘-resp-≈ʳ (λ-cong (exp.subst product product)) ⟩ + ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ (λg (λg ((f ∘ eval′) ∘ (eval′ ⁂ id))))) ≈⟨ exp.subst product product ⟩ + λg ((eval′ ∘ ⟨ eval′ , π₂ ⟩) ∘ ((λg (λg ((f ∘ eval′) ∘ (eval′ ⁂ id)))) ⁂ id )) ≈⟨ λ-cong assoc ⟩ + λg (eval′ ∘ (⟨ eval′ , π₂ ⟩ ∘ ((λg (λg ((f ∘ eval′) ∘ (eval′ ⁂ id)))) ⁂ id ))) ≈⟨ λ-cong (∘-resp-≈ʳ ⟨⟩∘) ⟩ + λg (eval′ ∘ (⟨ eval′ ∘ ((λg (λg ((f ∘ eval′) ∘ (eval′ ⁂ id)))) ⁂ id ) , π₂ ∘ ((λg (λg ((f ∘ eval′) ∘ (eval′ ⁂ id)))) ⁂ id ) ⟩)) ≈⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-cong₂ β′ π₂∘⁂)) ⟩ + λg (eval′ ∘ (⟨ λg ((f ∘ eval′) ∘ (eval′ ⁂ id)) , id ∘ π₂ ⟩)) ≈⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-congˡ identityˡ)) ⟩ + λg (eval′ ∘ ⟨ λg ((f ∘ eval′) ∘ (eval′ ⁂ id)) , π₂ ⟩) ≈⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-congʳ (sym (exp.subst product product)))) ⟩ + λg (eval′ ∘ ⟨ λg (f ∘ eval′) ∘ eval′ , π₂ ⟩) ≈⟨ λ-unique′ (( + begin + eval′ ∘ ((λg (eval′ ∘ ⟨ λg (f ∘ eval′) ∘ eval′ , π₂ ⟩)) ⁂ id) ≈⟨ β′ ⟩ + eval′ ∘ ⟨ λg (f ∘ eval′) ∘ eval′ , π₂ ⟩ ≈⟨ ∘-resp-≈ʳ (⟨⟩-congˡ (sym identityˡ)) ⟩ + (eval′ ∘ ⟨ λg (f ∘ eval′) ∘ eval′ , id ∘ π₂ ⟩) ≈⟨ ∘-resp-≈ʳ (sym ⁂∘⟨⟩) ⟩ + eval′ ∘ ( (λg (f ∘ eval′)) ⁂ id ) ∘ ⟨ eval′ , π₂ ⟩ ≈⟨ sym-assoc ⟩ + (eval′ ∘ ( (λg (f ∘ eval′)) ⁂ id )) ∘ ⟨ eval′ , π₂ ⟩ ≈⟨ ∘-resp-≈ˡ β′ ⟩ + (((f ∘ eval′)) ∘ ⟨ eval′ , π₂ ⟩) ≈⟨ assoc ⟩ + f ∘ (eval′ ∘ ⟨ eval′ , π₂ ⟩) ∎ + )) ⟩ + λg (f ∘ (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ≈⟨ sym (λ-cong (∘-resp-≈ʳ β′)) ⟩ + λg (f ∘ (eval′ ∘ ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ⁂ id))) ≈⟨ (λ-cong sym-assoc) ⟩ + λg ((f ∘ eval′) ∘ ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ⁂ id)) ≈⟨ sym (exp.subst product product) ⟩ + (λg (f ∘ eval′)) ∘ λg (eval′ ∘ ⟨ eval′ , π₂ ⟩) ∎ + } + open NaturalTransformation μ' renaming (η to μ) + assoc' : ∀ {X : Obj} → μ X ∘ F₁ (μ X) ≈ μ X ∘ μ (F₀ X) + assoc' {X} = begin + (λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ (λg ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ eval′)) ≈⟨ exp.subst product product ⟩ + λg ((eval′ ∘ ⟨ eval′ , π₂ ⟩) ∘ ((λg ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ eval′)) ⁂ id)) ≈⟨ λ-cong assoc ⟩ + λg (eval′ ∘ (⟨ eval′ , π₂ ⟩ ∘ ((λg ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ eval′)) ⁂ id))) ≈⟨ λ-cong (∘-resp-≈ʳ ⟨⟩∘) ⟩ + λg (eval′ ∘ (⟨ eval′ ∘ ((λg ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ eval′)) ⁂ id) , π₂ ∘ ((λg ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ eval′)) ⁂ id) ⟩)) ≈⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-cong₂ β′ π₂∘⁂)) ⟩ + λg (eval′ ∘ (⟨ (λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ eval′ , id ∘ π₂ ⟩)) ≈⟨ λ-cong (∘-resp-≈ʳ (sym ⁂∘⟨⟩)) ⟩ + λg (eval′ ∘ (((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ⁂ id) ∘ ⟨ eval′ , π₂ ⟩)) ≈⟨ λ-cong sym-assoc ⟩ + λg ((eval′ ∘ ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ⁂ id)) ∘ ⟨ eval′ , π₂ ⟩) ≈⟨ λ-cong (∘-resp-≈ˡ β′) ⟩ + λg (((eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ ⟨ eval′ , π₂ ⟩) ≈⟨ λ-cong assoc ⟩ + λg (eval′ ∘ ⟨ eval′ , π₂ ⟩ ∘ ⟨ eval′ , π₂ ⟩) ≈⟨ λ-cong (∘-resp-≈ʳ ⟨⟩∘) ⟩ + λg (eval′ ∘ ⟨ eval′ ∘ ⟨ eval′ , π₂ ⟩ , π₂ ∘ ⟨ eval′ , π₂ ⟩ ⟩) ≈⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-congˡ project₂)) ⟩ + λg (eval′ ∘ ⟨ eval′ ∘ ⟨ eval′ , π₂ ⟩ , π₂ ⟩) ≈⟨ λ-cong (∘-resp-≈ʳ (⟨⟩-congˡ (sym identityˡ))) ⟩ + λg (eval′ ∘ ⟨ eval′ ∘ ⟨ eval′ , π₂ ⟩ , id ∘ π₂ ⟩) ≈⟨ sym (λ-cong (∘-resp-≈ʳ (⟨⟩-cong₂ β′ π₂∘⁂))) ⟩ + λg (eval′ ∘ ⟨ eval′ ∘ ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ⁂ id) , π₂ ∘ ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ⁂ id) ⟩) ≈⟨ λ-cong (∘-resp-≈ʳ (sym ⟨⟩∘)) ⟩ + λg (eval′ ∘ ⟨ eval′ , π₂ ⟩ ∘ ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ⁂ id)) ≈⟨ λ-cong sym-assoc ⟩ + λg ((eval′ ∘ ⟨ eval′ , π₂ ⟩) ∘ ((λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ⁂ id)) ≈⟨ sym (exp.subst product product) ⟩ + (λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∘ (λg (eval′ ∘ ⟨ eval′ , π₂ ⟩)) ∎ \ No newline at end of file diff --git a/Monads.agda-lib b/Monads.agda-lib new file mode 100644 index 0000000..fe0c39f --- /dev/null +++ b/Monads.agda-lib @@ -0,0 +1,3 @@ +name: Monads +include: . +depend: agda-categories, standard-library \ No newline at end of file