module Algebra.Elgot {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where open Category C open Cocartesian cocartesian open MR C
Guarded Elgot algebras are algebras on an endofunctor together with an iteration operator that satisfies some axioms.
record Guarded-Elgot-Algebra-on {F : Endofunctor C} (FA : F-Algebra F) : Set (o ⊔ ℓ ⊔ e) where open Functor F public open F-Algebra FA public -- iteration operator field _# : ∀ {X} → (X ⇒ A + F₀ X) → (X ⇒ A) -- _# properties field #-Fixpoint : ∀ {X} {f : X ⇒ A + F₀ X } → f # ≈ [ id , α ∘ F₁ (f #) ] ∘ f #-Uniformity : ∀ {X Y} {f : X ⇒ A + F₀ X} {g : Y ⇒ A + F₀ Y} {h : X ⇒ Y} → (id +₁ F₁ h) ∘ f ≈ g ∘ h → f # ≈ g # ∘ h #-Compositionality : ∀ {X Y} {f : X ⇒ A + F₀ X} {h : Y ⇒ X + F₀ Y} → (((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 #) record Guarded-Elgot-Algebra (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where field algebra : F-Algebra F guarded-elgot-algebra-on : Guarded-Elgot-Algebra-on algebra open Guarded-Elgot-Algebra-on guarded-elgot-algebra-on public
Unguarded elgot algebras are Id
-guarded elgot algebras
where the functor algebra is also trivial. Here we give a different
(easier) Characterization and show that it is equal.
record Elgot-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where -- iteration operator field _# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A) -- _# properties field #-Fixpoint : ∀ {X} {f : X ⇒ A + X } → f # ≈ [ id , f # ] ∘ f #-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y} → (id +₁ h) ∘ f ≈ g ∘ h → f # ≈ g # ∘ h #-Folding : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} → ((f #) +₁ h)# ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # #-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #) open HomReasoning open Equiv -- Compositionality is derivable #-Compositionality : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} → (((f #) +₁ id) ∘ h)# ≈ ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ #-Compositionality {X} {Y} {f} {h} = begin (((f #) +₁ id) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ id) ∘ h} {g = (f #) +₁ h} {h = h} (trans (pullˡ +₁∘+₁) (+₁-cong₂ identityˡ identityʳ ⟩∘⟨refl))⟩ ((f # +₁ h)# ∘ h) ≈˘⟨ inject₂ ⟩ (([ id ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂)) ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩ (([ id , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂) ≈˘⟨ #-Fixpoint {f = (f # +₁ h) } ⟩∘⟨refl ⟩ (f # +₁ h)# ∘ i₂ ≈⟨ #-Folding ⟩∘⟨refl ⟩ ([ (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 (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₂))) ⟩ [ (id +₁ i₁) ∘ f , ([ ((id ∘ id) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) (pullʳ inject₂))) ⟩ [ (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 ] ∎)) ⟩ ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ 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 ] +₁ 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₁ +₁ 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 ⟩ [ id , (h +₁ i₁) # ] ∘ (h +₁ i₁) ≈⟨ []∘+₁ ○ []-cong₂ identityˡ refl ⟩ [ h , (h +₁ i₁) # ∘ i₁ ] ≈⟨ []-cong₂ refl (#-Fixpoint ⟩∘⟨refl) ⟩ [ 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₁ +₁ id) ≈ (id +₁ (i₁ +₁ id)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] by-uni = begin ([ 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) ⟩ [ (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)) → ((id +₁ [ id , id ]) ∘ f)# ≈ ([ i₁ , ((id +₁ [ id , id ]) ∘ f) # +₁ id ] ∘ f) # #-Diamond {X} f = begin g # ≈⟨ introʳ inject₂ ⟩ 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₂ ] ∘ (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 = (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 (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 (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 ∘ [ id , id ] ∎ by-fix : [ i₁ , (id +₁ i₂) ∘ g ] # ≈ [ id , g # ] by-fix = sym (begin [ 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 !ₑ = i₂ # record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where field A : Obj algebra : Elgot-Algebra-on A open Elgot-Algebra-on algebra public
Now we show that unguarded and Id-guarded Elgot algebras are the same.
First we show how to get an Id-guarded algebra from a unguarded one and vice versa:
private -- identity algebra Id-Algebra : Obj → F-Algebra (idF {C = C}) Id-Algebra A = record { A = A ; α = id } where open Functor (idF {C = C}) -- constructing an Id-Guarded Elgot-Algebra from an unguarded one Unguarded⇒Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra-on (Id-Algebra (Elgot-Algebra.A EA)) Unguarded⇒Id-Guarded ea = record { _# = _# ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (sym (∘-resp-≈ˡ ([]-congˡ identityˡ))) ; #-Uniformity = #-Uniformity ; #-Compositionality = #-Compositionality ; #-resp-≈ = #-resp-≈ } where open Elgot-Algebra ea open HomReasoning open Equiv -- constructing an unguarded Elgot-Algebra from an Id-Guarded one Id-Guarded⇒Unguarded : ∀ {A} → Guarded-Elgot-Algebra-on (Id-Algebra A) → Elgot-Algebra Id-Guarded⇒Unguarded gea = record { A = A ; algebra = record { _# = _# ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (∘-resp-≈ˡ ([]-congˡ identityˡ)) ; #-Uniformity = #-Uniformity ; #-Folding = λ {X} {Y} {f} {h} → begin ((f #) +₁ h) # ≈˘⟨ +-g-η ⟩ [ (f # +₁ h)# ∘ i₁ , (f # +₁ h)# ∘ i₂ ] ≈⟨ []-cong₂ left right ⟩ [ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] #) ∎ ; #-resp-≈ = #-resp-≈ } } where open Guarded-Elgot-Algebra-on gea open HomReasoning open Equiv left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} → (f # +₁ h)# ∘ i₁ ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ left {X} {Y} {f} {h} = begin (f # +₁ h)# ∘ i₁ ≈⟨ #-Fixpoint ⟩∘⟨refl ⟩ ([ id , id ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₁ ≈⟨ pullʳ +₁∘i₁ ⟩ [ id , id ∘ (((f #) +₁ h) #) ] ∘ (i₁ ∘ f #) ≈⟨ cancelˡ inject₁ ⟩ (f #) ≈⟨ #-Uniformity {f = f} {g = [ (id +₁ i₁) ∘ f , i₂ ∘ h ]} {h = i₁} (sym inject₁)⟩ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁) ∎ byUni : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} → (id +₁ [ i₁ , h ]) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] byUni {X} {Y} {f} {h} = begin (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)) ⟩ [ (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)) ⟩ [ (id +₁ i₁) ∘ f , [ (id +₁ i₁) ∘ f , i₂ ∘ ([ i₁ , h ] ∘ i₂) ] ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ [ (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₂ ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ right {X} {Y} {f} {h} = begin (f # +₁ h)# ∘ i₂ ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ ([ 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 #) +₁ 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)⟩ ([ (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)
Unguarded⇒Id-Guarded⇒Unguarded : ∀ (EA : Elgot-Algebra) {X : Obj} (f : X ⇒ Elgot-Algebra.A EA + X) → Elgot-Algebra._# EA f ≈ Elgot-Algebra._# (Id-Guarded⇒Unguarded (Unguarded⇒Id-Guarded EA)) f Unguarded⇒Id-Guarded⇒Unguarded EA {X} f = Equiv.refl Id-Guarded⇒Unguarded⇒Id-Guarded : ∀ (A : Obj) (EA : Guarded-Elgot-Algebra-on (Id-Algebra A)) {X : Obj} (f : X ⇒ A + X) → Guarded-Elgot-Algebra-on._# EA f ≈ Guarded-Elgot-Algebra-on._# (Unguarded⇒Id-Guarded (Id-Guarded⇒Unguarded EA)) f Id-Guarded⇒Unguarded⇒Id-Guarded A EA {X} f = Equiv.refl