diff --git a/src/Monad/Instance/K/Instance/Maybe.lagda.md b/src/Monad/Instance/K/Instance/Maybe.lagda.md index 8f2a8a9..77bebf3 100644 --- a/src/Monad/Instance/K/Instance/Maybe.lagda.md +++ b/src/Monad/Instance/K/Instance/Maybe.lagda.md @@ -5,16 +5,24 @@ open import Level open import Category.Instance.AmbientCategory open import Categories.Category -open import Categories.Category.Instance.Setoids +open import Categories.Category.Instance.Setoids renaming (Setoids to 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) import Categories.Morphism.Reasoning as MR -open import Relation.Binary +open import Relation.Binary renaming (Setoid to Setoid') +open import Data.Sum using (_⊎_; inj₁; inj₂) +open import Data.Sum.Function.Setoid +open import Data.Sum.Relation.Binary.Pointwise 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) ``` --> @@ -28,26 +36,104 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor ```agda module _ {c ℓ' : Level} where - open Cocartesian (Setoids-Cocartesian {c} {c ⊔ ℓ'}) + -- 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 c (c ⊔ ℓ')) - open Category (Setoids c (c ⊔ ℓ')) + open MR Setoids + open Category Setoids hiding (_∘_; _⇒_; id) + -- open HomReasoning open Equiv + -- open Setoid + + private + variable + a : Level + + data Maybe (A : Set a) : Set a where + nothing : Maybe A + just : A → Maybe A + + maybeSetoid : ∀ (A : Set a) → Setoid' a a + maybeSetoid A = record { Carrier = Maybe A ; _≈_ = eq ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } } + 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 + refl' {nothing} = lift tt + refl' {just x} = refl-≡ + sym' : Symmetric eq + sym' {nothing} {nothing} = id + sym' {nothing} {just y} = id + sym' {just x} {nothing} = id + sym' {just x} {just y} = sym-≡ + trans' : Transitive eq + trans' {nothing} {nothing} {nothing} = λ _ → id + trans' {nothing} {nothing} {just z} = λ _ → id + trans' {nothing} {just y} {nothing} = λ _ _ → lift tt + trans' {nothing} {just y} {just z} = λ () + 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 : Monad (Setoids c (c ⊔ ℓ')) + -- maybe-η : + + -- TODO this is completely wrong... + maybe : Monad Setoids maybe = record { F = record - { F₀ = λ X → X + ⊤ - ; F₁ = λ {A} {B} f → f +₁ ⟶-id - ; identity = {! !} - ; homomorphism = {! !} - ; F-resp-≈ = λ {A} {B} {f} {g} f≈g → +₁-cong₂ f≈g ? + { 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 } - ; η = {! !} - ; μ = {! !} - ; assoc = {! !} - ; sym-assoc = {! !} - ; identityˡ = {! !} - ; identityʳ = {! !} + ; η = ntHelper (record + { η = λ X → inj₁ₛ + ; commute = η-commute + }) + ; μ = ntHelper (record + { η = λ X → mult + ; commute = λ {X} {Y} f → μ-commute f + }) + ; assoc = assoc' + ; sym-assoc = sym-assoc' + ; identityˡ = identityˡ' + ; identityʳ = λ {X} → identityʳ' {X} } + 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