minor

agda/src/Algebra/Elgot/Free.lagda.md

@@ -22,7 +22,8 @@ import Categories.Morphism.Reasoning as MR
 ```agda
 module Algebra.Elgot.Free {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
   open import Algebra.Elgot cocartesian
-  open import Category.Construction.ElgotAlgebras cocartesian
+  open import Category.Construction.ElgotAlgebras {C = C}
+  open Cat cocartesian
   open import Categories.Morphism.Properties C
 
   open Category C

agda/src/Algebra/Elgot/Properties.lagda.md

@@ -0,0 +1,57 @@
+```agda
+open import Level
+open import Categories.FreeObjects.Free
+open import Categories.Functor.Core
+open import Categories.Functor.Algebra
+open import Categories.Functor.Coalgebra
+open import Categories.Object.Terminal
+open import Categories.Object.Exponential
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Distributive using (Distributive)
+open import Categories.Category.CartesianClosed using (CartesianClosed)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Construction.EilenbergMoore
+open import Categories.Monad.Relative renaming (Monad to RMonad)
+
+import Categories.Morphism as M
+import Categories.Morphism.Reasoning as MR
+```
+In a CCC free elgot algebras are automatically stable.
+
+
+```agda
+module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (expos : ∀ {A B} → Exponential C A B) where
+  open Category C
+  open HomReasoning
+  open Equiv
+  open Distributive distributive
+  open import Categories.Category.Distributive.Properties distributive
+  open Cartesian cartesian
+  open BinaryProducts products
+  open Cocartesian cocartesian
+  ccc : CartesianClosed C
+  ccc = record { cartesian = cartesian ; exp = expos }
+
+  open CartesianClosed ccc hiding (exp; cartesian)
+
+  open import Category.Construction.ElgotAlgebras {C = C}
+  open Cat cocartesian
+  open Exponentials distributive expos
+  open import Algebra.Elgot.Free cocartesian
+  open import Algebra.Elgot.Stable distributive
+
+  open CartesianClosed Elgot-CCC using () renaming (λg to λg#; _^_ to _^#_)
+
+  stable : ∀ {Y} (fe : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebraˡ fe
+  IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (stable {Y} fe) {X} A f = (eval′ ∘ (Elgot-Algebra-Morphism.h ((fe FreeObject.*) {A = B^A-Helper {A} {X}} (λg f)) ⁂ id))
+  IsStableFreeElgotAlgebraˡ.♯ˡ-law (stable {Y} fe) {X} {A} f = sym (begin 
+    {! [ stable fe , A ]♯ˡ f ∘ (η fe ⁂ id) !} ≈⟨ {!   !} ⟩ 
+    {!   !} ≈⟨ {!   !} ⟩ 
+    {!   !} ≈⟨ {!   !} ⟩ 
+    {!   !} ≈⟨ {!   !} ⟩ 
+    f ∎)
+  IsStableFreeElgotAlgebraˡ.♯ˡ-preserving (stable {Y} fe) {X} {B} f {Z} h = {!   !}
+  IsStableFreeElgotAlgebraˡ.♯ˡ-unique (stable {Y} fe) {X} {B} f g eq₁ eq₂ = {!   !}
+```

agda/src/Algebra/Elgot/Stable.lagda.md

@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import Level
-open import Category.Ambient using (Ambient)
 open import Categories.FreeObjects.Free
 open import Categories.Functor.Core
 open import Categories.Functor.Algebra
@@ -25,7 +24,8 @@ module Algebra.Elgot.Stable {o ℓ e} {C : Category o ℓ e} (distributive : Dis
   open Distributive distributive
   open import Categories.Category.Distributive.Properties distributive
   open import Algebra.Elgot cocartesian
-  open import Category.Construction.ElgotAlgebras cocartesian
+  open import Category.Construction.ElgotAlgebras {C = C}
+  open Cat cocartesian
   open import Categories.Morphism.Properties C
 
   open Category C
@@ -43,6 +43,19 @@ Stable free Elgot algebras have an additional universal iteration preserving mor
 
 ```agda
 
+  record IsStableFreeElgotAlgebraˡ {Y : Obj} (freeElgot : FreeElgotAlgebra Y) : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
+    open FreeObject freeElgot using (η) renaming (FX to FY)
+    open Elgot-Algebra FY using (_#)
+
+    field
+      [_,_]♯ˡ : ∀ {X : Obj} (A : Elgot-Algebra) (f : Y × X ⇒ Elgot-Algebra.A A) → Elgot-Algebra.A FY × X ⇒ Elgot-Algebra.A A
+      ♯ˡ-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ˡ ∘ (η ⁂ id)
+      ♯ˡ-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ˡ ∘ (h # ⁂ id) ≈ Elgot-Algebra._# B (([ B , f ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id))
+      ♯ˡ-unique : ∀ {X : Obj} {B : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A B) (g : Elgot-Algebra.A FY × X ⇒ Elgot-Algebra.A B)
+        → f ≈ g ∘ (η ⁂ id)
+        → ({Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (h # ⁂ id) ≈ Elgot-Algebra._# B ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)))
+        → g ≈ [ B , f ]♯ˡ
+
   record IsStableFreeElgotAlgebra {Y : Obj} (freeElgot : FreeElgotAlgebra Y) : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
     open FreeObject freeElgot using (η) renaming (FX to FY)
     open Elgot-Algebra FY using (_#)

agda/src/Category/Construction/ElgotAlgebras.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Category.Cocartesian using (Cocartesian)
 open import Categories.Category.Cartesian using (Cartesian)
@@ -382,4 +383,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} wher
       (Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) ∎)
     CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = β′
     CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = λ-unique′ eq
-```
+
+    Elgot-CCC : CartesianClosed Elgot-Algebras
+    Elgot-CCC = Equivalence.fromCanonical Elgot-Algebras cccc
+  ```