leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

refactor elgot algebras

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-01 10:29:03 +01:00
parent aea11ac62f
commit 85195b13d0
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
8 changed files with 590 additions and 416 deletions

2
agda/bsc.agda-lib
View file

@ -1,3 +1,3 @@
name: bsc
include: src/
depend: standard-library agda-categories
depend: standard-library agda-categories

290
agda/src/Algebra/Elgot.lagda.md
View file

@ -3,13 +3,17 @@
open import Level
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Algebra
open import Category.Ambient using (Ambient)
open import Categories.Category.Core using (Category)
open import Categories.Category.Cocartesian
import Categories.Morphism.Reasoning as MR
```
-->
```agda
module Algebra.Elgot {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
module Algebra.Elgot {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
open Category C
open Cocartesian cocartesian
open MR C
```
@ -29,12 +33,12 @@ Guarded Elgot algebras are algebras on an endofunctor together with an iteration
-- _# properties
field
#-Fixpoint : ∀ {X} {f : X ⇒ A + F₀ X }
→ f # ≈ [ idC , α ∘ F₁ (f #) ] ∘ f
→ f # ≈ [ id , α ∘ F₁ (f #) ] ∘ f
#-Uniformity : ∀ {X Y} {f : X ⇒ A + F₀ X} {g : Y ⇒ A + F₀ Y} {h : X ⇒ Y}
→ (idC +₁ F₁ h) ∘ f ≈ g ∘ h
→ (id +₁ F₁ h) ∘ f ≈ g ∘ h
→ f # ≈ g # ∘ h
#-Compositionality : ∀ {X Y} {f : X ⇒ A + F₀ X} {h : Y ⇒ X + F₀ Y}
→ (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ (F₁ i₁)) ∘ f , i₂ ∘ (F₁ i₂) ] ∘ [ i₁ , h ])# ∘ i₂
→ (((f #) +₁ id) ∘ h)# ≈ ([ (id +₁ (F₁ i₁)) ∘ f , i₂ ∘ (F₁ i₂) ] ∘ [ i₁ , h ])# ∘ i₂
#-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X}
→ f ≈ g
→ (f #) ≈ (g #)
@ -59,12 +63,12 @@ Here we give a different (easier) Characterization and show that it is equal.
-- _# properties
field
#-Fixpoint : ∀ {X} {f : X ⇒ A + X }
→ f # ≈ [ idC , f # ] ∘ f
→ f # ≈ [ id , f # ] ∘ f
#-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y}
→ (idC +₁ h) ∘ f ≈ g ∘ h
→ (id +₁ h) ∘ f ≈ g ∘ h
→ f # ≈ g # ∘ h
#-Folding : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
→ ((f #) +₁ h)# ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #
→ ((f #) +₁ h)# ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] #
#-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #)
open HomReasoning
@ -72,126 +76,126 @@ Here we give a different (easier) Characterization and show that it is equal.
-- Compositionality is derivable
#-Compositionality : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
→ (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂
→ (((f #) +₁ id) ∘ h)# ≈ ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂
#-Compositionality {X} {Y} {f} {h} = begin
(((f #) +₁ idC) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h}
(((f #) +₁ id) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ id) ∘ h}
{g = (f #) +₁ h}
{h = h}
(trans (pullˡ +₁∘+₁) (+₁-cong₂ identityˡ identityʳ ⟩∘⟨refl))⟩
((f # +₁ h)# ∘ h) ≈˘⟨ inject₂ ⟩
(([ idC ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂)) ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
(([ idC , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂) ≈˘⟨ #-Fixpoint {f = (f # +₁ h) } ⟩∘⟨refl ⟩
(([ id ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂)) ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
(([ id , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂) ≈˘⟨ #-Fixpoint {f = (f # +₁ h) } ⟩∘⟨refl ⟩
(f # +₁ h)# ∘ i₂ ≈⟨ #-Folding ⟩∘⟨refl ⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂) ≈⟨ #-Fixpoint ⟩∘⟨refl ⟩
([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ]
∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂ ≈⟨ pullʳ inject₂ ⟩
[ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ (i₂ ∘ h) ≈⟨ pullˡ inject₂ ⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h) ≈˘⟨ refl⟩∘⟨ inject₂ {f = i₁} {g = h} ⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ] ∘ i₂) ≈˘⟨ pushˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]}
{g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]}
([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂) ≈⟨ #-Fixpoint ⟩∘⟨refl ⟩
([ id , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ]
∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂ ≈⟨ pullʳ inject₂ ⟩
[ id , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ (i₂ ∘ h) ≈⟨ pullˡ inject₂ ⟩
([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h) ≈˘⟨ refl⟩∘⟨ inject₂ {f = i₁} {g = h} ⟩
([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ] ∘ i₂) ≈˘⟨ pushˡ (#-Uniformity {f = [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]}
{g = [ (id +₁ i₁) ∘ f , i₂ ∘ h ]}
{h = [ i₁ , h ]}
(begin
(idC +₁ [ i₁ , h ])
∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ refl⟩∘⟨ ∘[] ⟩
(idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁
, [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ refl⟩∘⟨ []-congʳ inject₁ ⟩
(idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f
, [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘[] ⟩
[ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f)
, (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ ∘[]) ⟩
[ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
, [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f)
, (idC +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ] ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁)))
(id +₁ [ i₁ , h ])
∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ refl⟩∘⟨ ∘[] ⟩
(id +₁ [ i₁ , h ]) ∘ [ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁
, [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ refl⟩∘⟨ []-congʳ inject₁ ⟩
(id +₁ [ i₁ , h ]) ∘ [ (id +₁ i₁) ∘ f
, [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘[] ⟩
[ (id +₁ [ i₁ , h ]) ∘ ((id +₁ i₁) ∘ f)
, (id +₁ [ i₁ , h ]) ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ ∘[]) ⟩
[ ((id ∘ id) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
, [ (id +₁ [ i₁ , h ]) ∘ ((id +₁ i₁) ∘ f)
, (id +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ] ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁)))
(∘-resp-≈ˡ ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ inject₂))) ⟩
[ (idC +₁ i₁) ∘ f , ([ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
[ (id +₁ i₁) ∘ f , ([ ((id ∘ id) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
, (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁))
(pullʳ inject₂))) ⟩
[ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ []-congʳ inject₁ ⟩
[ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁
, [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ ∘[] ⟩
[ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎))
[ (id +₁ i₁) ∘ f , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ []-congʳ inject₁ ⟩
[ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁
, [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ ∘[] ⟩
[ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎))
⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ ∎
([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ ∎
#-Stutter : ∀ {X Y} (f : X ⇒ (Y + Y) + X) (h : Y ⇒ A) → (([ h , h ] +₁ idC) ∘ f)# ≈ [ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂
#-Stutter : ∀ {X Y} (f : X ⇒ (Y + Y) + X) (h : Y ⇒ A) → (([ h , h ] +₁ id) ∘ f)# ≈ [ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂
#-Stutter {X} {Y} f h = begin
(([ h , h ] +₁ idC) ∘ f)# ≈⟨ #-resp-≈ ((+₁-cong₂ (sym help) refl) ⟩∘⟨refl) ⟩
(((h +₁ i₁) # +₁ idC) ∘ f) # ≈⟨ #-Compositionality ⟩
([ (idC +₁ i₁) ∘ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂ ≈⟨ ((#-resp-≈ (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
(([ h , h ] +₁ id) ∘ f)# ≈⟨ #-resp-≈ ((+₁-cong₂ (sym help) refl) ⟩∘⟨refl) ⟩
(((h +₁ i₁) # +₁ id) ∘ f) # ≈⟨ #-Compositionality ⟩
([ (id +₁ i₁) ∘ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂ ≈⟨ ((#-resp-≈ (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂ ≈˘⟨ (refl⟩∘⟨ (+₁∘i₂ ○ identityʳ)) ⟩
([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ (i₁ +₁ idC) ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity (sym by-uni))) ⟩
([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ (i₁ +₁ id) ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity (sym by-uni))) ⟩
[ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂ ∎
where
help : (h +₁ i₁) # ≈ [ h , h ]
help = begin
((h +₁ i₁) #) ≈⟨ #-Fixpoint ⟩
[ idC , (h +₁ i₁) # ] ∘ (h +₁ i₁) ≈⟨ []∘+₁ ○ []-cong₂ identityˡ refl ⟩
[ id , (h +₁ i₁) # ] ∘ (h +₁ i₁) ≈⟨ []∘+₁ ○ []-cong₂ identityˡ refl ⟩
[ h , (h +₁ i₁) # ∘ i₁ ] ≈⟨ []-cong₂ refl (#-Fixpoint ⟩∘⟨refl) ⟩
[ h , ([ idC , (h +₁ i₁) # ] ∘ (h +₁ i₁)) ∘ i₁ ] ≈⟨ []-cong₂ refl (pullʳ +₁∘i₁) ⟩
[ h , [ idC , (h +₁ i₁) # ] ∘ i₁ ∘ h ] ≈⟨ []-cong₂ refl (cancelˡ inject₁) ⟩
[ h , ([ id , (h +₁ i₁) # ] ∘ (h +₁ i₁)) ∘ i₁ ] ≈⟨ []-cong₂ refl (pullʳ +₁∘i₁) ⟩
[ h , [ id , (h +₁ i₁) # ] ∘ i₁ ∘ h ] ≈⟨ []-cong₂ refl (cancelˡ inject₁) ⟩
[ h , h ] ∎
by-uni : ([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ idC) ≈ (idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]
by-uni : ([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ id) ≈ (id +₁ (i₁ +₁ id)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]
by-uni = begin
([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ idC) ≈⟨ ((∘[] ○ []-cong₂ inject₁ refl) ⟩∘⟨refl) ⟩
[ h +₁ i₁ ∘ i₁ , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ∘ (i₁ +₁ idC) ≈⟨ ([]∘+₁ ○ []-cong₂ +₁∘i₁ identityʳ) ⟩
([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ id) ≈⟨ ((∘[] ○ []-cong₂ inject₁ refl) ⟩∘⟨refl) ⟩
[ h +₁ i₁ ∘ i₁ , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ∘ (i₁ +₁ id) ≈⟨ ([]∘+₁ ○ []-cong₂ +₁∘i₁ identityʳ) ⟩
[ i₁ ∘ h , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ (pullˡ (+₁∘i₁ ○ identityʳ)) (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ +₁∘i₁) (pullˡ +₁∘i₂ ○ pullʳ (+₁∘i₂ ○ identityʳ))) ⟩∘⟨refl) ⟩
[ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , [ (idC +₁ (i₁ +₁ idC)) ∘ (h +₁ i₁) , (idC +₁ (i₁ +₁ idC)) ∘ i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ refl (pullˡ ∘[]) ⟩
[ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ ∘[] ⟩
(idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ∎
[ (id +₁ (i₁ +₁ id)) ∘ i₁ ∘ h , [ (id +₁ (i₁ +₁ id)) ∘ (h +₁ i₁) , (id +₁ (i₁ +₁ id)) ∘ i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ refl (pullˡ ∘[]) ⟩
[ (id +₁ (i₁ +₁ id)) ∘ i₁ ∘ h , (id +₁ (i₁ +₁ id)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ ∘[] ⟩
(id +₁ (i₁ +₁ id)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ∎
#-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) → ((idC +₁ [ idC , idC ]) ∘ f)# ≈ ([ i₁ , ((idC +₁ [ idC , idC ]) ∘ f) # +₁ idC ] ∘ f) #
#-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) → ((id +₁ [ id , id ]) ∘ f)# ≈ ([ i₁ , ((id +₁ [ id , id ]) ∘ f) # +₁ id ] ∘ f) #
#-Diamond {X} f = begin
g # ≈⟨ introʳ inject₂ ⟩
g # ∘ [ idC , idC ] ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity by-uni₁)) ⟩
[ (idC +₁ i₁) ∘ g , f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩∘⟨refl) ⟩
[ (idC +₁ i₁) ∘ g , (idC +₁ idC) ∘ f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₁ identityˡ)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identityˡ)))) ⟩∘⟨refl) ⟩
[ ([ idC , idC ] +₁ idC) ∘ ((i₁ +₁ i₁) ∘ g) , ([ idC , idC ] +₁ idC) ∘ ((i₂ +₁ idC) ∘ f) ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ∘[]) ⟩∘⟨refl) ⟩
(([ idC , idC ] +₁ idC) ∘ [ ((i₁ +₁ i₁) ∘ g) , ((i₂ +₁ idC) ∘ f) ]) # ∘ i₂ ≈⟨ ((#-Stutter [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ] idC) ⟩∘⟨refl) ⟩
([ i₁ ∘ idC , [ idC +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ] ] # ∘ i₂) ∘ i₂ ≈⟨ (assoc ○ ((#-resp-≈ ([]-cong₂ identityʳ refl)) ⟩∘⟨refl)) ⟩
[ i₁ , ([ idC +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ]) ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl (∘[] ○ []-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁)))) ⟩∘⟨refl) ⟩
[ i₁ , [ [ (idC +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (idC +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ idC ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
g # ∘ [ id , id ] ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity by-uni₁)) ⟩
[ (id +₁ i₁) ∘ g , f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (elimˡ (+-unique id-comm-sym id-comm-sym)))) ⟩∘⟨refl) ⟩
[ (id +₁ i₁) ∘ g , (id +₁ id) ∘ f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₁ identityˡ)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identityˡ)))) ⟩∘⟨refl) ⟩
[ ([ id , id ] +₁ id) ∘ ((i₁ +₁ i₁) ∘ g) , ([ id , id ] +₁ id) ∘ ((i₂ +₁ id) ∘ f) ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ∘[]) ⟩∘⟨refl) ⟩
(([ id , id ] +₁ id) ∘ [ ((i₁ +₁ i₁) ∘ g) , ((i₂ +₁ id) ∘ f) ]) # ∘ i₂ ≈⟨ ((#-Stutter [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ id) ∘ f ] id) ⟩∘⟨refl) ⟩
([ i₁ ∘ id , [ id +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ id) ∘ f ] ] # ∘ i₂) ∘ i₂ ≈⟨ (assoc ○ ((#-resp-≈ ([]-cong₂ identityʳ refl)) ⟩∘⟨refl)) ⟩
[ i₁ , ([ id +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ id) ∘ f ]) ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl (∘[] ○ []-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁)))) ⟩∘⟨refl) ⟩
[ i₁ , [ [ (id +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (id +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ id ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
[ i₁ , [ [ i₁ , i₂ ∘ i₂ ∘ i₁ ] ∘ g , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl)) (∘[] ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
[ i₁ , [ [ i₁ , i₂ ] ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
[ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ pullˡ (sym (#-Uniformity by-uni₂)) ⟩
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ i₂ ∘ i₂ ≈⟨ (refl⟩∘⟨ (pullˡ inject₂ ○ (+₁∘i₂ ○ identityʳ))) ⟩
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ {A = A + X} {B = X} ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩
[ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩
([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩
([ idC , g # ] +₁ h ) # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ((sym ∘[] ○ elimʳ +-η) ⟩∘⟨refl))) ⟩∘⟨refl) ⟩
[ i₁ ∘ [ idC , g # ] , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ h ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (pullˡ ([]∘+₁ ○ []-cong₂ inject₂ identityʳ)))) ⟩∘⟨refl) ⟩
[ i₁ ∘ [ idC , g # ] , [ [ idC , g # ] +₁ i₁ , i₂ ∘ i₂ ] ∘ (i₂ +₁ idC) ∘ h ] # ∘ i₂ ≈⟨ sym (#-Stutter ((i₂ +₁ idC) ∘ h) [ idC , g # ]) ⟩
(([ [ idC , g # ] , [ idC , g # ] ] +₁ idC) ∘ (i₂ +₁ idC) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identity²)) ⟩
((([ idC , g # ] +₁ idC)) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) +₁∘+₁)) ⟩
([ (i₁ ∘ [ idC , g # ]) ∘ i₁ , [ idC , g # ] ∘ i₂ +₁ idC ∘ idC ] ∘ f) # ≈⟨ #-resp-≈ (([]-cong₂ (cancelʳ inject₁) (+₁-cong₂ inject₂ identity²)) ⟩∘⟨refl) ⟩
([ i₁ , g # +₁ idC ] ∘ f) # ∎
[ i₁ , [ [ i₁ , i₂ ] ∘ (id +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
[ i₁ , [ (id +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ pullˡ (sym (#-Uniformity by-uni₂)) ⟩
[ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ i₂ ∘ i₂ ≈⟨ (refl⟩∘⟨ (pullˡ inject₂ ○ (+₁∘i₂ ○ identityʳ))) ⟩
[ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ {A = A + X} {B = X} ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩
[ (id +₁ i₁) ∘ [ i₁ , (id +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩
([ i₁ , (id +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩
([ id , g # ] +₁ h ) # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ((sym ∘[] ○ elimʳ +-η) ⟩∘⟨refl))) ⟩∘⟨refl) ⟩
[ i₁ ∘ [ id , g # ] , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ h ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (pullˡ ([]∘+₁ ○ []-cong₂ inject₂ identityʳ)))) ⟩∘⟨refl) ⟩
[ i₁ ∘ [ id , g # ] , [ [ id , g # ] +₁ i₁ , i₂ ∘ i₂ ] ∘ (i₂ +₁ id) ∘ h ] # ∘ i₂ ≈⟨ sym (#-Stutter ((i₂ +₁ id) ∘ h) [ id , g # ]) ⟩
(([ [ id , g # ] , [ id , g # ] ] +₁ id) ∘ (i₂ +₁ id) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identity²)) ⟩
((([ id , g # ] +₁ id)) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) +₁∘+₁)) ⟩
([ (i₁ ∘ [ id , g # ]) ∘ i₁ , [ id , g # ] ∘ i₂ +₁ id ∘ id ] ∘ f) # ≈⟨ #-resp-≈ (([]-cong₂ (cancelʳ inject₁) (+₁-cong₂ inject₂ identity²)) ⟩∘⟨refl) ⟩
([ i₁ , g # +₁ id ] ∘ f) # ∎
where
g = (idC +₁ [ idC , idC ]) ∘ f
h = [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f
by-uni₂ : (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ]
g = (id +₁ [ id , id ]) ∘ f
h = [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f
by-uni₂ : (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ [ i₁ , [ (id +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈ [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ id ]
by-uni₂ = begin
(idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈⟨ ∘[] ⟩
[ (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ i₁ , (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈⟨ []-cong₂ (+₁∘i₁ ○ identityʳ) ∘[] ⟩
[ i₁ , [ (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ i₂ ∘ f ] ] ≈⟨ []-cong₂ refl ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂)) ⟩
[ i₁ , [ (idC ∘ idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ f ] ] ≈⟨ []-cong₂ refl ([]-cong₂ ((+₁-cong₂ identity² (pullˡ inject₂ ○ +₁∘i₁)) ⟩∘⟨refl) (∘[] ⟩∘⟨refl)) ⟩
[ i₁ , [ (idC +₁ i₁ ∘ i₂) ∘ g , [ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ idC) ] ∘ f ] ] ≈˘⟨ []-cong₂ refl ([]-cong₂ refl (pullˡ ∘[])) ⟩
[ i₁ , [ (idC +₁ i₁ ∘ i₂) ∘ g , i₂ ∘ h ] ] ≈˘⟨ []-cong₂ inject₁ ([]-cong₂ inject₂ identityʳ) ⟩
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] ∘ i₁ , [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] ∘ i₂ , (i₂ ∘ h) ∘ idC ] ] ≈˘⟨ []-cong₂ (pullˡ inject₁) []∘+₁ ⟩
[ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₁ ∘ i₁ , [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ (i₂ +₁ idC) ] ≈˘⟨ ∘[] ⟩
[ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∎
by-uni₁ : (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈ g ∘ [ idC , idC ]
(id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ [ i₁ , [ (id +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈⟨ ∘[] ⟩
[ (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ i₁ , (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ [ (id +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈⟨ []-cong₂ (+₁∘i₁ ○ identityʳ) ∘[] ⟩
[ i₁ , [ (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ (id +₁ i₂ ∘ i₁) ∘ g , (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ i₂ ∘ f ] ] ≈⟨ []-cong₂ refl ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂)) ⟩
[ i₁ , [ (id ∘ id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ f ] ] ≈⟨ []-cong₂ refl ([]-cong₂ ((+₁-cong₂ identity² (pullˡ inject₂ ○ +₁∘i₁)) ⟩∘⟨refl) (∘[] ⟩∘⟨refl)) ⟩
[ i₁ , [ (id +₁ i₁ ∘ i₂) ∘ g , [ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ id) ] ∘ f ] ] ≈˘⟨ []-cong₂ refl ([]-cong₂ refl (pullˡ ∘[])) ⟩
[ i₁ , [ (id +₁ i₁ ∘ i₂) ∘ g , i₂ ∘ h ] ] ≈˘⟨ []-cong₂ inject₁ ([]-cong₂ inject₂ identityʳ) ⟩
[ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] ∘ i₁ , [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] ∘ i₂ , (i₂ ∘ h) ∘ id ] ] ≈˘⟨ []-cong₂ (pullˡ inject₁) []∘+₁ ⟩
[ [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₁ ∘ i₁ , [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ (i₂ +₁ id) ] ≈˘⟨ ∘[] ⟩
[ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ id ] ∎
by-uni₁ : (id +₁ [ id , id ]) ∘ [ (id +₁ i₁) ∘ g , f ] ≈ g ∘ [ id , id ]
by-uni₁ = begin
(idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈⟨ ∘[] ⟩
[ (idC +₁ [ idC , idC ]) ∘ (idC +₁ i₁) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² inject₁)) refl ⟩
[ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩
(id +₁ [ id , id ]) ∘ [ (id +₁ i₁) ∘ g , f ] ≈⟨ ∘[] ⟩
[ (id +₁ [ id , id ]) ∘ (id +₁ i₁) ∘ g , (id +₁ [ id , id ]) ∘ f ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² inject₁)) refl ⟩
[ (id +₁ id) ∘ g , (id +₁ [ id , id ]) ∘ f ] ≈⟨ []-cong₂ (elimˡ (+-unique id-comm-sym id-comm-sym)) refl ⟩
[ g , g ] ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩
g ∘ [ idC , idC ] ∎
by-fix : [ i₁ , (idC +₁ i₂) ∘ g ] # ≈ [ idC , g # ]
g ∘ [ id , id ] ∎
by-fix : [ i₁ , (id +₁ i₂) ∘ g ] # ≈ [ id , g # ]
by-fix = sym (begin
[ idC , g # ] ≈⟨ []-cong₂ refl #-Fixpoint ⟩
[ idC , [ idC , g # ] ∘ g ] ≈⟨ []-cong₂ refl (([]-cong₂ refl (#-Uniformity (sym inject₂))) ⟩∘⟨refl) ⟩
[ idC , [ idC , [ i₁ , (idC +₁ i₂) ∘ g ] # ∘ i₂ ] ∘ g ] ≈˘⟨ ∘[] ○ []-cong₂ inject₁ (pullˡ ([]∘+₁ ○ []-cong₂ identity² refl)) ⟩
[ idC , [ i₁ , (idC +₁ i₂) ∘ g ] # ] ∘ [ i₁ , (idC +₁ i₂) ∘ g ] ≈˘⟨ #-Fixpoint ⟩
([ i₁ , (idC +₁ i₂) ∘ g ] #) ∎)
[ id , g # ] ≈⟨ []-cong₂ refl #-Fixpoint ⟩
[ id , [ id , g # ] ∘ g ] ≈⟨ []-cong₂ refl (([]-cong₂ refl (#-Uniformity (sym inject₂))) ⟩∘⟨refl) ⟩
[ id , [ id , [ i₁ , (id +₁ i₂) ∘ g ] # ∘ i₂ ] ∘ g ] ≈˘⟨ ∘[] ○ []-cong₂ inject₁ (pullˡ ([]∘+₁ ○ []-cong₂ identity² refl)) ⟩
[ id , [ i₁ , (id +₁ i₂) ∘ g ] # ] ∘ [ i₁ , (id +₁ i₂) ∘ g ] ≈˘⟨ #-Fixpoint ⟩
([ i₁ , (id +₁ i₂) ∘ g ] #) ∎)
-- every elgot-algebra comes with a divergence constant
!ₑ : ⊥ ⇒ A
@ -213,7 +217,7 @@ First we show how to get an Id-guarded algebra from a unguarded one and vice ver
Id-Algebra : Obj → F-Algebra (idF {C = C})
Id-Algebra A = record
{ A = A
; α = idC
; α = id
}
where open Functor (idF {C = C})
@ -242,8 +246,8 @@ First we show how to get an Id-guarded algebra from a unguarded one and vice ver
; #-Folding = λ {X} {Y} {f} {h} → begin
((f #) +₁ h) # ≈˘⟨ +-g-η ⟩
[ (f # +₁ h)# ∘ i₁ , (f # +₁ h)# ∘ i₂ ] ≈⟨ []-cong₂ left right ⟩
[ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #) ∎
[ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩
([ (id +₁ i₁) ∘ f , i₂ ∘ h ] #) ∎
; #-resp-≈ = #-resp-≈
}
}
@ -252,68 +256,68 @@ First we show how to get an Id-guarded algebra from a unguarded one and vice ver
open HomReasoning
open Equiv
left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
→ (f # +₁ h)# ∘ i₁ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁
→ (f # +₁ h)# ∘ i₁ ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁
left {X} {Y} {f} {h} = begin
(f # +₁ h)# ∘ i₁ ≈⟨ #-Fixpoint ⟩∘⟨refl ⟩
([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₁ ≈⟨ pullʳ +₁∘i₁ ⟩
[ idC , idC ∘ (((f #) +₁ h) #) ] ∘ (i₁ ∘ f #) ≈⟨ cancelˡ inject₁ ⟩
([ id , id ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₁ ≈⟨ pullʳ +₁∘i₁ ⟩
[ id , id ∘ (((f #) +₁ h) #) ] ∘ (i₁ ∘ f #) ≈⟨ cancelˡ inject₁ ⟩
(f #) ≈⟨ #-Uniformity {f = f}
{g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]}
{g = [ (id +₁ i₁) ∘ f , i₂ ∘ h ]}
{h = i₁}
(sym inject₁)⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁) ∎
([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁) ∎
byUni : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
→ (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]
→ (id +₁ [ i₁ , h ]) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]
byUni {X} {Y} {f} {h} = begin
(idC +₁ [ i₁ , h ])
∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ ∘-resp-≈ʳ (trans ∘[] ([]-congʳ inject₁)) ⟩
(idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f
, [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘[] ⟩
[ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f)
, (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩
[ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f
, ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩
[ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
, [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f)
, (idC +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ] ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁)))
(id +₁ [ i₁ , h ])
∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ ∘-resp-≈ʳ (trans ∘[] ([]-congʳ inject₁)) ⟩
(id +₁ [ i₁ , h ]) ∘ [ (id +₁ i₁) ∘ f
, [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘[] ⟩
[ (id +₁ [ i₁ , h ]) ∘ ((id +₁ i₁) ∘ f)
, (id +₁ [ i₁ , h ]) ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩
[ ((id +₁ [ i₁ , h ]) ∘ (id +₁ i₁)) ∘ f
, ((id +₁ [ i₁ , h ]) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩
[ ((id ∘ id) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
, [ (id +₁ [ i₁ , h ]) ∘ ((id +₁ i₁) ∘ f)
, (id +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ] ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁)))
(∘-resp-≈ˡ ([]-cong₂ sym-assoc sym-assoc)) ⟩
[ (idC +₁ i₁) ∘ f
, [ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f
, ((idC +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ] ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩
[ (idC +₁ i₁) ∘ f
, [ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
[ (id +₁ i₁) ∘ f
, [ ((id +₁ [ i₁ , h ]) ∘ (id +₁ i₁)) ∘ f
, ((id +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ] ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩
[ (id +₁ i₁) ∘ f
, [ ((id ∘ id) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f
, (i₂ ∘ [ i₁ , h ]) ∘ i₂ ] ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩
[ (idC +₁ i₁) ∘ f
, [ (idC +₁ i₁) ∘ f
[ (id +₁ i₁) ∘ f
, [ (id +₁ i₁) ∘ f
, i₂ ∘ ([ i₁ , h ] ∘ i₂) ] ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩
[ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ []-congʳ inject₁ ⟩
[ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁
, [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ ∘[] ⟩
[ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎
[ (id +₁ i₁) ∘ f , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ []-congʳ inject₁ ⟩
[ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁
, [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈˘⟨ ∘[] ⟩
[ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎
right : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
→ (f # +₁ h)# ∘ i₂ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂
→ (f # +₁ h)# ∘ i₂ ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂
right {X} {Y} {f} {h} = begin
(f # +₁ h)# ∘ i₂ ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩
([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₂ ≈⟨ pullʳ +₁∘i₂ ⟩
[ idC , idC ∘ (((f #) +₁ h) #) ] ∘ i₂ ∘ h ≈⟨ pullˡ inject₂ ⟩
(idC ∘ (((f #) +₁ h) #)) ∘ h ≈⟨ (identityˡ ⟩∘⟨refl) ⟩
((f #) +₁ h) # ∘ h ≈˘⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h}
([ id , id ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₂ ≈⟨ pullʳ +₁∘i₂ ⟩
[ id , id ∘ (((f #) +₁ h) #) ] ∘ i₂ ∘ h ≈⟨ pullˡ inject₂ ⟩
(id ∘ (((f #) +₁ h) #)) ∘ h ≈⟨ (identityˡ ⟩∘⟨refl) ⟩
((f #) +₁ h) # ∘ h ≈˘⟨ #-Uniformity {f = ((f #) +₁ id) ∘ h}
{g = (f #) +₁ h}
{h = h}
(pullˡ (trans (+₁∘+₁) (+₁-cong₂ identityˡ identityʳ)))⟩
(((f #) +₁ idC) ∘ h) # ≈⟨ #-Compositionality ⟩
(([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂) ≈⟨ ∘-resp-≈ˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]}
{g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]}
(((f #) +₁ id) ∘ h) # ≈⟨ #-Compositionality ⟩
(([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂) ≈⟨ ∘-resp-≈ˡ (#-Uniformity {f = [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]}
{g = [ (id +₁ i₁) ∘ f , i₂ ∘ h ]}
{h = [ i₁ , h ]}
byUni)⟩
([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂ ≈⟨ pullʳ inject₂ ⟩
[ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h ≈˘⟨ inject₂ ⟩∘⟨refl ⟩
([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h ≈˘⟨ pushʳ inject₂ ⟩
[ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ]
∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈˘⟨ []-congˡ identityˡ ⟩∘⟨refl ⟩
[ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ]
∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈˘⟨ pushˡ #-Fixpoint ⟩
[ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ∎
([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂ ≈⟨ pullʳ inject₂ ⟩
[ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h ≈˘⟨ inject₂ ⟩∘⟨refl ⟩
([ id , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h ≈˘⟨ pushʳ inject₂ ⟩
[ id , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ]
∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈˘⟨ []-congˡ identityˡ ⟩∘⟨refl ⟩
[ id , id ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ]
∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈˘⟨ pushˡ #-Fixpoint ⟩
[ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ∎
```
and now we show that this transformation is isomorphic (this is just a formality, it is of course obvious, since the record fields are the **same**)

106
agda/src/Algebra/Elgot/Free.lagda.md
View file

@ -7,29 +7,37 @@ open import Categories.Functor.Core
open import Categories.Functor.Algebra
open import Categories.Functor.Coalgebra
open import Categories.Object.Terminal
open import Categories.Category.Core using (Category)
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
```
-->
```agda
module Algebra.Elgot.Free {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Algebra.Elgot ambient
open import Category.Construction.ElgotAlgebras ambient
open import Monad.Instance.Delay ambient
module Algebra.Elgot.Free {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
open import Algebra.Elgot cocartesian
open import Category.Construction.ElgotAlgebras cocartesian
open import Categories.Morphism.Properties C
open Category C
open Cocartesian cocartesian
open Equiv
open HomReasoning
open MR C
open M C
```
# (stable) free Elgot algebras
# Free Elgot algebras
A free elgot algebra is a free object in the category of Elgot algebras.
```agda
elgotForgetfulF : Functor Elgot-Algebras C
elgotForgetfulF = record
@ -43,88 +51,4 @@ A free elgot algebra is a free object in the category of Elgot algebras.
-- typedef
FreeElgotAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e)
FreeElgotAlgebra X = FreeObject {C = C} {D = Elgot-Algebras} elgotForgetfulF X
```
Stable free Elgot algebras have an additional universal iteration preserving morphism.
```agda
record IsStableFreeElgotAlgebra {Y : Obj} (freeElgot : FreeElgotAlgebra Y) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
open FreeObject freeElgot using (η) renaming (FX to FY)
open Elgot-Algebra FY using (_#)
field
-- TODO awkward notation...
[_,_]♯ : ∀ {X : Obj} (A : Elgot-Algebra) (f : X × Y ⇒ Elgot-Algebra.A A) → X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A A
♯-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ ∘ (idC ⁂ η)
♯-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ ∘ (idC ⁂ h #) ≈ Elgot-Algebra._# B (([ B , f ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))
♯-unique : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A B) (g : X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A B)
→ f ≈ g ∘ (idC ⁂ η)
→ (∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (idC ⁂ h #) ≈ Elgot-Algebra._# B ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
→ g ≈ [ B , f ]♯
[_,_]♯ˡ : ∀ {X : Obj} (A : Elgot-Algebra) (f : Y × X ⇒ Elgot-Algebra.A A) → Elgot-Algebra.A FY × X ⇒ Elgot-Algebra.A A
[_,_]♯ˡ {X} A f = [ A , (f ∘ swap) ]♯ ∘ swap
♯ˡ-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ˡ ∘ (η ⁂ idC)
♯ˡ-law {X} {A} f = begin
f ≈⟨ introʳ swap∘swap ⟩
f ∘ swap ∘ swap ≈⟨ pullˡ (♯-law (f ∘ swap)) ⟩
([ A , f ∘ swap ]♯ ∘ (idC ⁂ η)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩
[ A , (f ∘ swap) ]♯ ∘ swap ∘ (η ⁂ idC) ≈⟨ sym-assoc ⟩
([ A , (f ∘ swap) ]♯ ∘ swap) ∘ (η ⁂ idC) ∎
♯ˡ-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ˡ ∘ (h # ⁂ idC) ≈ Elgot-Algebra._# B (([ B , f ]♯ˡ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))
♯ˡ-preserving {X} {B} f {Z} h = begin
([ B , (f ∘ swap) ]♯ ∘ swap) ∘ ((h #) ⁂ idC) ≈⟨ pullʳ swap∘⁂ ⟩
[ B , (f ∘ swap) ]♯ ∘ (idC ⁂ h #) ∘ swap ≈⟨ pullˡ (♯-preserving (f ∘ swap) h) ⟩
(([ B , (f ∘ swap) ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩
((([ B , (f ∘ swap) ]♯ ∘ swap) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #ᵇ ∎
where
open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
uni-helper : (idC +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈ (([ B , f ∘ swap ]♯ coproducts.+₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap
uni-helper = begin
(idC +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩
(idC ∘ [ B , f ∘ swap ]♯ ∘ swap +₁ swap ∘ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
([ B , f ∘ swap ]♯ ∘ swap +₁ idC ∘ swap) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩
(([ B , f ∘ swap ]♯ +₁ idC) ∘ (swap +₁ swap)) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹∘swap)) ⟩
([ B , f ∘ swap ]♯ +₁ idC) ∘ (distributeˡ⁻¹ ∘ swap) ∘ (h ⁂ idC) ≈⟨ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc ⟩
(([ B , f ∘ swap ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ∎
♯ˡ-unique : ∀ {X : Obj} {B : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A B) (g : Elgot-Algebra.A FY × X ⇒ Elgot-Algebra.A B)
→ f ≈ g ∘ (η ⁂ idC)
→ ({Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (h # ⁂ idC) ≈ Elgot-Algebra._# B ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)))
→ g ≈ [ B , f ]♯ˡ
♯ˡ-unique {X} {B} f g g-law g-preserving = begin
g ≈⟨ introʳ swap∘swap ⟩
g ∘ swap ∘ swap ≈⟨ sym-assoc ⟩
(g ∘ swap) ∘ swap ≈⟨ (♯-unique (f ∘ swap) (g ∘ swap) helper₁ helper₂) ⟩∘⟨refl ⟩
[ B , (f ∘ swap) ]♯ ∘ swap ∎
where
open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
helper₁ : f ∘ swap ≈ (g ∘ swap) ∘ (idC ⁂ η)
helper₁ = begin
f ∘ swap ≈⟨ g-law ⟩∘⟨refl ⟩
(g ∘ (η ⁂ idC)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩
g ∘ swap ∘ (idC ⁂ η) ≈⟨ sym-assoc ⟩
(g ∘ swap) ∘ (idC ⁂ η) ∎
helper₂ : ∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → (g ∘ swap) ∘ (idC ⁂ h #) ≈ ((g ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #ᵇ
helper₂ {Z} h = begin
(g ∘ swap) ∘ (idC ⁂ h #) ≈⟨ pullʳ swap∘⁂ ⟩
g ∘ (h # ⁂ idC) ∘ swap ≈⟨ pullˡ (g-preserving h) ⟩
((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩
((g ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #ᵇ ∎
where
uni-helper : (idC +₁ swap) ∘ (g ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈ ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ swap
uni-helper = pullˡ +₁∘+₁ ○ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ○ (sym +₁∘+₁) ⟩∘⟨refl ○ pullʳ (pullˡ (sym distributeʳ⁻¹∘swap)) ○ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc
record StableFreeElgotAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where
field
Y : Obj
freeElgot : FreeElgotAlgebra Y
isStableFreeElgotAlgebra : IsStableFreeElgotAlgebra freeElgot
open IsStableFreeElgotAlgebra isStableFreeElgotAlgebra public
```
In a cartesian closed category stability is derivable
```agda
-- TODO
```
```

125
agda/src/Algebra/Elgot/Stable.lagda.md Normal file
View file

@ -0,0 +1,125 @@
<!--
```agda
open import Level
open import Category.Ambient using (Ambient)
open import Categories.FreeObjects.Free
open import Categories.Functor.Core
open import Categories.Functor.Algebra
open import Categories.Functor.Coalgebra
open import Categories.Object.Terminal
open import Categories.Category.Core using (Category)
open import Categories.Category.Distributive using (Distributive)
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
```
-->
```agda
module Algebra.Elgot.Stable {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
open Distributive distributive
open import Categories.Category.Distributive.Properties distributive
open import Algebra.Elgot cocartesian
open import Category.Construction.ElgotAlgebras cocartesian
open import Categories.Morphism.Properties C
open Category C
open Cocartesian cocartesian
open Cartesian cartesian
open BinaryProducts products hiding (η)
open import Algebra.Elgot.Free cocartesian
open Equiv
open HomReasoning
open MR C
open M C
```
Stable free Elgot algebras have an additional universal iteration preserving morphism.
```agda
record IsStableFreeElgotAlgebra {Y : Obj} (freeElgot : FreeElgotAlgebra Y) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
open FreeObject freeElgot using (η) renaming (FX to FY)
open Elgot-Algebra FY using (_#)
field
-- TODO awkward notation...
[_,_]♯ : ∀ {X : Obj} (A : Elgot-Algebra) (f : X × Y ⇒ Elgot-Algebra.A A) → X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A A
♯-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ ∘ (id ⁂ η)
♯-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ ∘ (id ⁂ h #) ≈ Elgot-Algebra._# B (([ B , f ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))
♯-unique : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A B) (g : X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A B)
→ f ≈ g ∘ (id ⁂ η)
→ (∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (id ⁂ h #) ≈ Elgot-Algebra._# B ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)))
→ g ≈ [ B , f ]♯
[_,_]♯ˡ : ∀ {X : Obj} (A : Elgot-Algebra) (f : Y × X ⇒ Elgot-Algebra.A A) → Elgot-Algebra.A FY × X ⇒ Elgot-Algebra.A A
[_,_]♯ˡ {X} A f = [ A , (f ∘ swap) ]♯ ∘ swap
♯ˡ-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ˡ ∘ (η ⁂ id)
♯ˡ-law {X} {A} f = begin
f ≈⟨ introʳ swap∘swap ⟩
f ∘ swap ∘ swap ≈⟨ pullˡ (♯-law (f ∘ swap)) ⟩
([ A , f ∘ swap ]♯ ∘ (id ⁂ η)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩
[ A , (f ∘ swap) ]♯ ∘ swap ∘ (η ⁂ id) ≈⟨ sym-assoc ⟩
([ A , (f ∘ swap) ]♯ ∘ swap) ∘ (η ⁂ id) ∎
♯ˡ-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ˡ ∘ (h # ⁂ id) ≈ Elgot-Algebra._# B (([ B , f ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id))
♯ˡ-preserving {X} {B} f {Z} h = begin
([ B , (f ∘ swap) ]♯ ∘ swap) ∘ ((h #) ⁂ id) ≈⟨ pullʳ swap∘⁂ ⟩
[ B , (f ∘ swap) ]♯ ∘ (id ⁂ h #) ∘ swap ≈⟨ pullˡ (♯-preserving (f ∘ swap) h) ⟩
(([ B , (f ∘ swap) ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩
((([ B , (f ∘ swap) ]♯ ∘ swap) +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∎
where
open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
uni-helper : (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈ (([ B , f ∘ swap ]♯ coproducts.+₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ swap
uni-helper = begin
(id +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ pullˡ +₁∘+₁ ⟩
(id ∘ [ B , f ∘ swap ]♯ ∘ swap +₁ swap ∘ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
([ B , f ∘ swap ]♯ ∘ swap +₁ id ∘ swap) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩
(([ B , f ∘ swap ]♯ +₁ id) ∘ (swap +₁ swap)) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹∘swap)) ⟩
([ B , f ∘ swap ]♯ +₁ id) ∘ (distributeˡ⁻¹ ∘ swap) ∘ (h ⁂ id) ≈⟨ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc ⟩
(([ B , f ∘ swap ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ swap ∎
♯ˡ-unique : ∀ {X : Obj} {B : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A B) (g : Elgot-Algebra.A FY × X ⇒ Elgot-Algebra.A B)
→ f ≈ g ∘ (η ⁂ id)
→ ({Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (h # ⁂ id) ≈ Elgot-Algebra._# B ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)))
→ g ≈ [ B , f ]♯ˡ
♯ˡ-unique {X} {B} f g g-law g-preserving = begin
g ≈⟨ introʳ swap∘swap ⟩
g ∘ swap ∘ swap ≈⟨ sym-assoc ⟩
(g ∘ swap) ∘ swap ≈⟨ (♯-unique (f ∘ swap) (g ∘ swap) helper₁ helper₂) ⟩∘⟨refl ⟩
[ B , (f ∘ swap) ]♯ ∘ swap ∎
where
open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
helper₁ : f ∘ swap ≈ (g ∘ swap) ∘ (id ⁂ η)
helper₁ = begin
f ∘ swap ≈⟨ g-law ⟩∘⟨refl ⟩
(g ∘ (η ⁂ id)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩
g ∘ swap ∘ (id ⁂ η) ≈⟨ sym-assoc ⟩
(g ∘ swap) ∘ (id ⁂ η) ∎
helper₂ : ∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → (g ∘ swap) ∘ (id ⁂ h #) ≈ ((g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ
helper₂ {Z} h = begin
(g ∘ swap) ∘ (id ⁂ h #) ≈⟨ pullʳ swap∘⁂ ⟩
g ∘ (h # ⁂ id) ∘ swap ≈⟨ pullˡ (g-preserving h) ⟩
((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩
((g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ ∎
where
uni-helper : (id +₁ swap) ∘ (g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈ ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ∘ swap
uni-helper = pullˡ +₁∘+₁ ○ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ○ (sym +₁∘+₁) ⟩∘⟨refl ○ pullʳ (pullˡ (sym distributeʳ⁻¹∘swap)) ○ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc
record StableFreeElgotAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where
field
Y : Obj
freeElgot : FreeElgotAlgebra Y
isStableFreeElgotAlgebra : IsStableFreeElgotAlgebra freeElgot
open IsStableFreeElgotAlgebra isStableFreeElgotAlgebra public
```
In a cartesian closed category stability is derivable
```agda
-- TODO
```

478
agda/src/Category/Construction/ElgotAlgebras.lagda.md
View file

@ -3,6 +3,8 @@
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)
@ -11,20 +13,25 @@ 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)
```agda
module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Algebra.Elgot ambient
module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} where
open Category C
open M C
open MR C
open MP C
open HomReasoning
open Equiv
```
@ -32,198 +39,307 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e)
## The Category of Elgot Algebras
```agda
-- 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 +₁ idC) ∘ f)#₂
module Cat (cocartesian : Cocartesian C) where
open Cocartesian cocartesian
open import Algebra.Elgot cocartesian
-- 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 = 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 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ᵍ +₁ 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
-- 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-≈
}
; ∘-resp-≈ = ∘-resp-≈
}
where open Elgot-Algebra-Morphism
where open Elgot-Algebra-Morphism
```
## Finite Products of Elgot Algebras
```agda
-- if the carrier contains a terminal, so does elgot-algebras
Terminal-Elgot-Algebras : Terminal C → Terminal Elgot-Algebras
Terminal-Elgot-Algebras T = record
{ ⊤ = record
{ A = ⊤
; algebra = record
{ _# = λ x → !
; #-Fixpoint = λ {_ f} → !-unique ([ idC , ! ] ∘ 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 T
-- 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) → ⟨ ((π₁ +₁ idC) ∘ h)#ᵃ , ((π₂ +₁ idC) ∘ h)#ᵇ ⟩
; #-Fixpoint = λ {X} {f} → begin
⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩
⟨ [ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ ((π₁ +₁ idC) ∘ f) , [ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ ((π₂ +₁ idC) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁) ⟩
⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩ ≈˘⟨ ⟨⟩∘ ⟩
(⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f) ≈⟨ ∘-resp-≈ˡ (⟨⟩-unique′
(begin
π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩
[ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₁)) ⟩
[ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈˘⟨ ∘[] ⟩
π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∎)
(begin
π₂ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₂ ⟩
[ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₂)) ⟩
[ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈˘⟨ ∘[] ⟩
π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∎)
)⟩
([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f) ∎
; #-Uniformity = λ {X Y f g h} uni → ⟨⟩-unique′
(begin
π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩
(((π₁ +₁ idC) ∘ f)#ᵃ) ≈⟨ #ᵃ-Uniformity
(begin
-- TODO factor these out or adjust +₁ swap... maybe call it +₁-id-comm
(idC +₁ h) ∘ (π₁ +₁ idC) ∘ f ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm)) ⟩
(π₁ ∘ idC +₁ idC ∘ h) ∘ f ≈˘⟨ pullˡ +₁∘+₁ ⟩
(π₁ +₁ idC) ∘ (idC +₁ h) ∘ f ≈⟨ pushʳ uni ⟩
((π₁ +₁ idC) ∘ g) ∘ h ∎)⟩
(((π₁ +₁ idC) ∘ g)#ᵃ ∘ h) ≈˘⟨ pullˡ project₁ ⟩
π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎)
(begin
π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩
((π₂ +₁ idC) ∘ f)#ᵇ ≈⟨ #ᵇ-Uniformity
(begin
(idC +₁ h) ∘ (π₂ +₁ idC) ∘ f ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))⟩
((π₂ ∘ idC +₁ idC ∘ h) ∘ f) ≈˘⟨ pullˡ +₁∘+₁ ⟩
(π₂ +₁ idC) ∘ ((idC +₁ h)) ∘ f ≈⟨ pushʳ uni ⟩
((π₂ +₁ idC) ∘ g) ∘ h ∎)⟩
((π₂ +₁ idC) ∘ g)#ᵇ ∘ h ≈˘⟨ pullˡ project₂ ⟩
π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎)
; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y})
; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg))
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 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) → [ (idC +₁ i₁) ∘ ((π +₁ idC) ∘ f) , i₂ ∘ h ] ≈ (π +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]
+₁-id-swap {X} {Y} {C} {f} {h} π = begin ([ (idC +₁ i₁) ∘ ((π +₁ idC) ∘ f) , i₂ ∘ h ] ) ≈⟨ ([]-congʳ sym-assoc) ⟩
([ ((idC +₁ i₁) ∘ (π +₁ idC)) ∘ f , i₂ ∘ h ] ) ≈⟨ []-cong₂ (∘-resp-≈ˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))) (∘-resp-≈ˡ (sym identityʳ)) ⟩
(([ (π ∘ idC +₁ idC ∘ i₁) ∘ f , (i₂ ∘ idC) ∘ h ])) ≈˘⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂) ⟩
(([ (π +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π +₁ idC) ∘ i₂ ∘ h ])) ≈˘⟨ ∘[] ⟩
((π +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∎
foldingˡ : ∀ {X} {Y} {f} {h} → (((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ) ≈ ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ
foldingˡ {X} {Y} {f} {h} = begin
((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₁ identityˡ)) ⟩
((((π₁ +₁ idC) ∘ f)#ᵃ +₁ h)#ᵃ) ≈⟨ #ᵃ-Folding ⟩
([ (idC +₁ i₁) ∘ ((π₁ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ (+₁-id-swap π₁)⟩
((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ ∎
foldingʳ : ∀ {X} {Y} {f} {h} → ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈ ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ
foldingʳ {X} {Y} {f} {h} = begin
((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₂ identityˡ)) ⟩
((((π₂ +₁ idC) ∘ f)#ᵇ +₁ h)#ᵇ) ≈⟨ #ᵇ-Folding ⟩
[ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ ≈⟨ #ᵇ-resp-≈ (+₁-id-swap π₂) ⟩
((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ ∎
where
open Terminal terminal
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′ +₁ idC) ∘ h) #ᵃ , ((g′ +₁ idC) ∘ h) #ᵇ ⟩ ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₁ identity²))) (#ᵇ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₂ identity²))) ⟩
⟨ ((π₁ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵃ , ((π₂ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵇ ⟩ ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (pullˡ +₁∘+₁)) (#ᵇ-resp-≈ (pullˡ +₁∘+₁)) ⟩
⟨ ((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵃ , ((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ 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 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 terminal
; products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB }
}
-- 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
-- -- if the carriers of the algebra form a exponential, so do the algebras
-- B^A-Helper : ∀ {EA : Elgot-Algebra} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra
-- B^A-Helper {EA} {X} exp = record
-- { A = A^X
-- ; algebra = record
-- { _# = λ {Z} f → λg product (((((eval +₁ idC) ∘ (Categories.Object.Product.repack C product product' +₁ idC)) ∘ dstl) ∘ (f ⁂ idC)) #ᵃ)
-- ; #-Fixpoint = {! !}
-- ; #-Uniformity = {! !}
-- ; #-Folding = {! !}
-- ; #-resp-≈ = {! !}
-- }
-- }
-- where
-- open Exponential exp renaming (B^A to A^X; product to product')
-- open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
-- dstr = λ {X Y Z} → IsIso.inv (isIsoˡ {X} {Y} {Z})
-- dstl = λ {X Y Z} → IsIso.inv (isIsoʳ {X} {Y} {Z})
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ʳ ∎)
cccc : CanonicalCartesianClosed Elgot-Algebras
cccc = record
{ ⊤ = Terminal.⊤ Terminal-Elgot-Algebras
; _×_ = λ X Y → A×B-Helper {X} {Y}
; ! = Terminal.! Terminal-Elgot-Algebras
; π₁ = λ {X} {Y} → Product.π₁ (Product-Elgot-Algebras X Y)
; π₂ = λ {X} {Y} → Product.π₂ (Product-Elgot-Algebras X Y)
; ⟨_,_⟩ = λ {X} {Y} {Z} f g → Product.⟨_,_⟩ (Product-Elgot-Algebras Y Z) f g
; !-unique = Terminal.!-unique Terminal-Elgot-Algebras
; π₁-comp = λ {X} {Y} {f} {Z} {g} → Product.project₁ (Product-Elgot-Algebras Y Z) {h = f} {i = g}
; π₂-comp = λ {X} {Y} {f} {Z} {g} → Product.project₂ (Product-Elgot-Algebras Y Z) {h = f} {i = g}
; ⟨,⟩-unique = {! !}
; _^_ = {! !}
; eval = {! !}
; curry = {! !}
; eval-comp = {! !}
; curry-unique = {! !}
}
Exponential-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra) → Exponential Elgot-Algebras EA EB
Exponential-Elgot-Algebras EA EB = record
{ B^A = B^A-Helper {EA} {Elgot-Algebra.A EB}
; product = Product-Elgot-Algebras (B^A-Helper {EA} {Elgot-Algebra.A EB}) EA
; eval = record { h = {! eval′ {Elgot-Algebra.A EB} {Elgot-Algebra.A EA} !} ; preserves = {! !} }
; λg = {! λ {X} prod → !}
; β = {! !}
; λ-unique = {! !}
}
-- TODO instead show canonical ccc
```

2
agda/src/Monad/Instance/Delay.lagda.md
View file

@ -1,5 +1,7 @@
<!--
```agda
{-# OPTIONS --no-lossy-unification #-}
open import Level
open import Categories.Category
open import Categories.Monad

1
agda/src/Monad/Instance/Delay/Strong.lagda.md
View file

@ -1,5 +1,6 @@
<!--
```agda
{-# OPTIONS --no-lossy-unification #-}
open import Level
open import Data.Product using (_,_; proj₁; proj₂)

2
agda/src/Monad/Instance/K/Commutative.lagda.md
View file

@ -1,5 +1,7 @@
<!--
```agda
{-# OPTIONS --no-lossy-unification #-}
open import Level
open import Category.Ambient using (Ambient)
open import Categories.Monad.Commutative