minor
This commit is contained in:
parent
d7d6dda798
commit
113ae4259e
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 195 additions and 0 deletions
195
Monads-Sets.agda
Normal file
195
Monads-Sets.agda
Normal file
|
|
@ -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
|
||||
}
|
||||
Loading…
Reference in a new issue