From 113ae4259ea3a76ceae5d083de745178e675201f Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Fri, 16 Feb 2024 14:35:59 +0100 Subject: [PATCH] minor --- Monads-Sets.agda | 195 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 195 insertions(+) create mode 100644 Monads-Sets.agda diff --git a/Monads-Sets.agda b/Monads-Sets.agda new file mode 100644 index 0000000..715d6d0 --- /dev/null +++ b/Monads-Sets.agda @@ -0,0 +1,195 @@ +module Monads-Sets where + +open import Level +open import Categories.Category.Instance.Sets +open import Categories.Category +open import Categories.Monad +open import Categories.Category.Cartesian +open import Categories.Category.CartesianClosed.Canonical +open import Categories.Category.BinaryProducts +open import Categories.Object.Exponential +open import Categories.Object.Product +open import Categories.Object.Terminal +open import Categories.Functor renaming (id to idF) +open import Categories.Category.Cocartesian +open import Categories.NaturalTransformation renaming (id to idN) +open import Data.Unit.Polymorphic +open import Data.Empty.Polymorphic +open import Data.Product +open import Data.Product.Properties using (×-≡,≡↔≡) +open import Data.Sum +open import Data.Sum.Properties +open import Function.Base renaming (_∘_ to _∘f_) +open import Axiom.Extensionality.Propositional +import Relation.Binary.PropositionalEquality as Eq +open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst) + +module _ (o ℓ e : Level) (ext : Extensionality o o) where + + -- helpers + ,-resp-≡ : ∀ {ℓ : Level} {A B : Set ℓ} {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : A × B} → (a₁ ≡ a₂ × b₁ ≡ b₂) → p₁ ≡ p₂ + ,-resp-≡ (refl , refl) = refl + inj₁-resp-≡ : ∀ {ℓ} {A B : Set ℓ} {c1 c2 : A} → (c1 ≡ c2) → (inj₁ {B = B} c1 ≡ inj₁ {B = B} c2) + inj₁-resp-≡ refl = refl + inj₂-resp-≡ : ∀ {ℓ} {A B : Set ℓ} {c1 c2 : B} → (c1 ≡ c2) → (inj₂ {A = A} c1 ≡ inj₂ {A = A} c2) + inj₂-resp-≡ refl = refl + + --* + -- Sets is cartesian(closed) and cocartesian + --* + + SetsCartesian : Cartesian (Sets o) + SetsCartesian = record + { terminal = record + { ⊤ = ⊤ + ; ⊤-is-terminal = record + { ! = λ {A} _ → tt + ; !-unique = λ f → refl + } + } + ; products = record + { product = λ {A} {B} → record + { A×B = A × B + ; π₁ = proj₁ + ; π₂ = proj₂ + ; ⟨_,_⟩ = <_,_> + ; project₁ = refl + ; project₂ = refl + ; unique = λ p1 p2 → sym (,-resp-≡ (p1 , p2)) + } + } + } + + SetsCocartesian : Cocartesian (Sets o) + SetsCocartesian = record + { initial = record + { ⊥ = ⊥ + ; ⊥-is-initial = record + { ! = ⊥-elim + ; !-unique = λ {A} f {x} → ⊥-elim {Whatever = λ y → ⊥-elim y ≡ f y} x + } + } + ; coproducts = record + { coproduct = λ {A} {B} → record + { A+B = A ⊎ B + ; i₁ = inj₁ + ; i₂ = inj₂ + ; [_,_] = [_,_] + ; inject₁ = refl + ; inject₂ = refl + ; unique = λ p1 p2 → λ where + {inj₁ x} → sym $ p1 {x} + {inj₂ x} → sym $ p2 {x} + } + } + } + + SetsCCC : CartesianClosed (Sets o) + SetsCCC = record + { ⊤ = ⊤ + ; _×_ = _×_ + ; ! = ! + ; π₁ = π₁ + ; π₂ = π₂ + ; ⟨_,_⟩ = ⟨_,_⟩ + ; !-unique = !-unique + ; π₁-comp = λ {_ _ f _ g} → project₁ {h = f} {g} + ; π₂-comp = λ {_ _ f _ g} → project₂ {h = f} {g} + ; ⟨,⟩-unique = λ {_ _ _ f g h} → unique {h = h} {f} {g} + ; _^_ = λ X Y → Y → X + ; eval = λ {X Y} (f , y) → f y + ; curry = λ {C A B} f c a → f (c ,′ a) + ; eval-comp = λ {A} {B} {C} {f} {x} → refl + ; curry-unique = λ {A} {B} {C} {f} {g} fg {x} → ext λ y → fg + } + where + open Category (Sets o) + open Cartesian SetsCartesian + open HomReasoning + --open BinaryProducts products renaming (_×_ to _×'_; ⟨_,_⟩ to ⟨_,_⟩'; π₁ to π₁'; π₂ to π₂') + open Terminal terminal using (!; !-unique) + open BinaryProducts products using (π₁; π₂; ⟨_,_⟩; project₁; project₂; unique) + + --* + -- ExceptionMonad TX = X + E + --* + + ExceptionMonad : Set o → Monad (Sets o) + ExceptionMonad E = record + { F = F + ; η = η' + ; μ = μ' + ; assoc = λ {X} → λ where + {inj₁ x} → refl + {inj₂ x} → refl + ; sym-assoc = λ {X} → λ where + {inj₁ x} → refl + {inj₂ x} → refl + ; identityˡ = λ {X} → λ where + {inj₁ x} → refl + {inj₂ x} → refl + ; identityʳ = λ {X} → λ where + {inj₁ x} → refl + {inj₂ x} → refl + } + where + open Cocartesian (SetsCocartesian) using (_+_; _+₁_) + F = record + { F₀ = λ X → X + E + ; F₁ = λ f → f +₁ id + ; identity = λ {A} → λ where + {inj₁ x} → refl + {inj₂ x} → refl + ; homomorphism = λ {X} {Y} {Z} {f} {g} → λ where + {inj₁ x} → refl + {inj₂ x} → refl + ; F-resp-≈ = λ {A} {B} {f} {g} f≈g → λ where + {inj₁ x} → inj₁-resp-≡ (f≈g {x}) + {inj₂ x} → refl + } + η' = ntHelper record + { η = λ X → inj₁ + ; commute = λ {X} {Y} f {x} → refl + } + μ' = ntHelper record + { η = λ X → [ id , inj₂ ] + ; commute = λ {X} {Y} f → λ where + {inj₁ x} → refl + {inj₂ x} → refl + } + + MaybeMonad : Monad (Sets o) + MaybeMonad = ExceptionMonad ⊤ + + --* + -- Reader Monad TX = X^S + --* + + ReaderMonad : Set o → Monad (Sets o) + ReaderMonad S = record + { F = F + ; η = η' + ; μ = μ' + ; assoc = refl + ; sym-assoc = refl + ; identityˡ = refl + ; identityʳ = refl + } + where + open Cocartesian (SetsCocartesian) using (_+_; _+₁_) + open CartesianClosed SetsCCC + F = record + { F₀ = λ X → X ^ S + ; F₁ = λ f g s → f (g s) + ; identity = λ {A} {x} → refl + ; homomorphism = λ {X Y Z f g x} → refl + ; F-resp-≈ = λ {A B f g} fg {x} → ext λ y → fg {x y} + } + η' = ntHelper record + { η = λ X → const + ; commute = λ {X Y} f {x} → refl + } + μ' = ntHelper record + { η = λ X x s → x s s + ; commute = λ {X Y} f {x} → refl + } \ No newline at end of file