diff --git a/agda/src/Algebra/Elgot/Properties.lagda.md b/agda/src/Algebra/Elgot/Properties.lagda.md
index 7dda378..1807b89 100644
--- a/agda/src/Algebra/Elgot/Properties.lagda.md
+++ b/agda/src/Algebra/Elgot/Properties.lagda.md
@@ -1,4 +1,5 @@
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.FreeObjects.Free
 open import Categories.Functor.Core
diff --git a/agda/src/Category/Construction/PreElgotMonads.lagda.md b/agda/src/Category/Construction/PreElgotMonads.lagda.md
index 18cf2ec..c1ec186 100644
--- a/agda/src/Category/Construction/PreElgotMonads.lagda.md
+++ b/agda/src/Category/Construction/PreElgotMonads.lagda.md
@@ -18,7 +18,7 @@ open import Categories.Category.Core
 module Category.Construction.PreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
 open Ambient ambient
 open import Monad.PreElgot ambient
-open import Algebra.Elgot ambient
+open import Algebra.Elgot cocartesian
 open HomReasoning
 open Equiv
 open M C
diff --git a/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md b/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md
index 0ce0a39..bee3ae6 100644
--- a/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md
+++ b/agda/src/Category/Construction/StrongPreElgotMonads.lagda.md
@@ -20,7 +20,7 @@ open import Data.Product using (_,_)
 module Category.Construction.StrongPreElgotMonads {o ℓ e} (ambient : Ambient o ℓ e) where
 open Ambient ambient
 open import Monad.PreElgot ambient
-open import Algebra.Elgot ambient
+open import Algebra.Elgot cocartesian
 open HomReasoning
 open Equiv
 open M C
