re-add IsFreeObject, work on proof that delay is freeelgot

agda/src/FreeObject.lagda.md

@@ -0,0 +1,56 @@
+<!--
+```agda
+open import Level
+open import Categories.Category
+open import Categories.Functor
+```
+-->
+
+```agda
+module FreeObject where
+private
+  variable
+    o ℓ e o' ℓ' e' : Level
+```
+
+# Free objects
+The notion of free object has been formalized in agda-categories:
+
+```agda
+open import Categories.FreeObjects.Free
+``` 
+
+but we need a predicate expressing that an object 'is free':
+
+```agda 
+record IsFreeObject {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) : Set (suc (e ⊔ e' ⊔ o ⊔ ℓ ⊔ o' ⊔ ℓ')) where
+
+  private
+    module C = Category C using (Obj; id; identityʳ; identityˡ; _⇒_; _∘_; equiv; module Equiv)
+    module D = Category D using (Obj; _⇒_; _∘_; equiv)
+    module U = Functor U using (₀; ₁)
+
+  field
+     η : C [ X , U.₀ FX ]
+     _* : ∀ {A : D.Obj} → C [ X , U.₀ A ] → D [ FX , A ]
+     *-lift : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) → C [ (U.₁ (f *) C.∘ η) ≈ f ]
+     *-uniq : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) (g : D [ FX , A ]) → C [ (U.₁ g) C.∘ η ≈ f ] → D [ g ≈ f * ]
+```
+
+and some way to convert between these notions:
+
+```agda
+IsFreeObject⇒FreeObject : ∀ {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) → IsFreeObject U X FX → FreeObject U X
+IsFreeObject⇒FreeObject U X FX isFO = record 
+  { FX = FX 
+  ; η = η 
+  ; _* = _* 
+  ; *-lift = *-lift 
+  ; *-uniq = *-uniq 
+  }
+  where open IsFreeObject isFO
+
+  -- TODO FreeObject⇒IsFreeObject
+
+```
+

agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md

@@ -11,6 +11,7 @@ open import Codata.Musical.Notation
 open import Function using (_∘′_) renaming (_∘_ to _∘f_)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_) renaming (sym to ≡-sym)
+open import FreeObject
 ``` 
 -->
 
@@ -21,6 +22,8 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
   open import Monad.Instance.K.Instance.Delay {ℓ} {ℓ}
   open import Category.Ambient.Setoids
   open import Algebra.Elgot (setoidAmbient {ℓ})
+  open import Algebra.Elgot.Free (setoidAmbient {ℓ})
+  open import Category.Construction.ElgotAlgebras (setoidAmbient {ℓ})
   open import Monad.PreElgot (setoidAmbient {ℓ})
   open Equality
 
@@ -65,6 +68,17 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
   ...                                   | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy
   ...                                   | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx
   ...                                   | inj₂ a | inj₂ b = ≈-sym (later-eq (later≈ (♯ iter-cong f (∼-sym X (inj₂-helper f x∼y eqx eqy)))))
+
+  -- iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {g : Y ⟶ (delaySetoid A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ]
+  -- iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y = ≈-trans (helper x) (iter-cong g (cong h x∼y))
+  --   where
+  --   helper : ∀ (x : Setoid.Carrier X) → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ x) ]
+  --   helper x with f ⟨$⟩ x in eqa | g ⟨$⟩ (h ⟨$⟩ x) in eqb
+  --   ...                                      | inj₁ a     | inj₁ b          = {!   !}
+  --   ...                                      | inj₁ a     | inj₂ b          = {!   !} -- absurd
+  --   ...                                      | inj₂ a     | inj₁ b          = {!   !} -- absurd
+  --   ...                                      | inj₂ a     | inj₂ b rewrite (≡-sym eqb) = {!   !} -- later≈ (♯ {! iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {a} {(h ⟨$⟩ a)}  !}) -- ≈-trans {_} {{!   !}} (later≈ {{!   !}} {{!   !}} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ helper a)) (later≈ (♯ {!   !}))
+
   {-# TERMINATING #-}
   iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {g : Y ⟶ (delaySetoid A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ]
   iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy
@@ -152,8 +166,8 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
       helper : (X ⊎ₛ Y) [ inj₂ a ∼ inj₂ b ]
       helper rewrite (≡-sym eqx) | (≡-sym eqy) = cong h (drop-inj₂ ix∼iy)
 
-  delay-algebras : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (delaySetoid A)
-  delay-algebras {A} = record
+  delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (delaySetoid A)
+  delay-algebras-on {A} = record
     { _# = λ {X} f → record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = λ {x} {y} x∼y → iter-cong {A} {X} f {x} {y} x∼y }
     ; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f}
     ; #-Uniformity = λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h}
@@ -161,13 +175,25 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
     ; #-resp-≈ = λ {X} {f} {g} → iter-resp-≈ {A} {X} f g
     }
 
-  -- kleisli lifting (just for making the code cleaner)
-  -- TODO
-  -- TODO, freealgebras approach is probably easier
+  delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra
+  delay-algebras A = record { A = delaySetoid A ; algebra = delay-algebras-on {A} }
 
+  isFreeAlgebra : ∀ {A : Setoid ℓ ℓ} → IsFreeObject elgotForgetfulF (delaySetoid A) (delay-algebras A)
+  isFreeAlgebra {A} = record 
+    { η = SΠ.id 
+    ; _* = λ {B} f → record { h = f ; preserves = λ {X} {g} {x} {y} x∼y → *-preserves {B} f {X} {g} {x} {y} x∼y } 
+    ; *-lift = λ {B} f {x} {y} x∼y → cong f x∼y 
+    ; *-uniq = λ {B} f g g≋f {x} {y} x∼y → g≋f x∼y 
+    }
+    where
+      -- TODO use fixpoint for this 
+      *-preserves : ∀ {B : Elgot-Algebra} (f : delaySetoid A ⟶ Elgot-Algebra.A B) {X : Setoid ℓ ℓ} {g : X ⟶ (delaySetoid A) ⊎ₛ X} → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → Elgot-Algebra.A B [ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ∼ ((B Elgot-Algebra.#) _) ⟨$⟩ y ]
+      *-preserves {B} f {X} {g} {x} {y} x∼y = {!   !}
+
+  -- TODO remove
   delayPreElgot : IsPreElgot delayMonad
   delayPreElgot = record 
-    { elgotalgebras = delay-algebras
+    { elgotalgebras = delay-algebras-on
     ; extend-preserves = {!   !} 
     }