diff --git a/src/Coinduction/WellFounded/Indexed.agda b/src/Coinduction/WellFounded/Indexed.agda
index 91af2c3..ebe94a2 100644
--- a/src/Coinduction/WellFounded/Indexed.agda
+++ b/src/Coinduction/WellFounded/Indexed.agda
@@ -1,6 +1,6 @@
 module Coinduction.WellFounded.Indexed where
 
-open import Coinduction.WellFounded.Internal.Container public using
+open import Data.Container.Indexed public using
   ( Container
   ; _◃_/_
   ; ⟦_⟧
diff --git a/src/Coinduction/WellFounded/Indexed/Internal.agda b/src/Coinduction/WellFounded/Indexed/Internal.agda
index 0c53057..2187721 100644
--- a/src/Coinduction/WellFounded/Indexed/Internal.agda
+++ b/src/Coinduction/WellFounded/Indexed/Internal.agda
@@ -1,12 +1,12 @@
 module Coinduction.WellFounded.Indexed.Internal where
 
 open import Coinduction.WellFounded.Internal.Relation using
-  (Rel ; Setoid ; on-setoid)
-open import Coinduction.WellFounded.Internal.Container as Cont using
+  (IRel ; IndexedSetoid ; on-setoid)
+open import Data.Container.Indexed as Cont using
   (Container ; _◃_/_ ; ⟦_⟧)
 open import Data.Product
 open import Induction.Nat using (<-well-founded)
-open import Induction.WellFounded using (Well-founded ; Acc ; acc)
+open import Induction.WellFounded using (WellFounded ; Acc ; acc)
 open import Level using (_⊔_ ; Level)
 open import Relation.Binary.PropositionalEquality using
   (_≡_ ; refl ; Extensionality)
@@ -36,12 +36,12 @@ open M public
 -- This is sufficient for the purposes of fixM-unfold, but we may need the
 -- generalisation to an arbitrary setoid later.
 ≅F-setoid : ∀ {lo lc lr} {O : Set lo} (C : Container O O lc lr) (s : Size)
-  → Setoid O _ _
+  → IndexedSetoid O _ _
 ≅F-setoid C s = Cont.setoid C (Het.indexedSetoid (M C s))
 
 
 ≅M-setoid : ∀ {lo lc lr} {O : Set lo} (C : Container O O lc lr) s {t : Size< s}
-  → Setoid O _ _
+  → IndexedSetoid O _ _
 ≅M-setoid C _ {t} = on-setoid (≅F-setoid C t) (λ x → inf x {t})
 
 
@@ -49,8 +49,8 @@ open M public
 -- between objects of different sizes. I haven't needed this yet and it would
 -- complicate matters somewhat, so I'm leaving the definition as is for now.
 _≅F_ : ∀ {lo lc lr} {O : Set lo} {C : Container O O lc lr} {s}
-  → Rel (⟦ C ⟧ (M C s)) _
-_≅F_ {C = C} {s} = Setoid._≈_ (≅F-setoid C s)
+  → IRel (⟦ C ⟧ (M C s)) _
+_≅F_ {C = C} {s} = IndexedSetoid._≈_ (≅F-setoid C s)
 
 
 -- Copied the following from Data.Container.Indexed, where it is sadly
@@ -74,8 +74,8 @@ Eq⇒≅ {xs = c , k} {.c , k′} ext (refl , refl , k≈k′) =
 
 
 _≅M_ : ∀ {lo lc lr} {O : Set lo} {C : Container O O lc lr} {s} {t : Size< s}
-  → Rel (M C s) _
-_≅M_ {C = C} {s} = Setoid._≈_ (≅M-setoid C s)
+  → IRel (M C s) _
+_≅M_ {C = C} {s} = IndexedSetoid._≈_ (≅M-setoid C s)
 
 
 -- s and t are arguments of this definition rather than appearing on the
@@ -128,7 +128,7 @@ module _
 module _
   {lo lc lr} {O : Set lo} {C : Container O O lc lr}
   {lin l<} {In : Set lin}
-  {_<_ : In → In → Set l<} (<-wf : Well-founded _<_)
+  {_<_ : In → In → Set l<} (<-wf : WellFounded _<_)
   {P : In → O}
   (F : ∀ {t}
      → (x : In)
@@ -188,7 +188,7 @@ module _
         → F x f g ≅F F x f' g'
       F-ext x {f} {f'} {g} {g'} eq-f eq-g = go
         where
-          module S = Setoid (≅F-setoid C ∞)
+          module S = IndexedSetoid (≅F-setoid C ∞)
 
           ≡-ext : ∀ {a b} → Extensionality a b
           ≡-ext = ≅-ext-to-≡-ext ≅-ext
diff --git a/src/Coinduction/WellFounded/Internal.agda b/src/Coinduction/WellFounded/Internal.agda
index d834d8e..7017fe9 100644
--- a/src/Coinduction/WellFounded/Internal.agda
+++ b/src/Coinduction/WellFounded/Internal.agda
@@ -2,77 +2,78 @@ module Coinduction.WellFounded.Internal where
 
 open import Data.Container using (Container ; _▷_ ; ⟦_⟧)
 open import Data.Unit
-open import Induction.WellFounded using (Well-founded)
-open import Level using (Level) renaming (zero to lzero ; suc to lsuc)
+open import Induction.WellFounded using (WellFounded)
+open import Level using (Level ; _⊔_) renaming (zero to lzero ; suc to lsuc)
 open import Relation.Binary using (Rel ; Setoid)
-open import Relation.Binary.Indexed using (_at_)
-open import Relation.Binary.PropositionalEquality using
-  (_≡_ ; refl ; Extensionality)
 open import Relation.Binary.HeterogeneousEquality as Het using
   (_≅_ ; ≅-to-≡ ; ≡-ext-to-≅-ext ; ≡-to-≅)
+open import Relation.Binary.Indexed.Heterogeneous.Construct.At using (_atₛ_)
+open import Relation.Binary.PropositionalEquality using
+  (_≡_ ; refl ; Extensionality)
 open import Size using (Size ; Size<_ ; ∞)
 
 open import Coinduction.WellFounded.Indexed as Ix public
   using (inf ; M-Extensionality)
+
 -- TODO While defining the following notions via their generalisations in
 -- Ix is elegant, it also litters goals with garbage if Agda gets
 -- simplification wrong. Thus, we should probably reimplement everything
 -- independent of Ix, then provide conversion lemmas if necessary.
 
 
-container⇒indexedContainer : ∀ {l} → Container l → Ix.Container ⊤ ⊤ _ _
+container⇒indexedContainer : ∀ {σ π} → Container σ π → Ix.Container ⊤ ⊤ _ _
 container⇒indexedContainer (Shape ▷ Position)
     = (λ _ → Shape) Ix.◃ (λ {_} → Position) / (λ _ _ → tt)
 
 
-M : ∀ {l} → Container l → Size → Set _
+M : ∀ {σ π} → Container σ π → Size → Set _
 M C s = Ix.M (container⇒indexedContainer C) s tt
 
 
 -- TODO We should probably switch to the ≡ setoid rather than using the
 -- ≅ setoid (which does nothing for us). Part of the 'reimplement everything'
 -- plan.
-≅F-setoid : ∀ {l} (C : Container l) (s : Size) → Setoid _ _
-≅F-setoid C s = (Ix.≅F-setoid (container⇒indexedContainer C) s) at tt
+≅F-setoid : ∀ {σ π} (C : Container σ π) (s : Size) → Setoid _ _
+≅F-setoid C s = (Ix.≅F-setoid (container⇒indexedContainer C) s) atₛ tt
 
 
-_≅F_ : ∀ {l} {C : Container l} {s} → Rel (⟦ C ⟧ (M C s)) _
+_≅F_ : ∀ {σ π} {C : Container σ π} {s} → Rel (⟦ C ⟧ (M C s)) _
 _≅F_ {C = C} {s} = Setoid._≈_ (≅F-setoid C s)
 
 
-≅F⇒≡ : ∀ {l} {C : Container l} {s} {x y : ⟦ C ⟧ (M C s)}
-  → Extensionality l (lsuc l)
+≅F⇒≡ : ∀ {σ π} {C : Container σ π} {s} {x y : ⟦ C ⟧ (M C s)}
+  → Extensionality π (lsuc σ ⊔ lsuc π)
   → x ≅F y
   → x ≡ y
 ≅F⇒≡ ≡-ext eq = ≅-to-≡ (Ix.≅F⇒≅ (≡-ext-to-≅-ext ≡-ext) eq)
 
 
-≅M-setoid :  ∀ {l} (C : Container l) (s : Size) {t : Size< s} → Setoid _ _
-≅M-setoid C s = (Ix.≅M-setoid (container⇒indexedContainer C) s) at tt
+≅M-setoid :  ∀ {σ π} (C : Container σ π) (s : Size) {t : Size< s} → Setoid _ _
+≅M-setoid C s = (Ix.≅M-setoid (container⇒indexedContainer C) s) atₛ tt
 
 
-_≅M_ : ∀ {l} {C : Container l} {s} {t : Size< s} → Rel (M C s) _
+_≅M_ : ∀ {σ π} {C : Container σ π} {s} {t : Size< s} → Rel (M C s) _
 _≅M_ {C = C} {s} = Setoid._≈_ (≅M-setoid C s)
 
 
-M-Extensionality-from-Ix : ∀ {l s} {t : Size< s}
-  → Ix.M-Extensionality lzero l l s
-  → {C : Container l} {x y : M C s}
+M-Extensionality-from-Ix : ∀ {σ π s} {t : Size< s}
+  → Ix.M-Extensionality lzero σ π s
+  → {C : Container σ π} {x y : M C s}
   → inf x ≡ inf y
   → x ≡ y
 M-Extensionality-from-Ix M-ext eq = ≅-to-≡ (M-ext (≡-to-≅ eq))
 
 
-≅M⇒≡ : ∀ {l} {C : Container l} {s} {t : Size< s} {x y : M C s}
-  → M-Extensionality lzero l l s
-  → Extensionality l (lsuc l)
+≅M⇒≡ : ∀ {σ π} {C : Container σ π} {s} {t : Size< s} {x y : M C s}
+  → M-Extensionality lzero σ π s
+  → Extensionality π (lsuc σ ⊔ lsuc π)
   → x ≅M y
   → x ≡ y
 ≅M⇒≡ M-ext ≡-ext eq = M-Extensionality-from-Ix M-ext (≅F⇒≡ ≡-ext eq)
 
 
 module _
-  {l lin} {C : Container l} {In : Set lin}
+  {σ π lin} {C : Container σ π} {In : Set lin}
   (F : ∀ {t}
      → (x : In)
      → (In → M C t)
@@ -89,8 +90,8 @@ module _
 
 
 module _
-  {l lin l<} {C : Container l} {In : Set lin}
-  {_<_ : Rel In l<} (<-wf : Well-founded _<_)
+  {σ π lin l<} {C : Container σ π} {In : Set lin}
+  {_<_ : Rel In l<} (<-wf : WellFounded _<_)
   (F : ∀ {t}
      → (x : In)
      → (In → M C t)
diff --git a/src/Coinduction/WellFounded/Internal/Container.agda b/src/Coinduction/WellFounded/Internal/Container.agda
deleted file mode 100644
index a0d8101..0000000
--- a/src/Coinduction/WellFounded/Internal/Container.agda
+++ /dev/null
@@ -1,41 +0,0 @@
-module Coinduction.WellFounded.Internal.Container where
-
-open import Data.Product
-open import Relation.Binary.Indexed
-open import Relation.Binary.PropositionalEquality using (refl)
-open import Relation.Binary.HeterogeneousEquality using (refl)
-open import Level using (_⊔_)
-
-open import Data.Container.Indexed public hiding (setoid)
-
-
--- This is a generalisation of Data.Container.Indexed.setoid: The setoid
--- argument is at an arbitrary level `l` rather than `r ⊔ c`. The code
--- remains unchanged.
-setoid : ∀ {i o c r l} {I : Set i} {O : Set o}
-  → Container I O c r
-  → Setoid I l l
-  → Setoid O (l ⊔ r ⊔ c) (l ⊔ r ⊔ c ⊔ o)
-setoid C X = record
-    { Carrier       = ⟦ C ⟧ X.Carrier
-    ; _≈_           = _≈_
-    ; isEquivalence = record
-        { refl  = refl , refl , λ { r .r refl → X.refl }
-        ; sym   = sym
-        ; trans = λ { {_} {i = xs} {ys} {zs} → trans {_} {i = xs} {ys} {zs}  }
-        }
-    }
-  where
-    module X = Setoid X
-
-    _≈_ : Rel (⟦ C ⟧ X.Carrier) _
-    _≈_ = Eq C X.Carrier X.Carrier X._≈_
-
-    sym : Symmetric (⟦ C ⟧ X.Carrier) _≈_
-    sym {_} {._} {_ , _} {._ , _} (refl , refl , k) =
-      refl , refl , λ { r .r refl → X.sym (k r r refl) }
-
-    trans : Transitive (⟦ C ⟧ X.Carrier) _≈_
-    trans {._} {_} {._} {_ , _} {._ , _} {._ , _}
-      (refl , refl , k) (refl , refl , k′) =
-      refl , refl , λ { r .r refl → X.trans (k r r refl) (k′ r r refl) }
diff --git a/src/Coinduction/WellFounded/Internal/Relation.agda b/src/Coinduction/WellFounded/Internal/Relation.agda
index 3fba172..1fe69f3 100644
--- a/src/Coinduction/WellFounded/Internal/Relation.agda
+++ b/src/Coinduction/WellFounded/Internal/Relation.agda
@@ -1,11 +1,11 @@
 module Coinduction.WellFounded.Internal.Relation where
 
-open import Relation.Binary.Indexed public
+open import Relation.Binary.Indexed.Heterogeneous public
 
 
-on-setoid : ∀ {a b l i} {I : Set i} {A : I → Set a} (S : Setoid I b l)
-  → (∀ {i} → A i → Setoid.Carrier S i)
-  → Setoid I a l
+on-setoid : ∀ {a b l i} {I : Set i} {A : I → Set a} (S : IndexedSetoid I b l)
+  → (∀ {i} → A i → IndexedSetoid.Carrier S i)
+  → IndexedSetoid I a l
 on-setoid {I = I} {A} S f = record
     { Carrier = A
     ; _≈_ = λ x y → f x S.≈ f y
@@ -16,4 +16,4 @@ on-setoid {I = I} {A} S f = record
         }
     }
   where
-    module S = Setoid S
+    module S = IndexedSetoid S