diff --git a/src/Algebra/Elgot.lagda.md b/src/Algebra/Elgot.lagda.md index c8c086f..cbb130f 100644 --- a/src/Algebra/Elgot.lagda.md +++ b/src/Algebra/Elgot.lagda.md @@ -1,10 +1,9 @@ diff --git a/src/Algebra/Elgot/Free.lagda.md b/src/Algebra/Elgot/Free.lagda.md index cd1e795..586fac2 100644 --- a/src/Algebra/Elgot/Free.lagda.md +++ b/src/Algebra/Elgot/Free.lagda.md @@ -1,8 +1,7 @@ @@ -210,21 +209,21 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e) ## Exponentials of Elgot Algebras TODO ```agda - -- if the carriers of the algebra form a exponential, so do the algebras - B^A-Helper : ∀ {EA : Elgot-Algebra} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra - B^A-Helper {EA} {X} exp = record - { A = A^X - ; algebra = record - { _# = λ {Z} f → λg product (((((eval +₁ idC) ∘ (Categories.Object.Product.repack C product product' +₁ idC)) ∘ dstl) ∘ (f ⁂ idC)) #ᵃ) - ; #-Fixpoint = {! !} - ; #-Uniformity = {! !} - ; #-Folding = {! !} - ; #-resp-≈ = {! !} - } - } - where - open Exponential exp renaming (B^A to A^X; product to product') - open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈) - dstr = λ {X Y Z} → IsIso.inv (isIsoˡ {X} {Y} {Z}) - dstl = λ {X Y Z} → IsIso.inv (isIsoʳ {X} {Y} {Z}) + -- -- if the carriers of the algebra form a exponential, so do the algebras + -- B^A-Helper : ∀ {EA : Elgot-Algebra} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra + -- B^A-Helper {EA} {X} exp = record + -- { A = A^X + -- ; algebra = record + -- { _# = λ {Z} f → λg product (((((eval +₁ idC) ∘ (Categories.Object.Product.repack C product product' +₁ idC)) ∘ dstl) ∘ (f ⁂ idC)) #ᵃ) + -- ; #-Fixpoint = {! !} + -- ; #-Uniformity = {! !} + -- ; #-Folding = {! !} + -- ; #-resp-≈ = {! !} + -- } + -- } + -- where + -- open Exponential exp renaming (B^A to A^X; product to product') + -- open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈) + -- dstr = λ {X Y Z} → IsIso.inv (isIsoˡ {X} {Y} {Z}) + -- dstl = λ {X Y Z} → IsIso.inv (isIsoʳ {X} {Y} {Z}) ``` diff --git a/src/Category/Construction/PreElgotMonads.lagda.md b/src/Category/Construction/PreElgotMonads.lagda.md index 12a2531..18cf2ec 100644 --- a/src/Category/Construction/PreElgotMonads.lagda.md +++ b/src/Category/Construction/PreElgotMonads.lagda.md @@ -1,7 +1,7 @@ diff --git a/src/Monad/Instance/Delay/Commutative.lagda.md b/src/Monad/Instance/Delay/Commutative.lagda.md index f1b3f83..9a92496 100644 --- a/src/Monad/Instance/Delay/Commutative.lagda.md +++ b/src/Monad/Instance/Delay/Commutative.lagda.md @@ -1,13 +1,12 @@ diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md index e150a4b..ee2f6a8 100644 --- a/src/Monad/Instance/K/Commutative.lagda.md +++ b/src/Monad/Instance/K/Commutative.lagda.md @@ -1,8 +1,7 @@ ```agda --- TODO arguments c ℓ here! -module Monad.Instance.K.Instance.Maybe {o ℓ e} where +module Monad.Instance.K.Instance.Maybe {c ℓ} where ``` # The Maybe Monad as instance of K 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 @@ -78,6 +76,8 @@ module _ {c ℓ : Level} where _≋_ : ∀ {A B : Setoid c ℓ} → A ⟶ B → A ⟶ B → Set (c ⊔ ℓ) _≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g + ≋-sym : ∀ {A B : Setoid c ℓ} {f g : A ⟶ B} → f ≋ g → g ≋ f + ≋-sym {A} {B} {f} {g} = IsEquivalence.sym (Setoid.isEquivalence (A ⇨ B)) {f} {g} maybeFun-id : ∀ {A : Setoid c ℓ} → (maybeFun idₛ) ≋ idₛ {A = maybeSetoid A} maybeFun-id {A} {nothing} {nothing} i≈j = i≈j @@ -111,6 +111,21 @@ module _ {c ℓ : Level} where μ-natural {A} {B} f {nothing} {nothing} i≈j = i≈j μ-natural {A} {B} f {just i} {just j} i≈j = cong (maybeFun f) {i} {j} i≈j + μ-assoc : ∀ {A : Setoid c ℓ} → (μ A ∘ maybeFun (μ A)) ≋ (μ A ∘ μ (maybeSetoid A)) + μ-assoc {A} {nothing} {nothing} i≈j = i≈j + μ-assoc {A} {just i} {just j} i≈j = cong (μ A) {i} {j} i≈j + + μ-sym-assoc : ∀ {A : Setoid c ℓ} → (μ A ∘ μ (maybeSetoid A)) ≋ (μ A ∘ maybeFun (μ A)) + μ-sym-assoc {A} {nothing} {nothing} i≈j = i≈j + μ-sym-assoc {A} {just i} {just j} i≈j = cong (μ A) {i} {j} i≈j + + identityˡ : ∀ {A : Setoid c ℓ} → (μ A ∘ maybeFun (η A)) ≋ idₛ + identityˡ {A} {nothing} {nothing} i≈j = i≈j + identityˡ {A} {just _} {just _} i≈j = i≈j + + identityʳ : ∀ {A : Setoid c ℓ} → (μ A ∘ η (maybeSetoid A)) ≋ idₛ + identityʳ {A} {i} {j} i≈j = i≈j + maybeMonad : Monad (Setoids c ℓ) maybeMonad = record { F = record @@ -128,10 +143,10 @@ module _ {c ℓ : Level} where { η = μ ; commute = μ-natural }) - ; assoc = {! !} - ; sym-assoc = {! !} - ; identityˡ = {! !} - ; identityʳ = {! !} + ; assoc = λ {A} {i} {j} → μ-assoc {A} {i} {j} + ; sym-assoc = λ {A} {i} {j} → μ-sym-assoc {A} {i} {j} + ; identityˡ = λ {A} {i} {j} → identityˡ {A} {i} {j} + ; identityʳ = λ {A} {i} {j} → identityʳ {A} {i} {j} } diff --git a/src/Monad/Instance/K/Kleene.lagda.md b/src/Monad/Instance/K/Kleene.lagda.md index 2491b20..684578c 100644 --- a/src/Monad/Instance/K/Kleene.lagda.md +++ b/src/Monad/Instance/K/Kleene.lagda.md @@ -3,7 +3,7 @@ {-# OPTIONS --allow-unsolved-metas #-} open import Level open import Data.Product using (_,_) -open import Category.Instance.AmbientCategory +open import Category.Ambient using (Ambient) open import Categories.Object.Terminal open import Categories.Functor.Algebra open import Categories.Object.Initial diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md index a1c068e..dd9106e 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/src/Monad/Instance/K/PreElgot.lagda.md @@ -1,7 +1,7 @@