Guarded and unguarded Elgot algebras

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

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

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