From b325ecc6c3ba7bdd5b1f9bce1b78ede7ca6c0254 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 5 Oct 2023 16:22:05 +0200 Subject: [PATCH] =?UTF-8?q?=F0=9F=9A=A7=20Working=20on=20stable=20algebras?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Algebra/Properties.lagda.md | 99 +++++++++++++++++++++++++++++++++ src/Monad/Instance/K.lagda.md | 30 ++-------- 2 files changed, 104 insertions(+), 25 deletions(-) create mode 100644 src/Algebra/Properties.lagda.md diff --git a/src/Algebra/Properties.lagda.md b/src/Algebra/Properties.lagda.md new file mode 100644 index 0000000..74d19a1 --- /dev/null +++ b/src/Algebra/Properties.lagda.md @@ -0,0 +1,99 @@ + + +```agda +module Algebra.Properties {o ℓ e} (ambient : Ambient o ℓ e) where + open Ambient ambient + open import Algebra.ElgotAlgebra ambient + open import Algebra.UniformIterationAlgebra ambient + open import Category.Construction.ElgotAlgebras ambient + open import Category.Construction.UniformIterationAlgebras ambient + + open Equiv +``` + +# Properties of algebras +This file contains some typedefs and records concerning different algebras. + +## Free Uniform-Iteration Algebras + +```agda + uniformForgetfulF : Functor Uniform-Iteration-Algebras C + uniformForgetfulF = record + { F₀ = λ X → Uniform-Iteration-Algebra.A X + ; F₁ = λ f → Uniform-Iteration-Algebra-Morphism.h f + ; identity = refl + ; homomorphism = refl + ; F-resp-≈ = λ x → x + } + + -- typedef + FreeUniformIterationAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e) + FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras} uniformForgetfulF X +``` + +-- TODO this is an alternate characterization, prove it with lemma 18 and formalize definition 17 +## Stable Free Uniform-Iteration Algebras + +## Free Elgot Algebras + +```agda + elgotForgetfulF : Functor Elgot-Algebras C + elgotForgetfulF = record + { F₀ = λ X → Elgot-Algebra.A X + ; F₁ = λ f → Elgot-Algebra-Morphism.h f + ; identity = refl + ; homomorphism = refl + ; F-resp-≈ = λ x → x + } + + -- typedef + FreeElgotAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e) + FreeElgotAlgebra X = FreeObject {C = C} {D = Elgot-Algebras} elgotForgetfulF X +``` + +## Free Elgot to Free Uniform Iteration + +```agda + elgot-to-uniformF : Functor Elgot-Algebras Uniform-Iteration-Algebras + elgot-to-uniformF = record + { F₀ = λ X → record { A = Elgot-Algebra.A X ; algebra = record + { _# = λ f → (X Elgot-Algebra.#) f + ; #-Fixpoint = Elgot-Algebra.#-Fixpoint X + ; #-Uniformity = Elgot-Algebra.#-Uniformity X + ; #-resp-≈ = Elgot-Algebra.#-resp-≈ X + }} + ; F₁ = λ f → record { h = Elgot-Algebra-Morphism.h f ; preserves = Elgot-Algebra-Morphism.preserves f } + ; identity = refl + ; homomorphism = refl + ; F-resp-≈ = λ x → x + } + +{- +TODO / NOTES: +- Theorem 35 talks about stable free elgot algebras, + but it is supposed to show that Ď and K are equivalent (under assumptions). + This would require us being able to get FreeUniformIterationAlgebras from FreeElgotAlgebras, but the free _* doesn't type check! + It probably is possible to remedy it somehow, one naive way would be to do the proof of Theorem 35 twice, + once for the theorem and a second time to establish the connection between ĎX and KX. +- TODO talk to Sergey about this +-} + FreeElgot⇒FreeUniformIteration : ∀ {X} → FreeElgotAlgebra X → FreeUniformIterationAlgebra X + FreeElgot⇒FreeUniformIteration {X} free-elgot = record + { FX = F₀ elgot + ; η = η' + ; _* = λ {Y} f → F₁ (f *') + ; *-lift = {! !} + ; *-uniq = {! !} + } + where + open FreeObject free-elgot renaming (FX to elgot; η to η'; _* to _*'; *-lift to *-lift'; *-uniq to *-uniq') + open Elgot-Algebra elgot + open Functor elgot-to-uniformF using (F₀; F₁) +``` diff --git a/src/Monad/Instance/K.lagda.md b/src/Monad/Instance/K.lagda.md index fc29a53..5ec55c8 100644 --- a/src/Monad/Instance/K.lagda.md +++ b/src/Monad/Instance/K.lagda.md @@ -1,17 +1,11 @@ @@ -34,24 +28,10 @@ In this file I explore the monad ***K*** and its properties: module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where open Ambient ambient open import Category.Construction.UniformIterationAlgebras ambient - open import Algebra.UniformIterationAlgebra ambient + open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF) + open Equiv - -- TODO move this to a different file - - forgetfulF : Functor Uniform-Iteration-Algebras C - forgetfulF = record - { F₀ = λ X → Uniform-Iteration-Algebra.A X - ; F₁ = λ f → Uniform-Iteration-Algebra-Morphism.h f - ; identity = refl - ; homomorphism = refl - ; F-resp-≈ = id - } - - -- typedef - FreeUniformIterationAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e) - FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras} forgetfulF X - ``` ### *Lemma 16*: definition of monad ***K*** @@ -62,10 +42,10 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where algebras : ∀ X → FreeUniformIterationAlgebra X freeF : Functor C Uniform-Iteration-Algebras - freeF = FO⇒Functor forgetfulF algebras + freeF = FO⇒Functor uniformForgetfulF algebras - adjoint : freeF ⊣ forgetfulF - adjoint = FO⇒LAdj forgetfulF algebras + adjoint : freeF ⊣ uniformForgetfulF + adjoint = FO⇒LAdj uniformForgetfulF algebras K : Monad C K = adjoint⇒monad adjoint