Work on maybe monad

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
 ```