diff --git a/agda/src/FreeObject.lagda.md b/agda/src/FreeObject.lagda.md
deleted file mode 100644
index 78cc414..0000000
--- a/agda/src/FreeObject.lagda.md
+++ /dev/null
@@ -1,56 +0,0 @@
-<!--
-```agda
-open import Level
-open import Categories.Category
-open import Categories.Functor
-```
--->
-
-```agda
-module FreeObject where
-private
-  variable
-    o ℓ e o' ℓ' e' : Level
-```
-
-# Free objects
-The notion of free object has been formalized in agda-categories:
-
-```agda
-open import Categories.FreeObjects.Free
-``` 
-
-but we need a predicate expressing that an object 'is free':
-
-```agda 
-record IsFreeObject {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) : Set (suc (e ⊔ e' ⊔ o ⊔ ℓ ⊔ o' ⊔ ℓ')) where
-
-  private
-    module C = Category C using (Obj; id; identityʳ; identityˡ; _⇒_; _∘_; equiv; module Equiv)
-    module D = Category D using (Obj; _⇒_; _∘_; equiv)
-    module U = Functor U using (₀; ₁)
-
-  field
-     η : C [ X , U.₀ FX ]
-     _* : ∀ {A : D.Obj} → C [ X , U.₀ A ] → D [ FX , A ]
-     *-lift : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) → C [ (U.₁ (f *) C.∘ η) ≈ f ]
-     *-uniq : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) (g : D [ FX , A ]) → C [ (U.₁ g) C.∘ η ≈ f ] → D [ g ≈ f * ]
-```
-
-and some way to convert between these notions:
-
-```agda
-IsFreeObject⇒FreeObject : ∀ {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) → IsFreeObject U X FX → FreeObject U X
-IsFreeObject⇒FreeObject U X FX isFO = record 
-  { FX = FX 
-  ; η = η 
-  ; _* = _* 
-  ; *-lift = *-lift 
-  ; *-uniq = *-uniq 
-  }
-  where open IsFreeObject isFO
-
-  -- TODO FreeObject⇒IsFreeObject
-
-```
-
diff --git a/agda/src/Monad/Instance/K.lagda.md b/agda/src/Monad/Instance/K.lagda.md
index a107a82..5689fd9 100644
--- a/agda/src/Monad/Instance/K.lagda.md
+++ b/agda/src/Monad/Instance/K.lagda.md
@@ -17,9 +17,11 @@ open import Categories.Monad.Construction.Kleisli
 ```agda
 module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
-  open import Category.Construction.ElgotAlgebras ambient using (Elgot-Algebras)
-  open import Algebra.Elgot ambient using (Elgot-Algebra)
-  open import Algebra.Elgot.Free ambient using (FreeElgotAlgebra; elgotForgetfulF; IsStableFreeElgotAlgebra)
+  open import Category.Construction.ElgotAlgebras {C = C}
+  open Cat cocartesian using (Elgot-Algebras)
+  open import Algebra.Elgot cocartesian using (Elgot-Algebra)
+  open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
+  open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
 
   open Equiv
   open MR C
diff --git a/agda/src/Monad/Instance/K/Commutative.lagda.md b/agda/src/Monad/Instance/K/Commutative.lagda.md
index 41a9058..08ec99f 100644
--- a/agda/src/Monad/Instance/K/Commutative.lagda.md
+++ b/agda/src/Monad/Instance/K/Commutative.lagda.md
@@ -20,9 +20,11 @@ open MIK ambient
 open MonadK MK
 open import Monad.Instance.K.Strong ambient MK
 open import Monad.Instance.K.EquationalLifting ambient MK
-open import Category.Construction.ElgotAlgebras ambient
-open import Algebra.Elgot ambient
-open import Algebra.Elgot.Free ambient using (FreeElgotAlgebra; elgotForgetfulF; IsStableFreeElgotAlgebra)
+open import Category.Construction.ElgotAlgebras {C = C}
+open Cat cocartesian
+open import Algebra.Elgot cocartesian
+open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
+open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
 
 open Equiv
 open HomReasoning
diff --git a/agda/src/Monad/Instance/K/EquationalLifting.lagda.md b/agda/src/Monad/Instance/K/EquationalLifting.lagda.md
index 178a351..3c6166c 100644
--- a/agda/src/Monad/Instance/K/EquationalLifting.lagda.md
+++ b/agda/src/Monad/Instance/K/EquationalLifting.lagda.md
@@ -18,9 +18,10 @@ open Ambient ambient
 open MIK ambient
 open MonadK MK
 open import Monad.Instance.K.Strong ambient MK
-open import Category.Construction.ElgotAlgebras ambient
-open import Algebra.Elgot ambient
-open import Algebra.Elgot.Free ambient using (IsStableFreeElgotAlgebra)
+open import Category.Construction.ElgotAlgebras {C = C}
+open Cat cocartesian
+open import Algebra.Elgot cocartesian
+open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
 
 open HomReasoning
 open Equiv
diff --git a/agda/src/Monad/Instance/K/PreElgot.lagda.md b/agda/src/Monad/Instance/K/PreElgot.lagda.md
index dd9106e..a509f7b 100644
--- a/agda/src/Monad/Instance/K/PreElgot.lagda.md
+++ b/agda/src/Monad/Instance/K/PreElgot.lagda.md
@@ -18,13 +18,14 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK
 open Ambient ambient
 open MIK ambient
 open MonadK MK
-open import Algebra.Elgot ambient
+open import Algebra.Elgot cocartesian
 open import Monad.PreElgot ambient
 open import Monad.Instance.K ambient
 open import Monad.Instance.K.Commutative ambient MK
 open import Monad.Instance.K.Strong ambient MK
 open import Category.Construction.PreElgotMonads ambient
-open import Category.Construction.ElgotAlgebras ambient
+open import Category.Construction.ElgotAlgebras {C = C}
+open Cat cocartesian
 
 open Equiv
 open HomReasoning
diff --git a/agda/src/Monad/Instance/K/Strong.lagda.md b/agda/src/Monad/Instance/K/Strong.lagda.md
index 847c56b..1406a40 100644
--- a/agda/src/Monad/Instance/K/Strong.lagda.md
+++ b/agda/src/Monad/Instance/K/Strong.lagda.md
@@ -22,9 +22,11 @@ import Monad.Instance.K as MIK
 ```agda
 module Monad.Instance.K.Strong {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
   open Ambient ambient
-  open import Category.Construction.ElgotAlgebras ambient
-  open import Algebra.Elgot ambient
-  open import Algebra.Elgot.Free ambient using (FreeElgotAlgebra; elgotForgetfulF; IsStableFreeElgotAlgebra)
+  open import Category.Construction.ElgotAlgebras {C = C}
+  open Cat cocartesian
+  open import Algebra.Elgot cocartesian
+  open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
+  open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra)
 
   open MIK ambient
   open MonadK MK
