From a877cd3f256b6b8676c1a27f3fa96949fe68d247 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Wed, 15 Nov 2023 09:41:27 +0100 Subject: [PATCH] Proof that KX is freeElgot (still assuming compositionality) --- .../Instance/K/Compositionality.lagda.md | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/Monad/Instance/K/Compositionality.lagda.md b/src/Monad/Instance/K/Compositionality.lagda.md index ee365cc..3789165 100644 --- a/src/Monad/Instance/K/Compositionality.lagda.md +++ b/src/Monad/Instance/K/Compositionality.lagda.md @@ -15,7 +15,12 @@ module Monad.Instance.K.Compositionality {o ℓ e} (ambient : Ambient o ℓ e) ( open MonadK MK open import Algebra.UniformIterationAlgebra ambient + open import Category.Construction.UniformIterationAlgebras ambient + open import Category.Construction.ElgotAlgebras ambient open import Algebra.ElgotAlgebra ambient + open import Algebra.Properties ambient + open import Categories.Functor.Core + open Functor using (F₀; F₁) elgot : ∀ (A : Obj) → Elgot-Algebra-on (K.₀ A) elgot A = record @@ -27,4 +32,19 @@ module Monad.Instance.K.Compositionality {o ℓ e} (ambient : Ambient o ℓ e) ( } where open Uniform-Iteration-Algebra (algebras A) using (_#; #-Fixpoint; #-Uniformity; #-resp-≈) + + freeElgot : ∀ (A : Obj) → FreeElgotAlgebra A + freeElgot A = record + { FX = record { A = K.₀ A ; algebra = elgot A } + ; η = η (freealgebras A) + ; _* = λ {X} f → record + { h = Uniform-Iteration-Algebra-Morphism.h (_* (freealgebras A) {A = F₀ elgot-to-uniformF X} f) + ; preserves = λ {Y} {g} → Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras A) *) f) + } + ; *-lift = *-lift (freealgebras A) + ; *-uniq = λ {X} f g eq → *-uniq (freealgebras A) f (F₁ elgot-to-uniformF g) eq + } + where + open FreeObject using (η; _*; *-lift; *-uniq) ``` +2