src/Algebra/Elgot.lagda.md

@@ -139,6 +139,7 @@ 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₂ ⟩ 
@@ -152,8 +153,7 @@ 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₂                                                          ≈˘⟨ 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₂ ∘ f ] ] # ∘ i₂ ∘ i₂ {A = X} {B = X}                                          ≈⟨ {!   !} ⟩
       [ [ 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,24 +167,13 @@ 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,17 +10,11 @@ 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)
+
 ```
 -->
 
@@ -33,92 +27,27 @@ 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
-  data Maybe (A : Set c) : Set c where
-    nothing : Maybe A
-    just : A → Maybe A
+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
   
-  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
+  maybe : Monad (Setoids c (c ⊔ ℓ'))
+  maybe = record
     { F = record
-      { F₀ = maybeSetoid
-      ; F₁ = maybeFun
-      ; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y}
+      { F₀ = λ X → X + ⊤ 
+      ; F₁ = λ {A} {B} f → f +₁ ⟶-id
+      ; identity = {!   !}
       ; homomorphism = {!   !}
-      ; F-resp-≈ = {!   !}
+      ; F-resp-≈ = λ {A} {B} {f} {g} f≈g → +₁-cong₂ f≈g ?
       }
-    ; η = ntHelper (record 
-      { η = η 
-      ; commute = {!   !} 
-      })
-    ; μ = ntHelper (record 
-      { η = μ 
-      ; commute = {!   !} 
-      })
+    ; η = {!   !}
+    ; μ = {!   !}
     ; assoc = {!   !}
     ; sym-assoc = {!   !}
     ; identityˡ = {!   !}
     ; identityʳ = {!   !}
     }
-
-
 ```