sync

agda/src/Algebra/Elgot.lagda.md

@@ -47,8 +47,8 @@ Guarded Elgot algebras are algebras on an endofunctor together with an iteration
 ```
 
 ## Unguarded Elgot algebras
-Unguarded elgot algebras are `Id`-guarded elgot algebras.
-Here we give a different Characterization and show that it is equal.
+Unguarded elgot algebras are `Id`-guarded elgot algebras where the functor algebra is also trivial.
+Here we give a different (easier) Characterization and show that it is equal.
 
 ```agda
   record Elgot-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where
@@ -69,6 +69,7 @@ Here we give a different Characterization and show that it is equal.
 
     open HomReasoning
     open Equiv
+
     -- Compositionality is derivable
     #-Compositionality : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
       → (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂
@@ -195,6 +196,7 @@ Here we give a different Characterization and show that it is equal.
     -- every elgot-algebra comes with a divergence constant
     !ₑ : ⊥ ⇒ A
     !ₑ = i₂ #
+
   record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where
     field
       A : Obj

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

@@ -122,3 +122,9 @@ Stable free Elgot algebras have an additional universal iteration preserving mor
     
     open IsStableFreeElgotAlgebra isStableFreeElgotAlgebra public
 ```
+
+In a cartesian closed category stability is derivable
+
+```agda
+  -- TODO
+```

agda/src/Category/Ambient.lagda.md

@@ -52,6 +52,8 @@ module Category.Ambient where
     open Extensive extensive public
     open Cocartesian cocartesian renaming (+-unique to []-unique) public
     open Cartesian cartesian public
+
+    -- some helpers
     monoidal : Monoidal C
     monoidal = CartesianMonoidal.monoidal cartesian
 

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

@@ -14,7 +14,7 @@ open import Data.Product using (_,_)
 ```
 -->
 
-# The (functor) category of pre-Elgot monads.
+# The (functor) category of strong pre-Elgot monads.
 
 ```agda
 module Category.Construction.StrongPreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where

agda/src/Monad/Instance/Setoids/K.lagda.md

@@ -154,11 +154,11 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
   delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra
   delay-algebras A = record { A = Delayₛ A ; algebra = delay-algebras-on {A}}
 
-  open Elgot-Algebra using () renaming (A to ⟦_⟧)
+  open Elgot-Algebra using (#-Fixpoint; #-Uniformity) renaming (A to ⟦_⟧)
 
 
   delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
-  delay-lift {A} {B} f = record { h = record { to = < helper # > ; cong = helper#≈-cong } ; preserves = {!   !} }
+  delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → ? }
     where
     open Elgot-Algebra B using (_#)
     -- (f + id) ∘ out
@@ -265,6 +265,14 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
         eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)]
         eq₂ = Elgot-Algebra.#-Uniformity B {Delayₛ∼ (A ×ₛ ℕ-setoid {ℓ})} {Delayₛ∼ A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} {!   !} -- eq (∼-refl (A ×ₛ ℕ-setoid))
 
+    delay-lift' = record { to = < helper # > ; cong = helper#≈-cong }
+
+    preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delayₛ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (< helper # > (iter {A} {X} < g > x)) ≡ < ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # > x ] 
+    preserves' {X} {g} {x} = ≡-sym ⟦ B ⟧ (#-Uniformity B {!  λ {x} → by-uni {x} !}) -- #-Uniformity B {!   !}
+      where
+        by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ < [ inj₁ₛ ∘ delay-lift' , inj₂ₛ ∘ iterₛ {A} {X} g ]ₛ ∘ g > x ≡ (helper₁ ∘′ iter {A} {X} < g >) x ]
+        by-uni = {!   !}
+
   <<_>> = Elgot-Algebra-Morphism.h
 
   freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
@@ -276,9 +284,9 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
     ; *-uniq = λ {B} f g eq {x} → *-uniq' {B} f g eq {x}
     }
     where
-      *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x : Delay ∣ A ∣} → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift f >>) ⟨$⟩ x)
-      *-uniq' {B} f g eq {now x} = {!   !} -- ≡-trans ⟦ B ⟧ (eq {x} {y} (now-inj x≡y)) (≡-refl ⟦ B ⟧)
-      *-uniq' {B} f g eq {later x} = {!   !} 
+      *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x : Delay ∣ A ∣} → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift {A} {B} f >>) ⟨$⟩ x)
+      *-uniq' {B} f g eq {now x} = ≡-trans ⟦ B ⟧ (eq {x}) (≡-sym ⟦ B ⟧ (#-Fixpoint B))
+      *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {!   !} (≡-sym ⟦ B ⟧ (#-Fixpoint B))