Work on maybe monad

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
+module _ {c ℓ : Level} where
-  -- redefine Setoid and Setoids without universe levels for convenience
+  data Maybe (A : Set c) : Set c where
-  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
     nothing : Maybe A
     just : A → Maybe A
 
-  maybeSetoid : ∀ {a} (A : Set a) → Setoid' a a
+  maybe-eq : ∀ (A : Setoid c ℓ) → Maybe (Setoid.Carrier A) → Maybe (Setoid.Carrier A) → Set ℓ
-  maybeSetoid {a} A = record { Carrier = Maybe A ; _≈_ = eq ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } }
+  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
+      module A = Setoid A
-      eq nothing nothing = ⊤ₚ
+      refl' : Reflexive (maybe-eq A)
-      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-≡
+      refl' {just x} = IsEquivalence.refl A.isEquivalence
-      sym' : Symmetric eq
+      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-≡
+      sym' {just x} {just y} = IsEquivalence.sym A.isEquivalence
-      trans' : Transitive eq
+      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-≡
+      trans' {just x} {just y} {just z} = IsEquivalence.trans A.isEquivalence
 
-  -- maybe-η : 
+  maybeFun : ∀ {A B : Setoid c ℓ} → A ⟶ B → maybeSetoid A ⟶ maybeSetoid B
-  lift-maybe : ∀ {a} (A : Set a) (x : A) → Maybe A
+  maybeFun {A} {B} f = record { _⟨$⟩_ = app ; cong = λ {i} {j} → cong' i j }
-  lift-maybe {a} A x = just x
+    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
 
-  -- TODO this is completely wrong...
+  _≋_ : ∀ {A B : Setoid c ℓ} → A ⟶ B → A ⟶ B → Set (c ⊔ ℓ)
-  maybe : Monad Setoids
+  _≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
-  maybe = record
+
+  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₀ = maybeSetoid
-      ; F₁ = λ {A} {B} f → f ⊎-⟶ ⟶-id
+      ; F₁ = maybeFun
-      ; identity = λ {A} → id+id {A}
+      ; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y}
-      ; homomorphism = λ {A} {B} {C} {f} {g} → homomorphism' {f = f} {g = g}
+      ; homomorphism = {!   !}
-      ; F-resp-≈ = λ {A} {B} {f} {g} f≈g → F-resp-≈' f g f≈g
+      ; F-resp-≈ = {!   !}
       }
     ; η = ntHelper (record 
-      { η = λ X → inj₁ₛ 
+      { η = η 
-      ; commute = η-commute
+      ; commute = {!   !} 
       })
     ; μ = ntHelper (record 
-      { η = λ X → mult
+      { η = μ 
-      ; commute = λ {X} {Y} f → μ-commute f
+      ; commute = {!   !} 
       })
-    ; assoc = assoc'
+    ; assoc = {!   !}
-    ; sym-assoc = sym-assoc'
+    ; sym-assoc = {!   !}
-    ; identityˡ = identityˡ'
+    ; identityˡ = {!   !}
-    ; identityʳ = λ {X} → identityʳ' {X}
+    ; 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
 ```