diff --git a/ElgotAlgebra.agda b/ElgotAlgebra.agda
new file mode 100644
index 0000000..7b43509
--- /dev/null
+++ b/ElgotAlgebra.agda
@@ -0,0 +1,297 @@
+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 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
+
+private
+    variable
+        o ℓ e : Level
+
+
+module _ {C𝒞 : CocartesianCategory o ℓ e} where
+    open CocartesianCategory C𝒞 renaming (U to 𝒞; id to idC)
+    
+    --*
+    -- F-guarded Elgot Algebra
+    --*
+    module _ {F : Endofunctor 𝒞} (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 #)
+
+    --*
+    -- (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)
+
+            -- _# 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 #)
+
+            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₂  ∎
+
+            -- divergence constant
+            ⊥ₑ : ⊥ ⇒ A
+            ⊥ₑ = i₂ #
+
+    --*
+    -- let's define the category of elgot-algebras
+    --*
+
+    -- 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)#₂
+    
+    -- 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 #) ≈⟨ sym $ #-resp-≈ identityˡ ⟩ 
+                            ((idC ∘ f) #) ≈⟨ sym (#-resp-≈ (∘-resp-≈ˡ +-η)) ⟩ 
+                            (([ i₁ , i₂ ] ∘ f)#) ≈⟨ sym $ #-resp-≈ (∘-resp-≈ˡ ([]-cong₂ identityʳ identityʳ)) ⟩ 
+                            (([ i₁ ∘ idC , i₂ ∘ idC ] ∘ f)#) ≈⟨ sym $ #-resp-≈ (∘-resp-≈ˡ []∘+₁) ⟩ 
+                            ((([ i₁ , i₂ ] ∘ (idC +₁ idC)) ∘ f)#) ≈⟨ #-resp-≈ assoc ⟩ 
+                            (([ i₁ , i₂ ] ∘ (idC +₁ idC) ∘ f)#) ≈⟨ #-resp-≈ (∘-resp-≈ˡ +-η) ⟩
+                            ((idC ∘ (idC +₁ idC) ∘ f)#) ≈⟨ #-resp-≈ identityˡ ⟩ 
+                            ((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 #ᵃ) ≈⟨ assoc ⟩
+                            (hᶠ ∘ hᵍ ∘ (f #ᵃ)) ≈⟨ ∘-resp-≈ʳ preservesᵍ ⟩ 
+                            (hᶠ ∘ (((hᵍ +₁ idC) ∘ f) #ᵇ)) ≈⟨ preservesᶠ ⟩ 
+                            (((hᶠ +₁ idC) ∘ (hᵍ +₁ idC) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ sym-assoc ⟩ 
+                            ((((hᶠ +₁ idC) ∘ (hᵍ +₁ idC)) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ +₁∘+₁) ⟩ 
+                            ((((hᶠ ∘ hᵍ) +₁ (idC ∘ idC)) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ (+₁-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}
+        ; ∘-resp-≈  = ∘-resp-≈
+        }
+        where 
+            open Elgot-Algebra-Morphism
+            open HomReasoning
+            open Equiv
+
+    --*
+    -- products and exponentials of elgot-algebras
+    --*
+
+    -- product elgot-algebras
+    Product-Elgot-Algebra : ∀ {EA EB : Elgot-Algebra} → Product 𝒞 (Elgot-Algebra.A EA) (Elgot-Algebra.A EB) → Elgot-Algebra
+    Product-Elgot-Algebra {EA} {EB} p = record 
+        { A = A×B
+        ; _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ idC) ∘ h)#ᵃ , ((π₂ +₁ idC) ∘ h)#ᵇ ⟩ 
+        ; #-Fixpoint = λ {X} {f} → begin
+            ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ {!   !} ⟩ -- maybe use fixpoint on each side of pair..
+            ([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f) ∎  -- TODO
+        ; #-Uniformity = _ -- TODO
+        ; #-Folding = _ -- TODO 
+        ; #-resp-≈ = _ -- TODO
+        }
+        where 
+            open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ)
+            open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ)
+            open Product 𝒞 p
+            open HomReasoning
+
+    --*
+    -- Here follows the proof of equivalence for unguarded and Id-guarded Elgot-Algebras
+    --*
+
+    private
+        -- identity functor on 𝒞
+        Id : Functor 𝒞 𝒞
+        Id = idF {C = 𝒞}
+
+        -- identity algebra
+        Id-Algebra : Obj → F-Algebra Id
+        Id-Algebra A = record
+            { A = A
+            ; α = idC
+            }
+            where open Functor Id
+
+    -- 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
+
+    -- 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₂) ∎
+
+    -- 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
diff --git a/bsc.agda-lib b/bsc.agda-lib
new file mode 100644
index 0000000..3f08382
--- /dev/null
+++ b/bsc.agda-lib
@@ -0,0 +1,3 @@
+name: bsc
+include: .
+depend: standard-library, agda-categories
\ No newline at end of file