From 8af4faf80c76efd97145f8158c230020c0a13c0d Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Thu, 17 Aug 2023 18:07:14 +0200
Subject: [PATCH] Added UniformIterationAlgebras

---
 ElgotAlgebra.agda             |  2 ++
 UniformIterationAlgebra.agda  | 29 +++++++++++++++++
 UniformIterationAlgebras.agda | 60 +++++++++++++++++++++++++++++++++++
 3 files changed, 91 insertions(+)
 create mode 100644 UniformIterationAlgebra.agda
 create mode 100644 UniformIterationAlgebras.agda

diff --git a/ElgotAlgebra.agda b/ElgotAlgebra.agda
index 0e85bb5..62a9113 100644
--- a/ElgotAlgebra.agda
+++ b/ElgotAlgebra.agda
@@ -1,5 +1,7 @@
 open import Level
 
+module ElgotAlgebra where
+
 open import Categories.Functor renaming (id to idF)
 open import Categories.Functor.Algebra
 open import Categories.Category
diff --git a/UniformIterationAlgebra.agda b/UniformIterationAlgebra.agda
new file mode 100644
index 0000000..26b6749
--- /dev/null
+++ b/UniformIterationAlgebra.agda
@@ -0,0 +1,29 @@
+open import Level
+open import Categories.Category.Core
+open import Categories.Category.Extensive.Bundle
+open import Categories.Category.Extensive
+open import Categories.Category.Cocartesian
+
+module UniformIterationAlgebra {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where
+  open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
+  open Cocartesian (Extensive.cocartesian extensive)
+
+  record Uniform-Iteration-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where
+    -- iteration operator
+    field
+      _# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A)
+
+    -- _# properties
+    field
+      #-Fixpoint : ∀ {X} {f : X ⇒ A + X }
+        → f # ≈ [ idC , f # ] ∘ f
+      #-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y} 
+        → (idC +₁ h) ∘ f ≈ g ∘ h
+        → f # ≈ g # ∘ h
+      #-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #)
+
+  record Uniform-Iteration-Algebra : Set (o ⊔ ℓ ⊔ e) where
+    field
+      A : Obj
+      algebra : Uniform-Iteration-Algebra-on A
+    open Uniform-Iteration-Algebra-on algebra public
\ No newline at end of file
diff --git a/UniformIterationAlgebras.agda b/UniformIterationAlgebras.agda
new file mode 100644
index 0000000..c8c5489
--- /dev/null
+++ b/UniformIterationAlgebras.agda
@@ -0,0 +1,60 @@
+open import Level
+open import Categories.Category.Core
+open import Categories.Category.Extensive.Bundle
+open import Categories.Category.Extensive
+open import Categories.Category.Cocartesian
+import Categories.Morphism.Reasoning as MR
+
+open import UniformIterationAlgebra
+
+module UniformIterationAlgebras {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where
+  open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
+  open Cocartesian (Extensive.cocartesian extensive)
+  open HomReasoning
+  open MR C
+  open Equiv
+
+  -- iteration preversing morphism between two elgot-algebras
+  module _ (E₁ E₂ : Uniform-Iteration-Algebra D) where
+    open Uniform-Iteration-Algebra E₁ renaming (_# to _#₁)
+    open Uniform-Iteration-Algebra E₂ renaming (_# to _#₂; A to B)
+    record Uniform-Iteration-Algebra-Morphism : Set (o ⊔ ℓ ⊔ e) where
+      field
+        h : A ⇒ B
+        preserves : ∀ {X} {f : X ⇒ A + X} → h ∘ (f #₁) ≈ ((h +₁ idC) ∘ f)#₂
+
+  -- the category of uniform-iteration algebras for a given category
+  Uniform-Iteration-Algebras : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) e
+  Uniform-Iteration-Algebras = record
+    { Obj       = Uniform-Iteration-Algebra D
+    ; _⇒_       = Uniform-Iteration-Algebra-Morphism
+    ; _≈_       = λ f g → Uniform-Iteration-Algebra-Morphism.h f ≈ Uniform-Iteration-Algebra-Morphism.h g
+    ; id        = λ {EB} → let open Uniform-Iteration-Algebra EB in 
+    record { h = idC; preserves = λ {X : Obj} {f : X ⇒ A + X} → begin
+      idC ∘ f #            ≈⟨ identityˡ ⟩ 
+      f #                  ≈⟨ #-resp-≈ (introˡ (coproduct.unique id-comm-sym id-comm-sym)) ⟩
+      ((idC +₁ idC) ∘ f) # ∎ }
+    ; _∘_       = λ {EA} {EB} {EC} f g → let 
+      open Uniform-Iteration-Algebra-Morphism f renaming (h to hᶠ; preserves to preservesᶠ)
+      open Uniform-Iteration-Algebra-Morphism g renaming (h to hᵍ; preserves to preservesᵍ)
+      open Uniform-Iteration-Algebra EA using (A) renaming (_# to _#ᵃ)
+      open Uniform-Iteration-Algebra EB using () renaming (_# to _#ᵇ; A to B)
+      open Uniform-Iteration-Algebra EC using () renaming (_# to _#ᶜ; A to C; #-resp-≈ to #ᶜ-resp-≈)
+      in record { h = hᶠ ∘ hᵍ; preserves = λ {X} {f : X ⇒ A + X} → begin 
+        (hᶠ ∘ hᵍ) ∘ (f #ᵃ)                     ≈⟨ pullʳ preservesᵍ ⟩
+        (hᶠ ∘ (((hᵍ +₁ idC) ∘ f) #ᵇ))          ≈⟨ preservesᶠ ⟩ 
+        (((hᶠ +₁ idC) ∘ (hᵍ +₁ idC) ∘ f) #ᶜ)   ≈⟨ #ᶜ-resp-≈ (pullˡ (trans +₁∘+₁ (+₁-cong₂ refl (identity²)))) ⟩ 
+        ((hᶠ ∘ hᵍ +₁ idC) ∘ f) #ᶜ              ∎ }
+    ; identityˡ = identityˡ
+    ; identityʳ = identityʳ
+    ; identity² = identity²
+    ; assoc     = assoc
+    ; sym-assoc = sym-assoc
+    ; equiv     = record
+      { refl  = refl
+      ; sym   = sym
+      ; trans = trans
+      }
+    ; ∘-resp-≈  = ∘-resp-≈
+    }
+    where open Uniform-Iteration-Algebra-Morphism
\ No newline at end of file