Work on maybe monad

src/Algebra/Elgot.lagda.md

@@ -139,7 +139,6 @@ Here we give a different Characterization and show that it is equal.
           [ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]                        ≈˘⟨ ∘[] ⟩
           (idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]                                               ∎
 
-    -- TODO Proposition 41
     #-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) → ((idC +₁ [ idC , idC ]) ∘ f)# ≈ ([ i₁ , ((idC +₁ [ idC , idC ]) ∘ f) # +₁ idC ] ∘ f) #
     #-Diamond {X} f = begin 
       g #                                                                                                             ≈⟨ introʳ inject₂ ⟩ 
@@ -153,7 +152,8 @@ Here we give a different Characterization and show that it is equal.
       [ i₁ , [ [ (idC +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (idC +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ idC ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ 
       [ i₁ , [ [ i₁ , i₂ ∘ i₂ ∘ i₁ ] ∘ g , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ] # ∘ i₂ ∘ i₂                                  ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl)) (∘[] ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
       [ i₁ , [ [ i₁ , i₂ ] ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂                            ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ 
-      [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ {A = X} {B = X}                                          ≈⟨ {!   !} ⟩
+      [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂                                                          ≈˘⟨ pullˡ (sym (#-Uniformity by-uni₂)) ⟩
+      [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ i₂ ∘ i₂                                ≈⟨ (refl⟩∘⟨ (pullˡ inject₂ ○ (+₁∘i₂ ○ identityʳ))) ⟩
       [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ {A = A + X} {B = X}                                           ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩ 
       [ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂                                                      ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩ 
       ([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂                                                                         ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩ 
@@ -167,13 +167,24 @@ Here we give a different Characterization and show that it is equal.
       where
         g = (idC +₁ [ idC , idC ]) ∘ f
         h = [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f
+        by-uni₂ : (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ]
+        by-uni₂ = begin 
+          (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ]                                       ≈⟨ ∘[] ⟩ 
+          [ (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ i₁ , (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ]    ≈⟨ []-cong₂ (+₁∘i₁ ○ identityʳ) ∘[] ⟩ 
+          [ i₁ , [ (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ i₂ ∘ f ] ]    ≈⟨ []-cong₂ refl ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂)) ⟩ 
+          [ i₁ , [ (idC ∘ idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ f ] ]              ≈⟨ []-cong₂ refl ([]-cong₂ ((+₁-cong₂ identity² (pullˡ inject₂ ○ +₁∘i₁)) ⟩∘⟨refl) (∘[] ⟩∘⟨refl)) ⟩ 
+          [ i₁ , [ (idC +₁ i₁ ∘ i₂) ∘ g , [ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ idC) ] ∘ f ] ]                                         ≈˘⟨ []-cong₂ refl ([]-cong₂ refl (pullˡ ∘[])) ⟩ 
+          [ i₁ , [ (idC +₁ i₁ ∘ i₂) ∘ g , i₂ ∘ h ] ]                                                                          ≈˘⟨ []-cong₂ inject₁ ([]-cong₂ inject₂ identityʳ) ⟩ 
+          [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] ∘ i₁ , [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] ∘ i₂ , (i₂ ∘ h) ∘ idC ] ]                    ≈˘⟨ []-cong₂ (pullˡ inject₁) []∘+₁ ⟩ 
+          [ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₁ ∘ i₁ , [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ (i₂ +₁ idC) ] ≈˘⟨ ∘[] ⟩ 
+          [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ]                                                ∎
         by-uni₁ : (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈ g ∘ [ idC , idC ]
         by-uni₁ = begin 
-          (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈⟨ ∘[] ⟩ 
+          (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ]                          ≈⟨ ∘[] ⟩ 
           [ (idC +₁ [ idC , idC ]) ∘ (idC +₁ i₁) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² inject₁)) refl ⟩ 
-          [ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩ 
-          [ g , g ] ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩ 
-          g ∘ [ idC , idC ] ∎
+          [ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ]                         ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩ 
+          [ g , g ]                                                                 ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩ 
+          g ∘ [ idC , idC ]                                                         ∎
         by-fix : [ i₁ , (idC +₁ i₂) ∘ g ] # ≈ [ idC , g # ]
         by-fix = sym (begin 
           [ idC , g # ]                                                   ≈⟨ []-cong₂ refl #-Fixpoint ⟩ 

src/Monad/Instance/K/Instance/Maybe.lagda.md

@@ -10,11 +10,17 @@ 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
+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)
+open import Function.Base using (id)
 ```
 -->
 
@@ -27,27 +33,92 @@ 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
-  open Cocartesian (Setoids-Cocartesian {c} {c ⊔ ℓ'})
-  open Terminal (terminal {c} {c ⊔ ℓ'})
-  open MR (Setoids c (c ⊔ ℓ'))
-  open Category (Setoids c (c ⊔ ℓ'))
-  open Equiv
+module _ {c ℓ : Level} where
+  data Maybe (A : Set c) : Set c where
+    nothing : Maybe A
+    just : A → Maybe A
 
-  maybe : Monad (Setoids c (c ⊔ ℓ'))
-  maybe = record
+  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
+      module A = Setoid A
+      refl' : Reflexive (maybe-eq A)
+      refl' {nothing} = lift tt
+      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} = 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
+      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} = IsEquivalence.trans A.isEquivalence
+
+  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 = {!   !}
+      { F₀ = maybeSetoid
+      ; F₁ = maybeFun
+      ; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y}
       ; homomorphism = {!   !}
-      ; F-resp-≈ = λ {A} {B} {f} {g} f≈g → +₁-cong₂ f≈g ?
+      ; F-resp-≈ = {!   !}
       }
-    ; η = {!   !}
-    ; μ = {!   !}
+    ; η = ntHelper (record 
+      { η = η 
+      ; commute = {!   !} 
+      })
+    ; μ = ntHelper (record 
+      { η = μ 
+      ; commute = {!   !} 
+      })
     ; assoc = {!   !}
     ; sym-assoc = {!   !}
     ; identityˡ = {!   !}
     ; identityʳ = {!   !}
     }
+
+
 ```