From 11107c67b82df8f79d7b163baf503e2eaef78cff Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 30 Nov 2023 17:50:57 +0100 Subject: [PATCH] Work on maybe monad --- src/Monad/Instance/K/Instance/Maybe.lagda.md | 149 +++++++++---------- 1 file changed, 68 insertions(+), 81 deletions(-) diff --git a/src/Monad/Instance/K/Instance/Maybe.lagda.md b/src/Monad/Instance/K/Instance/Maybe.lagda.md index 5ca50cf..5a5326c 100644 --- a/src/Monad/Instance/K/Instance/Maybe.lagda.md +++ b/src/Monad/Instance/K/Instance/Maybe.lagda.md @@ -5,14 +5,14 @@ open import Level open import Category.Instance.AmbientCategory open import Categories.Category -open import Categories.Category.Instance.Setoids renaming (Setoids to Setoids') +open import Categories.Category.Instance.Setoids open import Categories.Monad open import Categories.Category.Monoidal.Instance.Setoids open import Categories.Category.Cocartesian open import Categories.Object.Terminal -open import Function.Equality as SΠ renaming (id to ⟶-id) +open import Function.Equality as SΠ renaming (id to idₛ) import Categories.Morphism.Reasoning as MR -open import Relation.Binary renaming (Setoid to Setoid') +open import Relation.Binary open import Data.Sum using (_⊎_; inj₁; inj₂) open import Data.Sum.Function.Setoid open import Data.Sum.Relation.Binary.Pointwise @@ -20,9 +20,7 @@ open import Agda.Builtin.Unit using (tt) open import Data.Unit.Polymorphic using () renaming (⊤ to ⊤ₚ) open import Data.Empty.Polymorphic using () renaming (⊥ to ⊥ₚ) open import Categories.NaturalTransformation using (ntHelper) -import Relation.Binary.PropositionalEquality as Eq open import Function.Base using (id) -open Eq using (_≡_) renaming (refl to refl-≡; sym to sym-≡; trans to trans-≡) -- refl; cong; sym) ``` --> @@ -35,40 +33,30 @@ open Ambient ambient using () Assuming the axiom of choice, the maybe monad is an instance of K in the category of setoids. ```agda -module _ {c ℓ' : Level} where - -- redefine Setoid and Setoids without universe levels for convenience - private - Setoid = Setoid' c (c ⊔ ℓ') - Setoids = Setoids' c (c ⊔ ℓ') - -- open Cocartesian (Setoids-Cocartesian {c} {c ⊔ ℓ'}) - open Terminal (terminal {c} {c ⊔ ℓ'}) - open MR Setoids - open Category Setoids hiding (_∘_; _⇒_; id) - -- open HomReasoning - open Equiv - -- open Setoid - - data Maybe {a} (A : Set a) : Set a where +module _ {c ℓ : Level} where + data Maybe (A : Set c) : Set c where nothing : Maybe A just : A → Maybe A - maybeSetoid : ∀ {a} (A : Set a) → Setoid' a a - maybeSetoid {a} A = record { Carrier = Maybe A ; _≈_ = eq ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } } + maybe-eq : ∀ (A : Setoid c ℓ) → Maybe (Setoid.Carrier A) → Maybe (Setoid.Carrier A) → Set ℓ + maybe-eq _ nothing nothing = ⊤ₚ + maybe-eq _ nothing (just y) = ⊥ₚ + maybe-eq _ (just x) nothing = ⊥ₚ + maybe-eq A (just x) (just y) = Setoid._≈_ A x y + + maybeSetoid : Setoid c ℓ → Setoid c ℓ + maybeSetoid A = record { Carrier = Maybe A.Carrier ; _≈_ = maybe-eq A ; isEquivalence = record { refl = λ {x} → refl' {x = x} ; sym = λ {x y} → sym' {x} {y} ; trans = λ {x y z} → trans' {x} {y} {z} } } where - eq : Maybe A → Maybe A → Set a - eq nothing nothing = ⊤ₚ - eq nothing (just y) = ⊥ₚ - eq (just x) nothing = ⊥ₚ - eq (just x) (just y) = x ≡ y - refl' : Reflexive eq + module A = Setoid A + refl' : Reflexive (maybe-eq A) refl' {nothing} = lift tt - refl' {just x} = refl-≡ - sym' : Symmetric eq + refl' {just x} = IsEquivalence.refl A.isEquivalence + sym' : Symmetric (maybe-eq A) sym' {nothing} {nothing} = id sym' {nothing} {just y} = id sym' {just x} {nothing} = id - sym' {just x} {just y} = sym-≡ - trans' : Transitive eq + sym' {just x} {just y} = IsEquivalence.sym A.isEquivalence + trans' : Transitive (maybe-eq A) trans' {nothing} {nothing} {nothing} = λ _ → id trans' {nothing} {nothing} {just z} = λ _ → id trans' {nothing} {just y} {nothing} = λ _ _ → lift tt @@ -76,62 +64,61 @@ module _ {c ℓ' : Level} where trans' {just x} {nothing} {nothing} = λ () trans' {just x} {nothing} {just z} = λ () trans' {just x} {just y} {nothing} = λ _ → id - trans' {just x} {just y} {just z} = trans-≡ - - -- maybe-η : - lift-maybe : ∀ {a} (A : Set a) (x : A) → Maybe A - lift-maybe {a} A x = just x + trans' {just x} {just y} {just z} = IsEquivalence.trans A.isEquivalence - -- TODO this is completely wrong... - maybe : Monad Setoids - maybe = record + maybeFun : ∀ {A B : Setoid c ℓ} → A ⟶ B → maybeSetoid A ⟶ maybeSetoid B + maybeFun {A} {B} f = record { _⟨$⟩_ = app ; cong = λ {i} {j} → cong' i j } + where + app : Setoid.Carrier (maybeSetoid A) → Setoid.Carrier (maybeSetoid B) + app nothing = nothing + app (just x) = just (f ⟨$⟩ x) + cong' : ∀ (i j : Maybe (Setoid.Carrier A)) → maybe-eq A i j → maybe-eq B (app i) (app j) + cong' nothing nothing i≈j = i≈j + cong' (just _) (just _) i≈j = cong f i≈j + + _≋_ : ∀ {A B : Setoid c ℓ} → A ⟶ B → A ⟶ B → Set (c ⊔ ℓ) + _≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g + + maybeFun-id : ∀ {A : Setoid c ℓ} → (maybeFun idₛ) ≋ idₛ {A = maybeSetoid A} + maybeFun-id {A} {nothing} {nothing} i≈j = i≈j + maybeFun-id {A} {just _} {just _} i≈j = i≈j + + + η : ∀ (A : Setoid c ℓ) → A ⟶ maybeSetoid A + η A = record { _⟨$⟩_ = just ; cong = id } + + μ : ∀ (A : Setoid c ℓ) → maybeSetoid (maybeSetoid A) ⟶ maybeSetoid A + μ A = record { _⟨$⟩_ = app ; cong = λ {i} {j} → cong' i j } + where + app : Setoid.Carrier (maybeSetoid (maybeSetoid A)) → Setoid.Carrier (maybeSetoid A) + app nothing = nothing + app (just x) = x + cong' : ∀ (i j : Maybe (Maybe (Setoid.Carrier A))) → maybe-eq (maybeSetoid A) i j → maybe-eq A (app i) (app j) + cong' nothing nothing i≈j = i≈j + cong' (just i) (just j) i≈j = i≈j + + maybeMonad : Monad (Setoids c ℓ) + maybeMonad = record { F = record - { F₀ = λ X → X ⊎ₛ ⊤ - ; F₁ = λ {A} {B} f → f ⊎-⟶ ⟶-id - ; identity = λ {A} → id+id {A} - ; homomorphism = λ {A} {B} {C} {f} {g} → homomorphism' {f = f} {g = g} - ; F-resp-≈ = λ {A} {B} {f} {g} f≈g → F-resp-≈' f g f≈g + { F₀ = maybeSetoid + ; F₁ = maybeFun + ; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y} + ; homomorphism = {! !} + ; F-resp-≈ = {! !} } ; η = ntHelper (record - { η = λ X → inj₁ₛ - ; commute = η-commute + { η = η + ; commute = {! !} }) ; μ = ntHelper (record - { η = λ X → mult - ; commute = λ {X} {Y} f → μ-commute f + { η = μ + ; commute = {! !} }) - ; assoc = assoc' - ; sym-assoc = sym-assoc' - ; identityˡ = identityˡ' - ; identityʳ = λ {X} → identityʳ' {X} + ; assoc = {! !} + ; sym-assoc = {! !} + ; identityˡ = {! !} + ; identityʳ = {! !} } - where - id+id : ∀ {A B : Setoid} → ⟶-id {A = A} ⊎-⟶ ⟶-id {A = B} ≈ ⟶-id - id+id (inj₁ x) = inj₁ x - id+id (inj₂ x) = inj₂ x - F-resp-≈' : ∀ {A B : Setoid} (f g : A ⟶ B) → f ≈ g → f ⊎-⟶ ⟶-id {A = ⊤} ≈ g ⊎-⟶ ⟶-id - F-resp-≈' {A} {B} f g f≈g (inj₁ x) = inj₁ (f≈g x) - F-resp-≈' {A} {B} f g f≈g (inj₂ x) = inj₂ x - homomorphism' : ∀ {A B C : Setoid } {f : A ⟶ B} {g : B ⟶ C} → (g ∘ f) ⊎-⟶ ⟶-id {A = ⊤} ≈ g ⊎-⟶ ⟶-id ∘ f ⊎-⟶ ⟶-id - homomorphism' {A} {B} {C} {f} {g} (inj₁ x) = inj₁ (refl {A} {C} {g ∘ f} x) - homomorphism' {A} {B} {C} {f} {g} (inj₂ x) = inj₂ x - η-commute : ∀ {A B : Setoid} (f : A ⟶ B) → f ⊎-⟶ ⟶-id ∘ inj₁ₛ {B = ⊤} ≈ inj₁ₛ ∘ f - η-commute {A} {B} f x = inj₁ (refl {A} {B} {f} x) - mult : ∀ {A B : Setoid} → (A ⊎ₛ B) ⊎ₛ B ⟶ A ⊎ₛ B - mult {A} {B} = record { _⟨$⟩_ = λ { (inj₁ x) → x ; (inj₂ x) → inj₂ x } ; cong = λ { (inj₁ x) → x ; (inj₂ x) → inj₂ x } } - μ-commute : ∀ {A B : Setoid} (f : A ⟶ B) → mult {B} {⊤} ∘ (f ⊎-⟶ ⟶-id) ⊎-⟶ ⟶-id ≈ f ⊎-⟶ ⟶-id {A = ⊤} ∘ mult - μ-commute {A} {B} f (inj₁ x) = refl {A ⊎ₛ ⊤} {B ⊎ₛ ⊤} {f ⊎-⟶ ⟶-id} x - μ-commute {A} {B} f (inj₂ x) = inj₂ x - assoc' : ∀ {A : Setoid} → mult {A = A} {B = ⊤} ∘ (mult ⊎-⟶ ⟶-id) ≈ mult ∘ mult - assoc' {A} (inj₁ x) = refl {(A ⊎ₛ ⊤) ⊎ₛ ⊤} {A ⊎ₛ ⊤} {mult} x - assoc' {A} (inj₂ x) = inj₂ x - sym-assoc' : ∀ {A : Setoid} → mult ∘ mult ≈ mult {A = A} {B = ⊤} ∘ (mult ⊎-⟶ ⟶-id) - sym-assoc' {A} (inj₁ x) = refl {(A ⊎ₛ ⊤) ⊎ₛ ⊤} {A ⊎ₛ ⊤} {mult} x - sym-assoc' {A} (inj₂ x) = inj₂ x - identityˡ' : ∀ {A : Setoid} → mult {A = A} {B = ⊤} ∘ inj₁ₛ ⊎-⟶ ⟶-id ≈ ⟶-id - identityˡ' {A} (inj₁ x) = inj₁ x - identityˡ' {A} (inj₂ x) = inj₂ x - identityʳ' : ∀ {A : Setoid} → mult {A = A} {B = ⊤} ∘ inj₁ₛ ≈ ⟶-id - identityʳ' {A} (inj₁ x) = inj₁ x - identityʳ' {A} (inj₂ x) = inj₂ x + + ``` \ No newline at end of file