diff --git a/agda/src/Monad/Instance/K/StrongPreElgot.lagda.md b/agda/src/Monad/Instance/K/StrongPreElgot.lagda.md
index 3554584..0730dc6 100644
--- a/agda/src/Monad/Instance/K/StrongPreElgot.lagda.md
+++ b/agda/src/Monad/Instance/K/StrongPreElgot.lagda.md
@@ -21,15 +21,17 @@ module Monad.Instance.K.StrongPreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK
 open Ambient ambient
 open MIK ambient
 open MonadK MK
-open import Algebra.Elgot ambient
-open import Algebra.Elgot.Free ambient
+open import Algebra.Elgot cocartesian
+open import Algebra.Elgot.Free cocartesian
+open import Algebra.Elgot.Stable distributive
 open import Monad.PreElgot ambient
 open import Monad.Instance.K ambient
 open import Monad.Instance.K.Commutative ambient MK
 open import Monad.Instance.K.Strong ambient MK
 open import Monad.Instance.K.PreElgot ambient MK
 open import Category.Construction.StrongPreElgotMonads ambient
-open import Category.Construction.ElgotAlgebras ambient
+open import Category.Construction.ElgotAlgebras {C = C}
+open Cat cocartesian
 
 open Equiv
 open HomReasoning
diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index fa0a904..fa9d9ad 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -12,13 +12,14 @@ open import Function.Construct.Setoid renaming (setoid to _⇨_; _∙_ to _∘_)
 open import Function using (_∘′_; id) renaming (_∘_ to _∘f_)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_) renaming (sym to ≣-sym; refl to ≣-refl; trans to ≣-trans)
-open import FreeObject
 open import Categories.FreeObjects.Free
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Product.Function.NonDependent.Setoid using (proj₁ₛ)
 open import Categories.Category.Instance.Properties.Setoids.Choice using ()
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Data.Product
+open import Category.Ambient using (Ambient)
+open import Categories.Category.Instance.Setoids
 ``` 
 -->
 
@@ -27,12 +28,14 @@ open import Data.Product
 ```agda
 module Monad.Instance.Setoids.K {ℓ : Level} where
   open _⟶_ using (cong)
-  open import Monad.Instance.Setoids.Delay {ℓ} {ℓ}
   open import Category.Ambient.Setoids
+  open Ambient (setoidAmbient {ℓ}) using (cocartesian; distributive)
+  open import Monad.Instance.Setoids.Delay {ℓ} {ℓ}
   open import Monad.Instance.K (setoidAmbient {ℓ})
-  open import Algebra.Elgot (setoidAmbient {ℓ})
-  open import Algebra.Elgot.Free (setoidAmbient {ℓ})
-  open import Category.Construction.ElgotAlgebras (setoidAmbient {ℓ})
+  open import Algebra.Elgot cocartesian
+  open import Algebra.Elgot.Free cocartesian
+  open import Category.Construction.ElgotAlgebras {C = Setoids ℓ ℓ}
+  open Cat cocartesian
   open import Monad.PreElgot (setoidAmbient {ℓ})
   open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_])
   open DelayMonad
diff --git a/agda/src/Monad/PreElgot.lagda.md b/agda/src/Monad/PreElgot.lagda.md
index 03792ac..75a377f 100644
--- a/agda/src/Monad/PreElgot.lagda.md
+++ b/agda/src/Monad/PreElgot.lagda.md
@@ -17,7 +17,7 @@ module Monad.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) where
   open HomReasoning
   open MR C
   open Equiv
-  open import Algebra.Elgot ambient
+  open import Algebra.Elgot cocartesian
 ```
 
 # (strong) pre-Elgot monads