diff --git a/ElgotAlgebra.agda b/ElgotAlgebra.agda index a2b2d8a..2b6d42e 100644 --- a/ElgotAlgebra.agda +++ b/ElgotAlgebra.agda @@ -1,228 +1,225 @@ -open import Level renaming (suc to ℓ-suc) -open import Function using (_$_) renaming (id to idf; _∘_ to _∘ᶠ_) -open import Data.Product using (_,_) renaming (_×_ to _∧_) +open import Level -open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory) open import Categories.Functor renaming (id to idF) open import Categories.Functor.Algebra -open import Categories.Object.Product -open import Categories.Object.Coproduct open import Categories.Category -open import Distributive.Core open import Categories.Category.Cartesian open import Categories.Category.BinaryProducts open import Categories.Category.Cocartesian open import Extensive.Bundle -open import Extensive.Core +import Categories.Morphism.Reasoning as MR private - variable - o ℓ e : Level + variable + o ℓ e : Level module _ (D : ExtensiveDistributiveCategory o ℓ e) where - open ExtensiveDistributiveCategory D renaming (U to C; id to idC) - open Cocartesian cocartesian - open Cartesian cartesian - - --* - -- F-guarded Elgot Algebra - --* - module _ {F : Endofunctor C} (FA : F-Algebra F) where - record Guarded-Elgot-Algebra : 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 # ≈ [ idC , α ∘ 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 - → 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₂ - #-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X} - → f ≈ g - → (f #) ≈ (g #) + open ExtensiveDistributiveCategory D renaming (U to C; id to idC) + open Cocartesian cocartesian + open Cartesian cartesian + open MR C - --* - -- (unguarded) Elgot-Algebra - --* - module _ where - record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where - -- Object - field - A : Obj - - -- iteration operator - field - _# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A) + --* + -- F-guarded Elgot Algebra + --* + module _ {F : Endofunctor C} (FA : F-Algebra F) where + record Guarded-Elgot-Algebra : 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 + X } - → f # ≈ [ idC , f # ] ∘ f - #-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y} - → (idC +₁ h) ∘ f ≈ g ∘ h - → f # ≈ g # ∘ h - #-Folding : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} - → ((f #) +₁ h)# ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # - #-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #) + -- _# properties + field + #-Fixpoint : ∀ {X} {f : X ⇒ A + F₀ X } + → f # ≈ [ idC , α ∘ 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 + → 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₂ + #-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X} + → f ≈ g + → (f #) ≈ (g #) - open HomReasoning - open Equiv - -- 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₂ - #-Compositionality {X} {Y} {f} {h} = begin - (((f #) +₁ idC) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h} {g = (f #) +₁ h} {h = h} ( - begin - ((idC +₁ h) ∘ ((f #) +₁ idC) ∘ h) ≈⟨ sym-assoc ⟩ - (((idC +₁ h) ∘ ((f #) +₁ idC)) ∘ h) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ - ((((idC ∘ (f #)) +₁ (h ∘ idC))) ∘ h) ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ - ((((f #) +₁ h)) ∘ h) ∎) - ⟩ - ((f # +₁ h)# ∘ h) ≈⟨ sym inject₂ ⟩ - (([ idC ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂)) ≈⟨ ∘-resp-≈ˡ (sym $ []∘+₁) ⟩ - (([ idC , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂) ≈⟨ (sym $ ∘-resp-≈ˡ (#-Fixpoint {f = (f # +₁ h) })) ⟩ - (f # +₁ h)# ∘ i₂ ≈⟨ ∘-resp-≈ˡ #-Folding ⟩ - ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂) ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ - ([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂ ≈⟨ assoc ⟩ - [ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈⟨ ∘-resp-≈ʳ inject₂ ⟩ - [ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ (i₂ ∘ h) ≈⟨ sym-assoc ⟩ - (([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h) ≈⟨ ∘-resp-≈ˡ inject₂ ⟩ - ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h) ≈⟨ ∘-resp-≈ʳ $ sym (inject₂ {f = i₁} {g = h}) ⟩ - [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ ([ i₁ , h ] ∘ i₂) ≈⟨ sym-assoc ⟩ - (([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂) ≈⟨ sym (∘-resp-≈ˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = [ i₁ , h ]} ( - begin - (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ ∘-resp-≈ʳ ∘[] ⟩ - (idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘-resp-≈ʳ ([]-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₁))) (∘-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 , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩ - [ (idC +₁ i₁) ∘ f , ([ (idC +₁ i₁) ∘ f , i₂ ∘ ([ i₁ , h ] ∘ i₂) ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ - [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ []-congʳ (sym (inject₁)) ⟩ - [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ sym ∘[] ⟩ - [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎)) - )⟩ - ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ ∎ + --* + -- (unguarded) Elgot-Algebra + --* + record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where + -- Object + field + A : Obj - -- every elgot-algebra comes with a divergence constant - !ₑ : ⊥ ⇒ A - !ₑ = i₂ # + -- iteration operator + field + _# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A) - --* - -- Here follows the proof of equivalence for unguarded and Id-guarded Elgot-Algebras - --* + -- _# properties + field + #-Fixpoint : ∀ {X} {f : X ⇒ A + X } + → f # ≈ [ idC , f # ] ∘ f + #-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y} + → (idC +₁ h) ∘ f ≈ g ∘ h + → f # ≈ g # ∘ h + #-Folding : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} + → ((f #) +₁ h)# ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # + #-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #) - private - -- identity functor on 𝒞 - Id : Functor C C - Id = idF {C = C} + open HomReasoning + open Equiv + -- 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₂ + #-Compositionality {X} {Y} {f} {h} = begin + (((f #) +₁ idC) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ 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 ⟩ + (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 ]} + {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₁))) + (∘-resp-≈ˡ ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ inject₂))) ⟩ + [ (idC +₁ i₁) ∘ f , ([ ((idC ∘ idC) +₁ ([ 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 ] ∎)) + ⟩ + ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ ∎ - -- identity algebra - Id-Algebra : Obj → F-Algebra Id - Id-Algebra A = record - { A = A - ; α = idC - } - where open Functor Id + -- every elgot-algebra comes with a divergence constant + !ₑ : ⊥ ⇒ A + !ₑ = i₂ # - -- constructing an Id-Guarded Elgot-Algebra from an unguarded one - Unguarded→Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra (Id-Algebra (Elgot-Algebra.A EA)) - Unguarded→Id-Guarded ea = record - { _# = _# - ; #-Fixpoint = λ {X} {f} → begin - f # ≈⟨ #-Fixpoint ⟩ - [ idC , f # ] ∘ f ≈⟨ sym $ ∘-resp-≈ˡ ([]-congˡ identityˡ) ⟩ - [ idC , idC ∘ f # ] ∘ f ∎ - ; #-Uniformity = #-Uniformity - ; #-Compositionality = #-Compositionality - ; #-resp-≈ = #-resp-≈ - } - where - open Elgot-Algebra ea - open HomReasoning - open Equiv + --* + -- Here follows the proof of equivalence for unguarded and Id-guarded Elgot-Algebras + --* - -- constructing an unguarded Elgot-Algebra from an Id-Guarded one - Id-Guarded→Unguarded : ∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra - Id-Guarded→Unguarded gea = record - { _# = _# - ; #-Fixpoint = λ {X} {f} → begin - f # ≈⟨ #-Fixpoint ⟩ - [ idC , idC ∘ f # ] ∘ f ≈⟨ ∘-resp-≈ˡ ([]-congˡ identityˡ) ⟩ - [ idC , f # ] ∘ f ∎ - ; #-Uniformity = #-Uniformity - ; #-Folding = λ {X} {Y} {f} {h} → begin - ((f #) +₁ h) # ≈⟨ sym +-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 ] #) ∎ - ; #-resp-≈ = #-resp-≈ - } - where - open Guarded-Elgot-Algebra gea - open HomReasoning - open Equiv - left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} - → (f # +₁ h)# ∘ i₁ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ - left {X} {Y} {f} {h} = begin - (f # +₁ h)# ∘ i₁ ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ - (([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₁) ≈⟨ assoc ⟩ - ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ (((f #) +₁ h) ∘ i₁)) ≈⟨ ∘-resp-≈ ([]-congˡ identityˡ) +₁∘i₁ ⟩ - ([ idC , ((f #) +₁ h) # ] ∘ (i₁ ∘ (f #))) ≈⟨ sym-assoc ⟩ - (([ idC , ((f #) +₁ h) # ] ∘ i₁) ∘ (f #)) ≈⟨ ∘-resp-≈ˡ inject₁ ⟩ - idC ∘ (f #) ≈⟨ identityˡ ⟩ - (f #) ≈⟨ #-Uniformity {f = f} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = i₁} (sym inject₁) ⟩ - ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁) ∎ - right : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} - → (f # +₁ h)# ∘ i₂ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ - right {X} {Y} {f} {h} = begin - (f # +₁ h)# ∘ i₂ ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ - (([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₂) ≈⟨ assoc ⟩ - ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h) ∘ i₂) ≈⟨ ∘-resp-≈ ([]-congˡ identityˡ) +₁∘i₂ ⟩ - ([ idC , ((f #) +₁ h) # ] ∘ (i₂ ∘ h)) ≈⟨ sym-assoc ⟩ - ([ idC , ((f #) +₁ h) # ] ∘ i₂) ∘ h ≈⟨ ∘-resp-≈ˡ inject₂ ⟩ - ((f #) +₁ h) # ∘ h ≈⟨ sym (#-Uniformity {f = ((f #) +₁ idC) ∘ h} {g = (f #) +₁ h} {h = h} ( - begin - (idC +₁ h) ∘ ((f #) +₁ idC) ∘ h ≈⟨ sym-assoc ⟩ - (((idC +₁ h) ∘ ((f #) +₁ idC)) ∘ h) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ - (((idC ∘ (f #)) +₁ (h ∘ idC)) ∘ h) ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ - (f # +₁ h) ∘ h ∎) - )⟩ - ((((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 ]} {h = [ i₁ , h ]} ( - begin - (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ ∘-resp-≈ʳ ∘[] ⟩ - (idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘-resp-≈ʳ ([]-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₁))) (∘-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 , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩ - [ (idC +₁ i₁) ∘ f , ([ (idC +₁ i₁) ∘ f , i₂ ∘ ([ i₁ , h ] ∘ i₂) ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ - [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ []-congʳ (sym (inject₁)) ⟩ - [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ sym ∘[] ⟩ - [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎) - )⟩ - (([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂) ≈⟨ assoc ⟩ - ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ ([ i₁ , h ] ∘ i₂)) ≈⟨ (∘-resp-≈ʳ $ inject₂) ⟩ - ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h) ≈⟨ sym $ ∘-resp-≈ˡ inject₂ ⟩ - (([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h) ≈⟨ assoc ⟩ - ([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂ ∘ h) ≈⟨ sym (∘-resp-≈ ([]-congˡ identityˡ) inject₂) ⟩ - ([ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂)) ≈⟨ sym-assoc ⟩ - (([ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂) ≈⟨ ∘-resp-≈ˡ (sym #-Fixpoint) ⟩ - ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂) ∎ + private + -- identity algebra + Id-Algebra : Obj → F-Algebra (idF {C = C}) + Id-Algebra A = record + { A = A + ; α = idC + } + where open Functor (idF {C = C}) - -- unguarded elgot-algebras are just Id-guarded Elgot-Algebras - Unguarded↔Id-Guarded : ((ea : Elgot-Algebra) → Guarded-Elgot-Algebra (Id-Algebra (Elgot-Algebra.A ea))) ∧ (∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra) - Unguarded↔Id-Guarded = Unguarded→Id-Guarded , Id-Guarded→Unguarded \ No newline at end of file + -- constructing an Id-Guarded Elgot-Algebra from an unguarded one + Unguarded→Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra (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 : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra + Id-Guarded→Unguarded gea = 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 ⟩ + [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩ + ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #) ∎ + ; #-resp-≈ = #-resp-≈ + } + where + open Guarded-Elgot-Algebra gea + open HomReasoning + open Equiv + left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} + → (f # +₁ h)# ∘ i₁ ≈ [ (idC +₁ 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₁ ⟩ + (f #) ≈⟨ #-Uniformity {f = f} + {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} + {h = i₁} + (sym inject₁)⟩ + ([ (idC +₁ 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 ] + 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₁))) + (∘-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 + , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ] ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩ + [ (idC +₁ i₁) ∘ f + , [ (idC +₁ 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 ] ∎ + right : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} + → (f # +₁ h)# ∘ i₂ ≈ [ (idC +₁ 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} + {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 ]} + {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₂ ∎