diff --git a/agda/src/Algebra/Elgot/Free.lagda.md b/agda/src/Algebra/Elgot/Free.lagda.md
index 9bd4d2e..8f14393 100644
--- a/agda/src/Algebra/Elgot/Free.lagda.md
+++ b/agda/src/Algebra/Elgot/Free.lagda.md
@@ -22,8 +22,7 @@ import Categories.Morphism.Reasoning as MR
```agda
module Algebra.Elgot.Free {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
open import Algebra.Elgot cocartesian
- open import Category.Construction.ElgotAlgebras {C = C}
- open Cat cocartesian
+ open import Category.Construction.ElgotAlgebras cocartesian
open import Categories.Morphism.Properties C
open Category C
diff --git a/agda/src/Algebra/Elgot/Properties.lagda.md b/agda/src/Algebra/Elgot/Properties.lagda.md
index b076444..9e82596 100644
--- a/agda/src/Algebra/Elgot/Properties.lagda.md
+++ b/agda/src/Algebra/Elgot/Properties.lagda.md
@@ -1,5 +1,4 @@
```agda
-{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Categories.FreeObjects.Free
open import Categories.Functor.Core
@@ -13,8 +12,6 @@ open import Categories.Category.CartesianClosed using (CartesianClosed)
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.BinaryProducts using (BinaryProducts)
-open import Categories.Category.Construction.EilenbergMoore
-open import Categories.Monad.Relative renaming (Monad to RMonad)
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
@@ -39,9 +36,8 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive :
open CartesianClosed ccc hiding (exp; cartesian)
- open import Category.Construction.ElgotAlgebras {C = C}
- open Cat cocartesian
- open Exponentials distributive expos
+ open import Category.Construction.ElgotAlgebras cocartesian
+ open import Category.Construction.ElgotAlgebras.Exponentials distributive expos
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian
open import Algebra.Elgot.Stable distributive
@@ -49,7 +45,7 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive :
open Elgot-Algebra-Morphism renaming (h to <_>)
free-isStableˡ : ∀ {Y} (fe : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebraˡ fe
- IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (free-isStableˡ {Y} fe) {X} A f = (eval′ ∘ (< FreeObject._* fe {B^A-Helper {A} {X}} (λg f) > ⁂ id))
+ IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (free-isStableˡ {Y} fe) {X} A f = (eval′ ∘ (< FreeObject._* fe {Exponential-Elgot-Algebra {A} {X}} (λg f) > ⁂ id))
where open FreeObject fe
IsStableFreeElgotAlgebraˡ.♯ˡ-law (free-isStableˡ {Y} fe) {X} {A} f = sym (begin
(eval′ ∘ (< (λg f)* > ⁂ id)) ∘ (η ⁂ id) ≈⟨ pullʳ ⁂∘⁂ ⟩
@@ -83,4 +79,7 @@ module Algebra.Elgot.Properties {o ℓ e} {C : Category o ℓ e} (distributive :
open FreeObject fe renaming (FX to KY)
open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-resp-≈ to #ᵇ-resp-≈)
open Elgot-Algebra KY using () renaming (_# to _#ʸ)
+
+ free-isStable : ∀ {Y} (fe : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebra fe
+ free-isStable {Y} fe = isStableˡ⇒isStable fe (free-isStableˡ fe)
```
\ No newline at end of file
diff --git a/agda/src/Algebra/Elgot/Stable.lagda.md b/agda/src/Algebra/Elgot/Stable.lagda.md
index f7652db..c0cc2e7 100644
--- a/agda/src/Algebra/Elgot/Stable.lagda.md
+++ b/agda/src/Algebra/Elgot/Stable.lagda.md
@@ -24,8 +24,7 @@ module Algebra.Elgot.Stable {o ℓ e} {C : Category o ℓ e} (distributive : Dis
open Distributive distributive
open import Categories.Category.Distributive.Properties distributive
open import Algebra.Elgot cocartesian
- open import Category.Construction.ElgotAlgebras {C = C}
- open Cat cocartesian
+ open import Category.Construction.ElgotAlgebras cocartesian
open import Categories.Morphism.Properties C
open Category C
diff --git a/agda/src/Category/Construction/ElgotAlgebras.lagda.md b/agda/src/Category/Construction/ElgotAlgebras.lagda.md
index cf4689a..2cd70b0 100644
--- a/agda/src/Category/Construction/ElgotAlgebras.lagda.md
+++ b/agda/src/Category/Construction/ElgotAlgebras.lagda.md
@@ -1,429 +1,67 @@
<!--
```agda
-{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Categories.Category.Cocartesian using (Cocartesian)
-open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.CartesianClosed using (CartesianClosed)
-open import Categories.Category.CartesianClosed.Canonical renaming (CartesianClosed to CanonicalCartesianClosed)
-open import Categories.Category.BinaryProducts using (BinaryProducts)
-open import Categories.Functor using (Functor) renaming (id to idF)
-open import Categories.Object.Terminal using (Terminal)
-open import Categories.Object.Product using (Product)
-open import Categories.Object.Coproduct using (Coproduct)
-open import Categories.Object.Exponential using (Exponential)
open import Categories.Category
-open import Categories.Category.Distributive
-open import Categories.Object.Exponential
-open import Categories.Category.Extensive.Bundle
-open import Categories.Category.Extensive
open import Category.Ambient using (Ambient)
-import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
-import Categories.Morphism.Properties as MP
```
-->
-# The Category of Elgot Algebras (and Constructions)
+# The Category of Elgot Algebras
```agda
-module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} where
+module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
open Category C
- open M C
open MR C
- open MP C
open HomReasoning
open Equiv
+ open Cocartesian cocartesian
+ open import Algebra.Elgot cocartesian
+
+ -- iteration preversing morphism between two elgot-algebras
+ module _ (E₁ E₂ : Elgot-Algebra) where
+ open Elgot-Algebra E₁ renaming (_# to _#₁)
+ open Elgot-Algebra E₂ renaming (_# to _#₂; A to B)
+ record Elgot-Algebra-Morphism : Set (o ⊔ ℓ ⊔ e) where
+ field
+ h : A ⇒ B
+ preserves : ∀ {X} {f : X ⇒ A + X} → h ∘ (f #₁) ≈ ((h +₁ id) ∘ f)#₂
+
+ -- the category of elgot algebras for a given category
+ Elgot-Algebras : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) e
+ Elgot-Algebras = record
+ { Obj = Elgot-Algebra
+ ; _⇒_ = Elgot-Algebra-Morphism
+ ; _≈_ = λ f g → Elgot-Algebra-Morphism.h f ≈ Elgot-Algebra-Morphism.h g
+ ; id = λ {EB} → let open Elgot-Algebra EB in
+ record { h = id; preserves = λ {X : Obj} {f : X ⇒ A + X} → begin
+ id ∘ f # ≈⟨ identityˡ ⟩
+ f # ≈⟨ #-resp-≈ (introˡ (coproduct.unique id-comm-sym id-comm-sym)) ⟩
+ ((id +₁ id) ∘ f) # ∎ }
+ ; _∘_ = λ {EA} {EB} {EC} f g → let
+ open Elgot-Algebra-Morphism f renaming (h to hᶠ; preserves to preservesᶠ)
+ open Elgot-Algebra-Morphism g renaming (h to hᵍ; preserves to preservesᵍ)
+ open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ)
+ open Elgot-Algebra EB using () renaming (_# to _#ᵇ; A to B)
+ open Elgot-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ᵍ +₁ id) ∘ f) #ᵇ)) ≈⟨ preservesᶠ ⟩
+ (((hᶠ +₁ id) ∘ (hᵍ +₁ id) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (pullˡ (trans +₁∘+₁ (+₁-cong₂ refl (identity²)))) ⟩
+ ((hᶠ ∘ hᵍ +₁ id) ∘ 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 Elgot-Algebra-Morphism
```
-
-## The Category of Elgot Algebras
-
-```agda
- module Cat (cocartesian : Cocartesian C) where
- open Cocartesian cocartesian
- open import Algebra.Elgot cocartesian
-
- -- iteration preversing morphism between two elgot-algebras
- module _ (E₁ E₂ : Elgot-Algebra) where
- open Elgot-Algebra E₁ renaming (_# to _#₁)
- open Elgot-Algebra E₂ renaming (_# to _#₂; A to B)
- record Elgot-Algebra-Morphism : Set (o ⊔ ℓ ⊔ e) where
- field
- h : A ⇒ B
- preserves : ∀ {X} {f : X ⇒ A + X} → h ∘ (f #₁) ≈ ((h +₁ id) ∘ f)#₂
-
- -- the category of elgot algebras for a given category
- Elgot-Algebras : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) e
- Elgot-Algebras = record
- { Obj = Elgot-Algebra
- ; _⇒_ = Elgot-Algebra-Morphism
- ; _≈_ = λ f g → Elgot-Algebra-Morphism.h f ≈ Elgot-Algebra-Morphism.h g
- ; id = λ {EB} → let open Elgot-Algebra EB in
- record { h = id; preserves = λ {X : Obj} {f : X ⇒ A + X} → begin
- id ∘ f # ≈⟨ identityˡ ⟩
- f # ≈⟨ #-resp-≈ (introˡ (coproduct.unique id-comm-sym id-comm-sym)) ⟩
- ((id +₁ id) ∘ f) # ∎ }
- ; _∘_ = λ {EA} {EB} {EC} f g → let
- open Elgot-Algebra-Morphism f renaming (h to hᶠ; preserves to preservesᶠ)
- open Elgot-Algebra-Morphism g renaming (h to hᵍ; preserves to preservesᵍ)
- open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ)
- open Elgot-Algebra EB using () renaming (_# to _#ᵇ; A to B)
- open Elgot-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ᵍ +₁ id) ∘ f) #ᵇ)) ≈⟨ preservesᶠ ⟩
- (((hᶠ +₁ id) ∘ (hᵍ +₁ id) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (pullˡ (trans +₁∘+₁ (+₁-cong₂ refl (identity²)))) ⟩
- ((hᶠ ∘ hᵍ +₁ id) ∘ 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 Elgot-Algebra-Morphism
-```
-
-## Finite Products of Elgot Algebras
-
-```agda
- module FiniteProducts (cocartesian : Cocartesian C) (cartesian : Cartesian C) where
- open Cartesian cartesian
- open Cocartesian cocartesian
- open import Algebra.Elgot cocartesian
- open Cat cocartesian
- open BinaryProducts products renaming (unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′)
- -- if the carrier contains a terminal, so does elgot-algebras
- Terminal-Elgot-Algebras : Terminal Elgot-Algebras
- Terminal-Elgot-Algebras = record
- { ⊤ = record
- { A = ⊤
- ; algebra = record
- { _# = λ x → !
- ; #-Fixpoint = λ {_ f} → !-unique ([ id , ! ] ∘ f)
- ; #-Uniformity = λ {_ _ _ _ h} _ → !-unique (! ∘ h)
- ; #-Folding = refl
- ; #-resp-≈ = λ _ → refl
- }
- }
- ; ⊤-is-terminal = record
- { ! = λ {A} → record { h = ! ; preserves = λ {X} {f} → sym (!-unique (! ∘ (A Elgot-Algebra.#) f)) }
- ; !-unique = λ {A} f → !-unique (Elgot-Algebra-Morphism.h f)
- }
- }
- where
- open Terminal terminal
-
- -- if the carriers of the algebra form a product, so do the algebras
- A×B-Helper : ∀ {EA EB : Elgot-Algebra} → Elgot-Algebra
- A×B-Helper {EA} {EB} = record
- { A = A × B
- ; algebra = record
- { _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ id) ∘ h)#ᵃ , ((π₂ +₁ id) ∘ h)#ᵇ ⟩
- ; #-Fixpoint = λ {X} {f} → begin
- ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩
- ⟨ [ id , ((π₁ +₁ id) ∘ f)#ᵃ ] ∘ ((π₁ +₁ id) ∘ f) , [ id , ((π₂ +₁ id) ∘ f)#ᵇ ] ∘ ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁) ⟩
- ⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] ∘ f , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ∘ f ⟩ ≈˘⟨ ⟨⟩∘ ⟩
- (⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ⟩ ∘ f) ≈⟨ ∘-resp-≈ˡ (⟨⟩-unique′
- (begin
- π₁ ∘ ⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ⟩ ≈⟨ project₁ ⟩
- [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₁)) ⟩
- [ π₁ ∘ id , π₁ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ≈˘⟨ ∘[] ⟩
- π₁ ∘ [ id , ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ∎)
- (begin
- π₂ ∘ ⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ⟩ ≈⟨ project₂ ⟩
- [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₂)) ⟩
- [ π₂ ∘ id , π₂ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ≈˘⟨ ∘[] ⟩
- π₂ ∘ [ id , ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ∎)
- )⟩
- ([ id , ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ∘ f) ∎
- ; #-Uniformity = λ {X Y f g h} uni → ⟨⟩-unique′
- (begin
- π₁ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩
- (((π₁ +₁ id) ∘ f)#ᵃ) ≈⟨ #ᵃ-Uniformity
- (begin
- -- TODO factor these out or adjust +₁ swap... maybe call it +₁-id-comm
- (id +₁ h) ∘ (π₁ +₁ id) ∘ f ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm)) ⟩
- (π₁ ∘ id +₁ id ∘ h) ∘ f ≈˘⟨ pullˡ +₁∘+₁ ⟩
- (π₁ +₁ id) ∘ (id +₁ h) ∘ f ≈⟨ pushʳ uni ⟩
- ((π₁ +₁ id) ∘ g) ∘ h ∎)⟩
- (((π₁ +₁ id) ∘ g)#ᵃ ∘ h) ≈˘⟨ pullˡ project₁ ⟩
- π₁ ∘ ⟨ ((π₁ +₁ id) ∘ g)#ᵃ , ((π₂ +₁ id) ∘ g)#ᵇ ⟩ ∘ h ∎)
- (begin
- π₂ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩
- ((π₂ +₁ id) ∘ f)#ᵇ ≈⟨ #ᵇ-Uniformity
- (begin
- (id +₁ h) ∘ (π₂ +₁ id) ∘ f ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))⟩
- ((π₂ ∘ id +₁ id ∘ h) ∘ f) ≈˘⟨ pullˡ +₁∘+₁ ⟩
- (π₂ +₁ id) ∘ ((id +₁ h)) ∘ f ≈⟨ pushʳ uni ⟩
- ((π₂ +₁ id) ∘ g) ∘ h ∎)⟩
- ((π₂ +₁ id) ∘ g)#ᵇ ∘ h ≈˘⟨ pullˡ project₂ ⟩
- π₂ ∘ ⟨ ((π₁ +₁ id) ∘ g)#ᵃ , ((π₂ +₁ id) ∘ g)#ᵇ ⟩ ∘ h ∎)
- ; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y})
- ; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg))
- }
- }
- where
- open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
- open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity; #-Folding to #ᵇ-Folding; #-resp-≈ to #ᵇ-resp-≈)
- +₁-id-swap : ∀ {X Y C} {f : X ⇒ (A × B) + X} {h : Y ⇒ X + Y} (π : A × B ⇒ C) → [ (id +₁ i₁) ∘ ((π +₁ id) ∘ f) , i₂ ∘ h ] ≈ (π +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ]
- +₁-id-swap {X} {Y} {C} {f} {h} π = begin ([ (id +₁ i₁) ∘ ((π +₁ id) ∘ f) , i₂ ∘ h ] ) ≈⟨ ([]-congʳ sym-assoc) ⟩
- ([ ((id +₁ i₁) ∘ (π +₁ id)) ∘ f , i₂ ∘ h ] ) ≈⟨ []-cong₂ (∘-resp-≈ˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))) (∘-resp-≈ˡ (sym identityʳ)) ⟩
- (([ (π ∘ id +₁ id ∘ i₁) ∘ f , (i₂ ∘ id) ∘ h ])) ≈˘⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂) ⟩
- (([ (π +₁ id) ∘ (id +₁ i₁) ∘ f , (π +₁ id) ∘ i₂ ∘ h ])) ≈˘⟨ ∘[] ⟩
- ((π +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ]) ∎
- foldingˡ : ∀ {X} {Y} {f} {h} → (((π₁ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ) ≈ ((π₁ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ
- foldingˡ {X} {Y} {f} {h} = begin
- ((π₁ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₁ identityˡ)) ⟩
- ((((π₁ +₁ id) ∘ f)#ᵃ +₁ h)#ᵃ) ≈⟨ #ᵃ-Folding ⟩
- ([ (id +₁ i₁) ∘ ((π₁ +₁ id) ∘ f) , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ (+₁-id-swap π₁)⟩
- ((π₁ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ ∎
- foldingʳ : ∀ {X} {Y} {f} {h} → ((π₂ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈ ((π₂ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ
- foldingʳ {X} {Y} {f} {h} = begin
- ((π₂ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₂ identityˡ)) ⟩
- ((((π₂ +₁ id) ∘ f)#ᵇ +₁ h)#ᵇ) ≈⟨ #ᵇ-Folding ⟩
- [ (id +₁ i₁) ∘ ((π₂ +₁ id) ∘ f) , i₂ ∘ h ] #ᵇ ≈⟨ #ᵇ-resp-≈ (+₁-id-swap π₂) ⟩
- ((π₂ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ ∎
-
- Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra) → Product Elgot-Algebras EA EB
- Product-Elgot-Algebras EA EB = record
- { A×B = A×B-Helper {EA} {EB}
- ; π₁ = record { h = π₁ ; preserves = λ {X} {f} → project₁ }
- ; π₂ = record { h = π₂ ; preserves = λ {X} {f} → project₂ }
- ; ⟨_,_⟩ = λ {E} f g → let
- open Elgot-Algebra-Morphism f renaming (h to f′; preserves to preservesᶠ)
- open Elgot-Algebra-Morphism g renaming (h to g′; preserves to preservesᵍ)
- open Elgot-Algebra E renaming (_# to _#ᵉ) in record { h = ⟨ f′ , g′ ⟩ ; preserves = λ {X} {h} →
- begin
- ⟨ f′ , g′ ⟩ ∘ (h #ᵉ) ≈⟨ ⟨⟩∘ ⟩
- ⟨ f′ ∘ (h #ᵉ) , g′ ∘ (h #ᵉ) ⟩ ≈⟨ ⟨⟩-cong₂ preservesᶠ preservesᵍ ⟩
- ⟨ ((f′ +₁ id) ∘ h) #ᵃ , ((g′ +₁ id) ∘ h) #ᵇ ⟩ ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₁ identity²))) (#ᵇ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₂ identity²))) ⟩
- ⟨ ((π₁ ∘ ⟨ f′ , g′ ⟩ +₁ id ∘ id) ∘ h) #ᵃ , ((π₂ ∘ ⟨ f′ , g′ ⟩ +₁ id ∘ id) ∘ h) #ᵇ ⟩ ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (pullˡ +₁∘+₁)) (#ᵇ-resp-≈ (pullˡ +₁∘+₁)) ⟩
- ⟨ ((π₁ +₁ id) ∘ (⟨ f′ , g′ ⟩ +₁ id) ∘ h) #ᵃ , ((π₂ +₁ id) ∘ (⟨ f′ , g′ ⟩ +₁ id) ∘ h) #ᵇ ⟩ ∎ }
- ; project₁ = project₁
- ; project₂ = project₂
- ; unique = ⟨⟩-unique
- }
- where
- open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
- open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity; #-Folding to #ᵇ-Folding; #-resp-≈ to #ᵇ-resp-≈)
- open Elgot-Algebra (A×B-Helper {EA} {EB}) using () renaming (_# to _#ᵖ)
-
-
- -- if the carrier is cartesian, so is the category of algebras
- Cartesian-Elgot-Algebras : Cartesian Elgot-Algebras
- Cartesian-Elgot-Algebras = record
- { terminal = Terminal-Elgot-Algebras
- ; products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB }
- }
-```
-
-## Exponentials of Elgot Algebras TODO
-
-```agda
-
- module Exponentials (distributive : Distributive C) (exp : ∀ {A B : Obj} → Exponential C A B) where
- open Distributive distributive
- open import Categories.Category.Distributive.Properties distributive
- ccc : CartesianClosed C
- ccc = record { cartesian = cartesian ; exp = exp }
- open CartesianClosed ccc hiding (cartesian; exp)
- open Cocartesian cocartesian
- open Cartesian cartesian
- open BinaryProducts products renaming (unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′)
- open import Algebra.Elgot cocartesian
- open Cat cocartesian
- open FiniteProducts cocartesian cartesian
-
- B^A-Helper : ∀ {EA : Elgot-Algebra} {X : Obj} → Elgot-Algebra
- B^A-Helper {EA} {X} = record
- { A = A ^ X
- ; algebra = record
- { _# = λ {Z} f → λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)
- ; #-Fixpoint = λ {X} {f} → begin
- λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ≈⟨ λ-cong #ᵃ-Fixpoint ⟩
- λg ([ id , ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ] ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) ≈⟨ λ-cong ((pullˡ []∘+₁) ○ ([]-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩
- λg ([ eval′ , ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) ≈˘⟨ λ-unique′ (begin
- eval′ ∘ (([ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ∘ f) ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩
- eval′ ∘ ([ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ⁂ id) ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ (⟨⟩-unique (begin
- π₁ ∘ [ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id ] ∘ distributeʳ⁻¹ ≈⟨ pullˡ (∘[] ○ []-cong₂ id-comm π₁∘⁂) ⟩
- [ id ∘ π₁ , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ∘ π₁ ] ∘ distributeʳ⁻¹ ≈˘⟨ pullˡ []∘+₁ ⟩
- [ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ≈⟨ refl⟩∘⟨ distributeʳ⁻¹-π₁ ⟩
- [ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ∘ π₁ ∎)
- (begin
- π₂ ∘ [ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id ] ∘ distributeʳ⁻¹ ≈⟨ pullˡ (∘[] ○ []-cong₂ identityʳ (π₂∘⁂ ○ identityˡ)) ⟩
- [ π₂ , π₂ ] ∘ distributeʳ⁻¹ ≈⟨ distributeʳ⁻¹-π₂ ○ (sym identityˡ) ⟩
- id ∘ π₂ ∎)
- ⟩∘⟨refl) ⟩
- eval′ ∘ ([ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id ] ∘ distributeʳ⁻¹) ∘ (f ⁂ id) ≈⟨ pullˡ (pullˡ ∘[]) ⟩
- ([ eval′ ∘ id , eval′ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id) ] ∘ distributeʳ⁻¹) ∘ (f ⁂ id) ≈⟨ assoc ○ ([]-cong₂ identityʳ β′) ⟩∘⟨refl ⟩
- [ eval′ , ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ∎) ⟩
- [ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ∘ f ∎
- ; #-Uniformity = #-Uniformity
- ; #-Folding = #-Folding
- ; #-resp-≈ = λ {Z} {f} {g} f≈g → λ-cong (#ᵃ-resp-≈ (refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ f≈g refl))
- }
- }
- where
- open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
- #-Uniformity : ∀ {D E} {f : D ⇒ A ^ X + D} {g : E ⇒ A ^ X + E} {h : D ⇒ E} → (id +₁ h) ∘ f ≈ g ∘ h → λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ≈ λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ) ∘ h
- #-Uniformity {D} {E} {f} {g} {h} eq = sym (λ-unique′ (begin
- eval′ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ) ∘ h) ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identityˡ) ⟩
- eval′ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ)) ⁂ id) ∘ (h ⁂ id) ≈⟨ pullˡ β′ ⟩
- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ ∘ (h ⁂ id) ≈˘⟨ #ᵃ-Uniformity by-uni ⟩
- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ∎))
- where
- by-uni : (id +₁ (h ⁂ id)) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ∘ (h ⁂ id)
- by-uni = begin
- (id +₁ (h ⁂ id)) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
- (eval′ +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ) ⟩
- (eval′ +₁ id) ∘ (id +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ pullˡ ((+₁-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl) ⟩∘⟨refl ○ distributeʳ⁻¹-natural id id h) ⟩
- (eval′ +₁ id) ∘ (distributeʳ⁻¹ ∘ ((id +₁ h) ⁂ id)) ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ eq identity²) ⟩
- (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ∘ h ⁂ id) ≈˘⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩
- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ∘ (h ⁂ id) ∎
- #-Folding : ∀ {D E} {f : D ⇒ A ^ X + D} {h : E ⇒ D + E} → λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) +₁ h) ⁂ id)) #ᵃ) ≈ λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) #ᵃ)
- #-Folding {D} {E} {f} {h} = λ-cong (begin
- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) +₁ h) ⁂ id)) #ᵃ ≈⟨ #ᵃ-resp-≈ (refl⟩∘⟨ sym (distributeʳ⁻¹-natural id (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) h)) ⟩
- ((eval′ +₁ id) ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ⁂ id) +₁ (h ⁂ id)) ∘ distributeʳ⁻¹) #ᵃ ≈⟨ #ᵃ-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ identityˡ)) ⟩
- ((((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ h ⁂ id) ∘ distributeʳ⁻¹) #ᵃ ≈⟨ #ᵃ-Uniformity by-uni₁ ⟩
- (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵃ ∘ distributeʳ⁻¹ ≈⟨ #ᵃ-Folding ⟩∘⟨refl ⟩
- [ ((id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) , (i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ] #ᵃ ∘ distributeʳ⁻¹ ≈˘⟨ #ᵃ-Uniformity by-uni₂ ⟩
- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) #ᵃ ∎)
- where
- by-uni₁ : (id +₁ distributeʳ⁻¹) ∘ (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ h ⁂ id) ∘ distributeʳ⁻¹ ≈ ((((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ distributeʳ⁻¹ ∘ (h ⁂ id))) ∘ distributeʳ⁻¹
- by-uni₁ = begin
- (id +₁ distributeʳ⁻¹) ∘ (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ h ⁂ id) ∘ distributeʳ⁻¹ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ⟩
- ((((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ distributeʳ⁻¹ ∘ (h ⁂ id))) ∘ distributeʳ⁻¹ ∎
- by-uni₂ : (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id) ≈ [ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹
- by-uni₂ = Iso⇒Epi (IsIso.iso isIsoʳ) ((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ([ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹) (begin
- ((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ distributeʳ ≈⟨ ∘[] ⟩
- [ (((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ (i₁ ⁂ id)) , (((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ (i₂ ⁂ id)) ] ≈⟨ []-cong₂ (pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ inject₁ identity²)))) (pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ inject₂ identity²)))) ⟩
- [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((id +₁ i₁) ∘ f) ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((i₂ ∘ h) ⁂ id) ] ≈⟨ []-cong₂ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩
- [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((id +₁ i₁)) ⁂ id) ∘ (f ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (i₂ ⁂ id) ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (distributeʳ⁻¹-natural id id i₁))) (refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeʳ⁻¹-i₂) ⟩
- [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ ((id ⁂ id +₁ i₁ ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ i₂ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘+₁) ⟩
- [ (id ∘ eval′ +₁ distributeʳ⁻¹ ∘ id) ∘ ((id ⁂ id +₁ i₁ ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (id ∘ eval′ +₁ distributeʳ⁻¹ ∘ id) ∘ i₂ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (pullˡ (pullˡ +₁∘+₁)) (pullˡ +₁∘i₂) ⟩
- [ ((((id ∘ eval′) ∘ (id ⁂ id)) +₁ ((distributeʳ⁻¹ ∘ id) ∘ (i₁ ⁂ id))) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (i₂ ∘ (distributeʳ⁻¹ ∘ id)) ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (((+₁-cong₂ (identityˡ ⟩∘⟨refl) (identityʳ ⟩∘⟨refl ○ distributeʳ⁻¹-i₁)) ⟩∘⟨refl) ⟩∘⟨refl) (pullʳ (pullʳ identityˡ)) ⟩
- [ (((eval′ ∘ (id ⁂ id)) +₁ i₁) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (assoc ○ (+₁-cong₂ (elimʳ (⟨⟩-unique id-comm id-comm)) refl) ⟩∘⟨refl) refl ⟩
- [ (eval′ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈˘⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) refl ⟩
- [ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩
- ([ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹) ∘ distributeʳ ∎)
-
- open Elgot-Algebra-Morphism renaming (h to <_>)
-
- -- cccc : CanonicalCartesianClosed Elgot-Algebras
- -- CanonicalCartesianClosed.⊤ cccc = Terminal.⊤ Terminal-Elgot-Algebras
- -- CanonicalCartesianClosed._×_ cccc X Y = A×B-Helper {X} {Y}
- -- CanonicalCartesianClosed.! cccc = Terminal.! Terminal-Elgot-Algebras
- -- CanonicalCartesianClosed.π₁ cccc {X} {Y} = Product.π₁ (Product-Elgot-Algebras X Y)
- -- CanonicalCartesianClosed.π₂ cccc {X} {Y} = Product.π₂ (Product-Elgot-Algebras X Y)
- -- CanonicalCartesianClosed.⟨_,_⟩ cccc {X} {Y} {Z} f g = Product.⟨_,_⟩ (Product-Elgot-Algebras Y Z) f g
- -- CanonicalCartesianClosed.!-unique cccc = Terminal.!-unique Terminal-Elgot-Algebras
- -- CanonicalCartesianClosed.π₁-comp cccc {X} {Y} {f} {Z} {g} = Product.project₁ (Product-Elgot-Algebras Y Z) {h = f} {i = g}
- -- CanonicalCartesianClosed.π₂-comp cccc {X} {Y} {f} {Z} {g} = Product.project₂ (Product-Elgot-Algebras Y Z) {h = f} {i = g}
- -- CanonicalCartesianClosed.⟨,⟩-unique cccc {C} {A} {B} {f} {g} {h} eq₁ eq₂ = Product.unique (Product-Elgot-Algebras A B) {h = h} {i = f} {j = g} eq₁ eq₂
- -- CanonicalCartesianClosed._^_ cccc A X = B^A-Helper {A} {Elgot-Algebra.A X}
- -- (Elgot-Algebra-Morphism.h) (CanonicalCartesianClosed.eval cccc {A} {B}) = eval′
- -- (Elgot-Algebra-Morphism.preserves) (CanonicalCartesianClosed.eval cccc {A} {B}) {X} {f} = begin
- -- eval′ ∘ ⟨ (λg ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) , _ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
- -- eval′ ∘ ((λg ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) ⁂ id) ∘ ⟨ id , _ ⟩ ≈⟨ pullˡ β′ ⟩
- -- ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id))) ∘ ⟨ id , _ ⟩ ≈˘⟨ Elgot-Algebra.#-Uniformity A by-uni ⟩
- -- (Elgot-Algebra._# A) ((eval′ +₁ id) ∘ f) ∎ -- ⟨ ((π₁ +₁ id) ∘ h)#ᵃ , ((π₂ +₁ id) ∘ h)#ᵇ ⟩
- -- where
- -- by-uni : (id +₁ ⟨ id , _ ⟩) ∘ ((eval′ +₁ id) ∘ f) ≈ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)) ∘ ⟨ id , _ ⟩
- -- by-uni = begin
- -- (id +₁ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩) ∘ ((eval′ +₁ id) ∘ f) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
- -- (eval′ +₁ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩) ∘ f ≈˘⟨ sym-assoc ○ sym-assoc ○ (sym (+-unique by-inj₁ by-inj₂)) ⟩∘⟨refl ⟩
- -- (eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩ ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ refl assoc) ⟩
- -- (eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ ⟨ id ∘ f , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ∘ f ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (⟨⟩-cong₂ refl (Elgot-Algebra.#-Fixpoint B))) ⟩
- -- (eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ ⟨ id ∘ f , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈˘⟨ pullʳ (pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ id-comm identityˡ)) ⟩
- -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈˘⟨ (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id π₁ id)))) ⟩∘⟨refl ⟩
- -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ⁂ id) ∘ (f ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩∘⟨refl ⟩
- -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎
- -- where
- -- by-inj₁ : (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₁ ≈ i₁ ∘ eval′
- -- by-inj₁ = begin
- -- (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₁ ≈⟨ pullʳ ⟨⟩∘ ⟩
- -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id ∘ i₁ , ([ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id)) ∘ i₁ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ id-comm-sym (pullʳ inject₁ ○ pullˡ inject₁ ○ identityˡ)) ⟩
- -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ i₁ ∘ id , π₂ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ) ⟩
- -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ (i₁ ⁂ id) ∘ ⟨ id , π₂ ⟩ ≈⟨ pullʳ (pullʳ (pullˡ distributeʳ⁻¹-i₁)) ⟩
- -- (eval′ +₁ id) ∘ (π₁ ⁂ id +₁ id ⁂ id) ∘ i₁ ∘ ⟨ id , π₂ ⟩ ≈⟨ refl⟩∘⟨ (pullˡ +₁∘i₁) ⟩
- -- (eval′ +₁ id) ∘ (i₁ ∘ (π₁ ⁂ id)) ∘ ⟨ id , π₂ ⟩ ≈⟨ pullˡ (pullˡ +₁∘i₁) ⟩
- -- ((i₁ ∘ eval′) ∘ (π₁ ⁂ id)) ∘ ⟨ id , π₂ ⟩ ≈⟨ cancelʳ (⁂∘⟨⟩ ○ (⟨⟩-cong₂ identityʳ identityˡ) ○ ⟨⟩-unique identityʳ identityʳ) ⟩
- -- i₁ ∘ eval′ ∎
- -- by-inj₂ : (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₂ ≈ i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩
- -- by-inj₂ = begin
- -- (((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ (π₂ +₁ id) ⟩) ∘ i₂ ≈⟨ pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ id-comm-sym (pullʳ inject₂)) ⟩
- -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ i₂ ∘ id , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ] ∘ i₂ ∘ id ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ identityʳ ○ inject₂)) ⟩
- -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ ⟨ i₂ ∘ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ) ⟩
- -- ((eval′ +₁ id) ∘ ((π₁ ⁂ id +₁ id ⁂ id) ∘ distributeʳ⁻¹)) ∘ (i₂ ⁂ id) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ pullʳ (pullʳ (pullˡ distributeʳ⁻¹-i₂)) ⟩
- -- (eval′ +₁ id) ∘ (π₁ ⁂ id +₁ id ⁂ id) ∘ i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ refl⟩∘⟨ (pullˡ inject₂) ⟩
- -- (eval′ +₁ id) ∘ (i₂ ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ pullˡ (pullˡ inject₂) ⟩
- -- ((i₂ ∘ id) ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (cancelʳ (identityˡ ○ ⟨⟩-unique id-comm id-comm)) ⟩∘⟨refl ⟩
- -- i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎
- -- < CanonicalCartesianClosed.curry cccc {A} {B} {C} f > = λg < f >
- -- preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = begin
- -- λg < f > ∘ g #ᵃ ≈⟨ subst ⟩
- -- λg (< f > ∘ (g #ᵃ ⁂ id)) ≈⟨ {! !} ⟩
- -- {! !} ≈⟨ {! !} ⟩
- -- {! !} ≈⟨ {! !} ⟩
- -- λg (< f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩) ≈⟨ λ-cong (preserves f) ⟩
- -- λg (((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ) ≈⟨ {! !} ⟩
- -- {! !} ≈⟨ {! !} ⟩
- -- {! !} ≈⟨ {! !} ⟩
- -- λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ) ∎
- -- where
- -- open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity)
- -- open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
- -- open Elgot-Algebra C using () renaming (_# to _#ᶜ; #-resp-≈ to #ᶜ-resp-≈)
- -- -- uniqueness : ∀
- -- -- Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = λ-unique′ (begin
- -- -- eval′ ∘ ((λg < f > ∘ g #ᵃ) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩
- -- -- eval′ ∘ ((λg (< f > ∘ (g #ᵃ ⁂ id))) ⁂ id) ≈⟨ β′ ⟩
- -- -- < f > ∘ (g #ᵃ ⁂ id) ≈⟨ refl⟩∘⟨ (⟨⟩-unique by-π₁ by-π₂) ⟩
- -- -- < f > ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩
- -- -- ((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᶜ ≈˘⟨ #ᶜ-resp-≈ (refl⟩∘⟨ assoc ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩
- -- -- ((eval′ +₁ id) ∘ (((λg < f > ⁂ id) +₁ (id ⁂ id)) ∘ distributeʳ⁻¹) ∘ (g ⁂ id)) #ᶜ ≈˘⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg < f >) id)))) ⟩
- -- -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg < f > +₁ id) ⁂ id) ∘ (g ⁂ id)) #ᶜ ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩
- -- -- ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) #ᶜ ∎)
- -- -- where
- -- -- open Elgot-Algebra A using () renaming (_# to _#ᵃ; #-Uniformity to #ᵃ-Uniformity)
- -- -- open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
- -- -- open Elgot-Algebra C using () renaming (_# to _#ᶜ; #-resp-≈ to #ᶜ-resp-≈)
- -- -- by-π₁ : π₁ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ g #ᵃ ∘ π₁
- -- -- by-π₁ = project₁ ○ #ᵃ-Uniformity by-uni
- -- -- where
- -- -- by-uni : (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈ g ∘ π₁
- -- -- by-uni = begin
- -- -- (id +₁ π₁) ∘ (π₁ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
- -- -- (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ id) ≈⟨ pullˡ distributeʳ⁻¹-π₁ ⟩
- -- -- π₁ ∘ (g ⁂ id) ≈⟨ project₁ ⟩
- -- -- g ∘ π₁ ∎
- -- -- by-π₂ : π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈ id ∘ π₂
- -- -- by-π₂ = begin
- -- -- π₂ ∘ ⟨ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵃ , ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ⟩ ≈⟨ project₂ ⟩
- -- -- ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)))#ᵇ ≈⟨ #ᵇ-Uniformity by-uni ⟩
- -- -- {! !} #ᵇ ∘ π₂ ≈⟨ {! !} ⟩
- -- -- {! !} ≈⟨ {! !} ⟩
- -- -- {! !} ≈⟨ {! !} ⟩
- -- -- {! !} ≈⟨ {! !} ⟩
- -- -- id ∘ π₂ ∎
- -- -- where
- -- -- by-uni : (id +₁ π₂) ∘ (π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id)) ≈ {! !} ∘ π₂
- -- -- by-uni = begin
- -- -- {! !} ≈⟨ {! !} ⟩
- -- -- {! !} ≈⟨ {! !} ⟩
- -- -- {! !} ≈⟨ {! !} ⟩
- -- -- {! !} ≈⟨ {! !} ⟩
- -- -- {! !} ∎
- -- CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = β′
- -- CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = λ-unique′ eq
-
- -- Elgot-CCC : CartesianClosed Elgot-Algebras
- -- Elgot-CCC = Equivalence.fromCanonical Elgot-Algebras cccc
- ```
diff --git a/agda/src/Category/Construction/ElgotAlgebras/Exponentials.lagda.md b/agda/src/Category/Construction/ElgotAlgebras/Exponentials.lagda.md
new file mode 100644
index 0000000..a7a82b9
--- /dev/null
+++ b/agda/src/Category/Construction/ElgotAlgebras/Exponentials.lagda.md
@@ -0,0 +1,115 @@
+<!--
+```agda
+open import Level
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.CartesianClosed using (CartesianClosed)
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Object.Terminal using (Terminal)
+open import Categories.Object.Product using (Product)
+open import Categories.Object.Coproduct using (Coproduct)
+open import Categories.Object.Exponential using (Exponential)
+open import Categories.Category
+open import Categories.Category.Distributive
+open import Categories.Object.Exponential
+open import Category.Ambient using (Ambient)
+
+import Categories.Morphism as M
+import Categories.Morphism.Reasoning as MR
+import Categories.Morphism.Properties as MP
+```
+-->
+
+```agda
+module Category.Construction.ElgotAlgebras.Exponentials {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (exp : ∀ {A B} → Exponential C A B) where
+ open Category C
+ open HomReasoning
+ open M C
+ open MR C
+ open MP C
+ open Equiv
+ open Distributive distributive
+ open import Categories.Category.Distributive.Properties distributive
+ ccc : CartesianClosed C
+ ccc = record { cartesian = cartesian ; exp = exp }
+ open CartesianClosed ccc hiding (cartesian; exp)
+ open Cocartesian cocartesian
+ open Cartesian cartesian
+ open BinaryProducts products renaming (unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′)
+ open import Algebra.Elgot cocartesian
+ open import Category.Construction.ElgotAlgebras cocartesian
+ open import Category.Construction.ElgotAlgebras.Products cocartesian cartesian
+
+ Exponential-Elgot-Algebra : ∀ {EA : Elgot-Algebra} {X : Obj} → Elgot-Algebra
+ Exponential-Elgot-Algebra {EA} {X} = record
+ { A = A ^ X
+ ; algebra = record
+ { _# = λ {Z} f → λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)
+ ; #-Fixpoint = λ {X} {f} → begin
+ λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ≈⟨ λ-cong #ᵃ-Fixpoint ⟩
+ λg ([ id , ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ] ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) ≈⟨ λ-cong ((pullˡ []∘+₁) ○ ([]-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩
+ λg ([ eval′ , ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) ≈˘⟨ λ-unique′ (begin
+ eval′ ∘ (([ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ∘ f) ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩
+ eval′ ∘ ([ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ⁂ id) ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ (⟨⟩-unique (begin
+ π₁ ∘ [ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id ] ∘ distributeʳ⁻¹ ≈⟨ pullˡ (∘[] ○ []-cong₂ id-comm π₁∘⁂) ⟩
+ [ id ∘ π₁ , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ∘ π₁ ] ∘ distributeʳ⁻¹ ≈˘⟨ pullˡ []∘+₁ ⟩
+ [ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ≈⟨ refl⟩∘⟨ distributeʳ⁻¹-π₁ ⟩
+ [ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ∘ π₁ ∎)
+ (begin
+ π₂ ∘ [ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id ] ∘ distributeʳ⁻¹ ≈⟨ pullˡ (∘[] ○ []-cong₂ identityʳ (π₂∘⁂ ○ identityˡ)) ⟩
+ [ π₂ , π₂ ] ∘ distributeʳ⁻¹ ≈⟨ distributeʳ⁻¹-π₂ ○ (sym identityˡ) ⟩
+ id ∘ π₂ ∎)
+ ⟩∘⟨refl) ⟩
+ eval′ ∘ ([ id , (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id ] ∘ distributeʳ⁻¹) ∘ (f ⁂ id) ≈⟨ pullˡ (pullˡ ∘[]) ⟩
+ ([ eval′ ∘ id , eval′ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) ⁂ id) ] ∘ distributeʳ⁻¹) ∘ (f ⁂ id) ≈⟨ assoc ○ ([]-cong₂ identityʳ β′) ⟩∘⟨refl ⟩
+ [ eval′ , ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ∎) ⟩
+ [ id , λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ] ∘ f ∎
+ ; #-Uniformity = #-Uniformity
+ ; #-Folding = #-Folding
+ ; #-resp-≈ = λ {Z} {f} {g} f≈g → λ-cong (#ᵃ-resp-≈ (refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ f≈g refl))
+ }
+ }
+ where
+ open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
+ #-Uniformity : ∀ {D E} {f : D ⇒ A ^ X + D} {g : E ⇒ A ^ X + E} {h : D ⇒ E} → (id +₁ h) ∘ f ≈ g ∘ h → λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ≈ λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ) ∘ h
+ #-Uniformity {D} {E} {f} {g} {h} eq = sym (λ-unique′ (begin
+ eval′ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ) ∘ h) ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identityˡ) ⟩
+ eval′ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ)) ⁂ id) ∘ (h ⁂ id) ≈⟨ pullˡ β′ ⟩
+ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) #ᵃ ∘ (h ⁂ id) ≈˘⟨ #ᵃ-Uniformity by-uni ⟩
+ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ ∎))
+ where
+ by-uni : (id +₁ (h ⁂ id)) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ∘ (h ⁂ id)
+ by-uni = begin
+ (id +₁ (h ⁂ id)) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩
+ (eval′ +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ) ⟩
+ (eval′ +₁ id) ∘ (id +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ pullˡ ((+₁-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl) ⟩∘⟨refl ○ distributeʳ⁻¹-natural id id h) ⟩
+ (eval′ +₁ id) ∘ (distributeʳ⁻¹ ∘ ((id +₁ h) ⁂ id)) ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ eq identity²) ⟩
+ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ∘ h ⁂ id) ≈˘⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩
+ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ∘ (h ⁂ id) ∎
+ #-Folding : ∀ {D E} {f : D ⇒ A ^ X + D} {h : E ⇒ D + E} → λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) +₁ h) ⁂ id)) #ᵃ) ≈ λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) #ᵃ)
+ #-Folding {D} {E} {f} {h} = λ-cong (begin
+ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) +₁ h) ⁂ id)) #ᵃ ≈⟨ #ᵃ-resp-≈ (refl⟩∘⟨ sym (distributeʳ⁻¹-natural id (λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ)) h)) ⟩
+ ((eval′ +₁ id) ∘ ((λg (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ) ⁂ id) +₁ (h ⁂ id)) ∘ distributeʳ⁻¹) #ᵃ ≈⟨ #ᵃ-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ identityˡ)) ⟩
+ ((((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ h ⁂ id) ∘ distributeʳ⁻¹) #ᵃ ≈⟨ #ᵃ-Uniformity by-uni₁ ⟩
+ (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵃ ∘ distributeʳ⁻¹ ≈⟨ #ᵃ-Folding ⟩∘⟨refl ⟩
+ [ ((id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) , (i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ] #ᵃ ∘ distributeʳ⁻¹ ≈˘⟨ #ᵃ-Uniformity by-uni₂ ⟩
+ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) #ᵃ ∎)
+ where
+ by-uni₁ : (id +₁ distributeʳ⁻¹) ∘ (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ h ⁂ id) ∘ distributeʳ⁻¹ ≈ ((((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ distributeʳ⁻¹ ∘ (h ⁂ id))) ∘ distributeʳ⁻¹
+ by-uni₁ = begin
+ (id +₁ distributeʳ⁻¹) ∘ (((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ h ⁂ id) ∘ distributeʳ⁻¹ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ⟩
+ ((((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) #ᵃ +₁ distributeʳ⁻¹ ∘ (h ⁂ id))) ∘ distributeʳ⁻¹ ∎
+ by-uni₂ : (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id) ≈ [ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹
+ by-uni₂ = Iso⇒Epi (IsIso.iso isIsoʳ) ((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ([ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹) (begin
+ ((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ distributeʳ ≈⟨ ∘[] ⟩
+ [ (((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ (i₁ ⁂ id)) , (((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ (i₂ ⁂ id)) ] ≈⟨ []-cong₂ (pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ inject₁ identity²)))) (pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ inject₂ identity²)))) ⟩
+ [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((id +₁ i₁) ∘ f) ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((i₂ ∘ h) ⁂ id) ] ≈⟨ []-cong₂ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩
+ [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((id +₁ i₁)) ⁂ id) ∘ (f ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (i₂ ⁂ id) ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (distributeʳ⁻¹-natural id id i₁))) (refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeʳ⁻¹-i₂) ⟩
+ [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ ((id ⁂ id +₁ i₁ ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ i₂ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘+₁) ⟩
+ [ (id ∘ eval′ +₁ distributeʳ⁻¹ ∘ id) ∘ ((id ⁂ id +₁ i₁ ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (id ∘ eval′ +₁ distributeʳ⁻¹ ∘ id) ∘ i₂ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (pullˡ (pullˡ +₁∘+₁)) (pullˡ +₁∘i₂) ⟩
+ [ ((((id ∘ eval′) ∘ (id ⁂ id)) +₁ ((distributeʳ⁻¹ ∘ id) ∘ (i₁ ⁂ id))) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (i₂ ∘ (distributeʳ⁻¹ ∘ id)) ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (((+₁-cong₂ (identityˡ ⟩∘⟨refl) (identityʳ ⟩∘⟨refl ○ distributeʳ⁻¹-i₁)) ⟩∘⟨refl) ⟩∘⟨refl) (pullʳ (pullʳ identityˡ)) ⟩
+ [ (((eval′ ∘ (id ⁂ id)) +₁ i₁) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (assoc ○ (+₁-cong₂ (elimʳ (⟨⟩-unique id-comm id-comm)) refl) ⟩∘⟨refl) refl ⟩
+ [ (eval′ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈˘⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) refl ⟩
+ [ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩
+ ([ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹) ∘ distributeʳ ∎)
+ ```
\ No newline at end of file
diff --git a/agda/src/Category/Construction/ElgotAlgebras/Products.lagda.md b/agda/src/Category/Construction/ElgotAlgebras/Products.lagda.md
new file mode 100644
index 0000000..3ef5908
--- /dev/null
+++ b/agda/src/Category/Construction/ElgotAlgebras/Products.lagda.md
@@ -0,0 +1,154 @@
+<!--
+```agda
+open import Level
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.CartesianClosed using (CartesianClosed)
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Object.Terminal using (Terminal)
+open import Categories.Object.Product using (Product)
+open import Categories.Category.Core
+open import Category.Ambient using (Ambient)
+
+import Categories.Morphism.Reasoning as MR
+```
+-->
+
+# The category of elgot algebras on C is cartesian if C is cartesian
+
+```agda
+module Category.Construction.ElgotAlgebras.Products {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) (cartesian : Cartesian C) where
+ open Category C
+ open Equiv
+ open HomReasoning
+ open MR C
+ open import Category.Construction.ElgotAlgebras cocartesian
+ open Cartesian cartesian
+ open Cocartesian cocartesian
+ open import Algebra.Elgot cocartesian
+ open BinaryProducts products renaming (unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′)
+
+ -- if the carrier contains a terminal, so does elgot-algebras
+ Terminal-Elgot-Algebras : Terminal Elgot-Algebras
+ Terminal-Elgot-Algebras = record
+ { ⊤ = record
+ { A = ⊤
+ ; algebra = record
+ { _# = λ x → !
+ ; #-Fixpoint = λ {_ f} → !-unique ([ id , ! ] ∘ f)
+ ; #-Uniformity = λ {_ _ _ _ h} _ → !-unique (! ∘ h)
+ ; #-Folding = refl
+ ; #-resp-≈ = λ _ → refl
+ }
+ }
+ ; ⊤-is-terminal = record
+ { ! = λ {A} → record { h = ! ; preserves = λ {X} {f} → sym (!-unique (! ∘ (A Elgot-Algebra.#) f)) }
+ ; !-unique = λ {A} f → !-unique (Elgot-Algebra-Morphism.h f)
+ }
+ }
+ where
+ open Terminal terminal
+
+ -- the product of the carrier of two elgot algebras is again an elgot algebra
+ Product-Elgot-Algebra : ∀ {EA EB : Elgot-Algebra} → Elgot-Algebra
+ Product-Elgot-Algebra {EA} {EB} = record
+ { A = A × B
+ ; algebra = record
+ { _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ id) ∘ h)#ᵃ , ((π₂ +₁ id) ∘ h)#ᵇ ⟩
+ ; #-Fixpoint = λ {X} {f} → begin
+ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩
+ ⟨ [ id , ((π₁ +₁ id) ∘ f)#ᵃ ] ∘ ((π₁ +₁ id) ∘ f) , [ id , ((π₂ +₁ id) ∘ f)#ᵇ ] ∘ ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁) ⟩
+ ⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] ∘ f , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ∘ f ⟩ ≈˘⟨ ⟨⟩∘ ⟩
+ (⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ⟩ ∘ f) ≈⟨ ∘-resp-≈ˡ (⟨⟩-unique′
+ (begin
+ π₁ ∘ ⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ⟩ ≈⟨ project₁ ⟩
+ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₁)) ⟩
+ [ π₁ ∘ id , π₁ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ≈˘⟨ ∘[] ⟩
+ π₁ ∘ [ id , ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ∎)
+ (begin
+ π₂ ∘ ⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ⟩ ≈⟨ project₂ ⟩
+ [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₂)) ⟩
+ [ π₂ ∘ id , π₂ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ≈˘⟨ ∘[] ⟩
+ π₂ ∘ [ id , ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ∎)
+ )⟩
+ ([ id , ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ∘ f) ∎
+ ; #-Uniformity = λ {X Y f g h} uni → ⟨⟩-unique′
+ (begin
+ π₁ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩
+ (((π₁ +₁ id) ∘ f)#ᵃ) ≈⟨ #ᵃ-Uniformity
+ (begin
+ -- TODO factor these out or adjust +₁ swap... maybe call it +₁-id-comm
+ (id +₁ h) ∘ (π₁ +₁ id) ∘ f ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm)) ⟩
+ (π₁ ∘ id +₁ id ∘ h) ∘ f ≈˘⟨ pullˡ +₁∘+₁ ⟩
+ (π₁ +₁ id) ∘ (id +₁ h) ∘ f ≈⟨ pushʳ uni ⟩
+ ((π₁ +₁ id) ∘ g) ∘ h ∎)⟩
+ (((π₁ +₁ id) ∘ g)#ᵃ ∘ h) ≈˘⟨ pullˡ project₁ ⟩
+ π₁ ∘ ⟨ ((π₁ +₁ id) ∘ g)#ᵃ , ((π₂ +₁ id) ∘ g)#ᵇ ⟩ ∘ h ∎)
+ (begin
+ π₂ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩
+ ((π₂ +₁ id) ∘ f)#ᵇ ≈⟨ #ᵇ-Uniformity
+ (begin
+ (id +₁ h) ∘ (π₂ +₁ id) ∘ f ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))⟩
+ ((π₂ ∘ id +₁ id ∘ h) ∘ f) ≈˘⟨ pullˡ +₁∘+₁ ⟩
+ (π₂ +₁ id) ∘ ((id +₁ h)) ∘ f ≈⟨ pushʳ uni ⟩
+ ((π₂ +₁ id) ∘ g) ∘ h ∎)⟩
+ ((π₂ +₁ id) ∘ g)#ᵇ ∘ h ≈˘⟨ pullˡ project₂ ⟩
+ π₂ ∘ ⟨ ((π₁ +₁ id) ∘ g)#ᵃ , ((π₂ +₁ id) ∘ g)#ᵇ ⟩ ∘ h ∎)
+ ; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y})
+ ; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg))
+ }
+ }
+ where
+ open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
+ open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity; #-Folding to #ᵇ-Folding; #-resp-≈ to #ᵇ-resp-≈)
+ +₁-id-swap : ∀ {X Y C} {f : X ⇒ (A × B) + X} {h : Y ⇒ X + Y} (π : A × B ⇒ C) → [ (id +₁ i₁) ∘ ((π +₁ id) ∘ f) , i₂ ∘ h ] ≈ (π +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ]
+ +₁-id-swap {X} {Y} {C} {f} {h} π = begin ([ (id +₁ i₁) ∘ ((π +₁ id) ∘ f) , i₂ ∘ h ] ) ≈⟨ ([]-congʳ sym-assoc) ⟩
+ ([ ((id +₁ i₁) ∘ (π +₁ id)) ∘ f , i₂ ∘ h ] ) ≈⟨ []-cong₂ (∘-resp-≈ˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))) (∘-resp-≈ˡ (sym identityʳ)) ⟩
+ (([ (π ∘ id +₁ id ∘ i₁) ∘ f , (i₂ ∘ id) ∘ h ])) ≈˘⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂) ⟩
+ (([ (π +₁ id) ∘ (id +₁ i₁) ∘ f , (π +₁ id) ∘ i₂ ∘ h ])) ≈˘⟨ ∘[] ⟩
+ ((π +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ]) ∎
+ foldingˡ : ∀ {X} {Y} {f} {h} → (((π₁ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ) ≈ ((π₁ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ
+ foldingˡ {X} {Y} {f} {h} = begin
+ ((π₁ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₁ identityˡ)) ⟩
+ ((((π₁ +₁ id) ∘ f)#ᵃ +₁ h)#ᵃ) ≈⟨ #ᵃ-Folding ⟩
+ ([ (id +₁ i₁) ∘ ((π₁ +₁ id) ∘ f) , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ (+₁-id-swap π₁)⟩
+ ((π₁ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ ∎
+ foldingʳ : ∀ {X} {Y} {f} {h} → ((π₂ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈ ((π₂ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ
+ foldingʳ {X} {Y} {f} {h} = begin
+ ((π₂ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₂ identityˡ)) ⟩
+ ((((π₂ +₁ id) ∘ f)#ᵇ +₁ h)#ᵇ) ≈⟨ #ᵇ-Folding ⟩
+ [ (id +₁ i₁) ∘ ((π₂ +₁ id) ∘ f) , i₂ ∘ h ] #ᵇ ≈⟨ #ᵇ-resp-≈ (+₁-id-swap π₂) ⟩
+ ((π₂ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ ∎
+
+ Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra) → Product Elgot-Algebras EA EB
+ Product-Elgot-Algebras EA EB = record
+ { A×B = Product-Elgot-Algebra {EA} {EB}
+ ; π₁ = record { h = π₁ ; preserves = λ {X} {f} → project₁ }
+ ; π₂ = record { h = π₂ ; preserves = λ {X} {f} → project₂ }
+ ; ⟨_,_⟩ = λ {E} f g → let
+ open Elgot-Algebra-Morphism f renaming (h to f′; preserves to preservesᶠ)
+ open Elgot-Algebra-Morphism g renaming (h to g′; preserves to preservesᵍ)
+ open Elgot-Algebra E renaming (_# to _#ᵉ) in record { h = ⟨ f′ , g′ ⟩ ; preserves = λ {X} {h} →
+ begin
+ ⟨ f′ , g′ ⟩ ∘ (h #ᵉ) ≈⟨ ⟨⟩∘ ⟩
+ ⟨ f′ ∘ (h #ᵉ) , g′ ∘ (h #ᵉ) ⟩ ≈⟨ ⟨⟩-cong₂ preservesᶠ preservesᵍ ⟩
+ ⟨ ((f′ +₁ id) ∘ h) #ᵃ , ((g′ +₁ id) ∘ h) #ᵇ ⟩ ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₁ identity²))) (#ᵇ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₂ identity²))) ⟩
+ ⟨ ((π₁ ∘ ⟨ f′ , g′ ⟩ +₁ id ∘ id) ∘ h) #ᵃ , ((π₂ ∘ ⟨ f′ , g′ ⟩ +₁ id ∘ id) ∘ h) #ᵇ ⟩ ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (pullˡ +₁∘+₁)) (#ᵇ-resp-≈ (pullˡ +₁∘+₁)) ⟩
+ ⟨ ((π₁ +₁ id) ∘ (⟨ f′ , g′ ⟩ +₁ id) ∘ h) #ᵃ , ((π₂ +₁ id) ∘ (⟨ f′ , g′ ⟩ +₁ id) ∘ h) #ᵇ ⟩ ∎ }
+ ; project₁ = project₁
+ ; project₂ = project₂
+ ; unique = ⟨⟩-unique
+ }
+ where
+ open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
+ open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity; #-Folding to #ᵇ-Folding; #-resp-≈ to #ᵇ-resp-≈)
+ open Elgot-Algebra (Product-Elgot-Algebra {EA} {EB}) using () renaming (_# to _#ᵖ)
+
+
+ -- if the carrier is cartesian, so is the category of algebras
+ Cartesian-Elgot-Algebras : Cartesian Elgot-Algebras
+ Cartesian-Elgot-Algebras = record
+ { terminal = Terminal-Elgot-Algebras
+ ; products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB }
+ }
+```
\ No newline at end of file
diff --git a/agda/src/Monad/Instance/Delay.lagda.md b/agda/src/Monad/Instance/Delay.lagda.md
index decadd8..be02b23 100644
--- a/agda/src/Monad/Instance/Delay.lagda.md
+++ b/agda/src/Monad/Instance/Delay.lagda.md
@@ -1,7 +1,5 @@
<!--
```agda
-{-# OPTIONS --no-lossy-unification #-}
-
open import Level
open import Categories.Category
open import Categories.Monad
diff --git a/agda/src/Monad/Instance/Delay/Quotienting.lagda.md b/agda/src/Monad/Instance/Delay/Quotienting.lagda.md
index 0caa000..ca8642a 100644
--- a/agda/src/Monad/Instance/Delay/Quotienting.lagda.md
+++ b/agda/src/Monad/Instance/Delay/Quotienting.lagda.md
@@ -1,6 +1,5 @@
<!--
```agda
-{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Categories.Functor
diff --git a/agda/src/Monad/Instance/Delay/Strong.lagda.md b/agda/src/Monad/Instance/Delay/Strong.lagda.md
index 0dbae41..537d234 100644
--- a/agda/src/Monad/Instance/Delay/Strong.lagda.md
+++ b/agda/src/Monad/Instance/Delay/Strong.lagda.md
@@ -1,6 +1,5 @@
<!--
```agda
-{-# OPTIONS --no-lossy-unification #-}
open import Level
open import Data.Product using (_,_; proj₁; proj₂)
diff --git a/agda/src/Monad/Instance/K.lagda.md b/agda/src/Monad/Instance/K.lagda.md
index 5689fd9..09e23c9 100644
--- a/agda/src/Monad/Instance/K.lagda.md
+++ b/agda/src/Monad/Instance/K.lagda.md
@@ -17,8 +17,7 @@ open import Categories.Monad.Construction.Kleisli
```agda
module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
- open import Category.Construction.ElgotAlgebras {C = C}
- open Cat cocartesian using (Elgot-Algebras)
+ open import Category.Construction.ElgotAlgebras cocartesian
open import Algebra.Elgot cocartesian using (Elgot-Algebra)
open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
diff --git a/agda/src/Monad/Instance/K/Commutative.lagda.md b/agda/src/Monad/Instance/K/Commutative.lagda.md
index fc20b1a..0ee436f 100644
--- a/agda/src/Monad/Instance/K/Commutative.lagda.md
+++ b/agda/src/Monad/Instance/K/Commutative.lagda.md
@@ -1,7 +1,5 @@
<!--
```agda
-{-# OPTIONS --no-lossy-unification #-}
-
open import Level
open import Category.Ambient using (Ambient)
open import Categories.Monad.Commutative
@@ -20,8 +18,7 @@ open MIK ambient
open MonadK MK
open import Monad.Instance.K.Strong ambient MK
open import Monad.Instance.K.EquationalLifting ambient MK
-open import Category.Construction.ElgotAlgebras {C = C}
-open Cat cocartesian
+open import Category.Construction.ElgotAlgebras cocartesian
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra; IsStableFreeElgotAlgebraˡ; isStable⇒isStableˡ)
diff --git a/agda/src/Monad/Instance/K/EquationalLifting.lagda.md b/agda/src/Monad/Instance/K/EquationalLifting.lagda.md
index 3c6166c..cbb9e87 100644
--- a/agda/src/Monad/Instance/K/EquationalLifting.lagda.md
+++ b/agda/src/Monad/Instance/K/EquationalLifting.lagda.md
@@ -18,8 +18,7 @@ open Ambient ambient
open MIK ambient
open MonadK MK
open import Monad.Instance.K.Strong ambient MK
-open import Category.Construction.ElgotAlgebras {C = C}
-open Cat cocartesian
+open import Category.Construction.ElgotAlgebras cocartesian
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
diff --git a/agda/src/Monad/Instance/K/PreElgot.lagda.md b/agda/src/Monad/Instance/K/PreElgot.lagda.md
index a509f7b..93b2785 100644
--- a/agda/src/Monad/Instance/K/PreElgot.lagda.md
+++ b/agda/src/Monad/Instance/K/PreElgot.lagda.md
@@ -24,8 +24,7 @@ open import Monad.Instance.K ambient
open import Monad.Instance.K.Commutative ambient MK
open import Monad.Instance.K.Strong ambient MK
open import Category.Construction.PreElgotMonads ambient
-open import Category.Construction.ElgotAlgebras {C = C}
-open Cat cocartesian
+open import Category.Construction.ElgotAlgebras cocartesian
open Equiv
open HomReasoning
diff --git a/agda/src/Monad/Instance/K/Strong.lagda.md b/agda/src/Monad/Instance/K/Strong.lagda.md
index 1406a40..3c793fe 100644
--- a/agda/src/Monad/Instance/K/Strong.lagda.md
+++ b/agda/src/Monad/Instance/K/Strong.lagda.md
@@ -22,8 +22,7 @@ import Monad.Instance.K as MIK
```agda
module Monad.Instance.K.Strong {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
open Ambient ambient
- open import Category.Construction.ElgotAlgebras {C = C}
- open Cat cocartesian
+ open import Category.Construction.ElgotAlgebras cocartesian
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
diff --git a/agda/src/Monad/Instance/K/StrongPreElgot.lagda.md b/agda/src/Monad/Instance/K/StrongPreElgot.lagda.md
index 0730dc6..20aa07d 100644
--- a/agda/src/Monad/Instance/K/StrongPreElgot.lagda.md
+++ b/agda/src/Monad/Instance/K/StrongPreElgot.lagda.md
@@ -30,8 +30,7 @@ open import Monad.Instance.K.Commutative ambient MK
open import Monad.Instance.K.Strong ambient MK
open import Monad.Instance.K.PreElgot ambient MK
open import Category.Construction.StrongPreElgotMonads ambient
-open import Category.Construction.ElgotAlgebras {C = C}
-open Cat cocartesian
+open import Category.Construction.ElgotAlgebras cocartesian
open Equiv
open HomReasoning
diff --git a/agda/src/Monad/Instance/Setoids/Delay.lagda.md b/agda/src/Monad/Instance/Setoids/Delay.lagda.md
index 38bac63..6ccfc54 100644
--- a/agda/src/Monad/Instance/Setoids/Delay.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/Delay.lagda.md
@@ -1,5 +1,5 @@
```agda
-{-# OPTIONS --allow-unsolved-metas --guardedness #-}
+{-# OPTIONS --guardedness #-}
open import Level renaming (zero to ℓ-zero; suc to ℓ-suc)
open import Function.Bundles using (_⟨$⟩_) renaming (Func to _⟶_)
@@ -66,13 +66,6 @@ module Bisimilarity (A : Setoid c (c ⊔ ℓ)) where
open _∼′_ public
- record _∼′′_ (x y : Delay′ ∣ A ∣) : Set (c ⊔ ℓ) where
- coinductive
-
- field
- force∼′′ : force x ∼ force y
- open _∼′′_ public
-
-- strong bisimilarity of now and later leads to a clash
now∼later : ∀ {ℓ'}{Z : Set ℓ'}{x : ∣ A ∣}{y : Delay′ ∣ A ∣} → now x ∼ later y → Z
now∼later ()
@@ -179,7 +172,7 @@ module Bisimilarity (A : Setoid c (c ⊔ ℓ)) where
open _≲′_ public
-open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _∼′′_ to [_][_∼′′_]; _↓_ to [_][_↓_]; _≲_ to [_][_≲_]; _≲′_ to [_][_≲′_])
+open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_]; _≲_ to [_][_≲_]; _≲′_ to [_][_≲′_])
module DelayMonad where
@@ -187,8 +180,6 @@ module DelayMonad where
Delayₛ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } }
Delayₛ∼ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
Delayₛ∼ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } }
- Delayₛ∼′ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
- Delayₛ∼′ A = record { Carrier = Delay′ ∣ A ∣ ; _≈_ = [_][_∼′′_] A ; isEquivalence = {! !} }
<_> = _⟨$⟩_
open _⟶_ using (cong)
diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index f725555..46dc08f 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -1,6 +1,6 @@
<!--
```agda
-{-# OPTIONS --allow-unsolved-metas --guardedness #-}
+{-# OPTIONS --guardedness #-}
open import Level renaming (zero to ℓ-zero; suc to ℓ-suc)
open import Relation.Binary
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
@@ -36,8 +36,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian
open import Algebra.Elgot.Stable distributive
- open import Category.Construction.ElgotAlgebras {C = Setoids ℓ ℓ}
- open Cat cocartesian
+ open import Category.Construction.ElgotAlgebras {C = Setoids ℓ ℓ} cocartesian
open import Monad.PreElgot (setoidAmbient {ℓ})
open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_])
open DelayMonad
@@ -388,8 +387,8 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
iter-id {later x} = later≈ (iter-id′ {force x})
open CartesianClosed (Setoids-CCC ℓ) renaming (exp to setoid-exp)
- open import Algebra.Elgot.Properties distributive setoid-exp using (free-isStableˡ)
+ open import Algebra.Elgot.Properties distributive setoid-exp using (free-isStable)
delayK : MonadK
- delayK = record { freealgebras = freeAlgebra ; stable = λ X → isStableˡ⇒isStable (freeAlgebra X) (free-isStableˡ (freeAlgebra X)) }
+ delayK = record { freealgebras = freeAlgebra ; stable = λ X → free-isStable (freeAlgebra X) }
```
\ No newline at end of file