diff --git a/src/Mugen/Cat/HierarchyTheory.agda b/src/Mugen/Cat/HierarchyTheory.agda
index cc1680c..251ad27 100644
--- a/src/Mugen/Cat/HierarchyTheory.agda
+++ b/src/Mugen/Cat/HierarchyTheory.agda
@@ -22,127 +22,125 @@ Hierarchy-theory o r = Monad (Strict-orders o r)
 --------------------------------------------------------------------------------
 -- Morphisms between hierarchy theories
 
-private
-  M∘-functor : ∀ {o r} →
-    Functor
-    (Cat[ Strict-orders o r , Strict-orders o r ] ×ᶜ Cat[ Strict-orders o r , Strict-orders o r ])
-    Cat[ Strict-orders o r , Strict-orders o r ]
-  M∘-functor = F∘-functor
-
-  module M∘ {o r : Level} = Functor (M∘-functor {o} {r})
-
-record Hierarchy-map {o r} (M N : Hierarchy-theory o r) : Type (lsuc o ⊔ lsuc r) where
-  no-eta-equality
-  module M = Monad M
-  module N = Monad N
-  field
-    nat : M.M => N.M
-  open _=>_ nat public
-  field
-    pres-unit : nat ∘nt M.unit ≡ N.unit
-    pres-mult : nat ∘nt M.mult ≡ N.mult ∘nt (nat ◆ nat)
-
-module _ {o r} {M N : Hierarchy-theory o r} (ν1 ν2 : Hierarchy-map M N) where
+module _ {o r} where
   private
-    module M = Monad M
-    module N = Monad N
+    SOrd : Precategory (lsuc (o ⊔ r)) (o ⊔ r)
+    SOrd = Strict-orders o r
 
-  Hierarchy-map-path
-    : ν1 .Hierarchy-map.nat ≡ ν2 .Hierarchy-map.nat
-    → ν1 ≡ ν2
-  Hierarchy-map-path p i .Hierarchy-map.nat = p i
-  Hierarchy-map-path p i .Hierarchy-map.pres-unit =
-    is-prop→pathp
-      (λ i → Nat-is-set (p i ∘nt M.unit) N.unit)
-      (ν1 .Hierarchy-map.pres-unit)
-      (ν2 .Hierarchy-map.pres-unit)
-      i
-  Hierarchy-map-path p i .Hierarchy-map.pres-mult =
-    is-prop→pathp
-      (λ i → Nat-is-set (p i ∘nt M.mult) (N.mult ∘nt (p i ◆ p i)))
-      (ν1 .Hierarchy-map.pres-mult)
-      (ν2 .Hierarchy-map.pres-mult)
-      i
-
-module _ {o r} {M N : Hierarchy-theory o r} where
-  private
-    module M = Monad M
-    module N = Monad N
+    Endo : Precategory (lsuc (o ⊔ r)) (lsuc (o ⊔ r))
+    Endo = Cat[ SOrd , SOrd ]
+    module Endo = Cat Endo
 
-  abstract instance
-    H-Level-Hierarchy-map : ∀ {n} → H-Level (Hierarchy-map M N) (2 + n)
-    H-Level-Hierarchy-map = basic-instance 2 $ Iso→is-hlevel 2 eqv (hlevel 2)
-      where unquoteDecl eqv = declare-record-iso eqv (quote Hierarchy-map)
-
-  instance
-    Extensional-Hierarchy-map
-      : ∀ {ℓ} ⦃ sa : Extensional (M.M => N.M) ℓ ⦄
-      → Extensional (Hierarchy-map M N) ℓ
-    Extensional-Hierarchy-map ⦃ sa ⦄ =
-      injection→extensional!
-        {f = Hierarchy-map.nat}
-        (Hierarchy-map-path _ _) sa
-
-    Funlike-Hierarchy-map
-      : Funlike (Hierarchy-map M N) (Poset o r) (λ Δ → Strictly-monotone (M.M # Δ) (N.M # Δ))
-    Funlike-Hierarchy-map ._#_ = Hierarchy-map.η
-
-Hierarchy-map-id : ∀ {o r} {M : Hierarchy-theory o r} → Hierarchy-map M M
-Hierarchy-map-id {M = M} = hm where
-  module M = Monad M
-
-  abstract
-    pres-unit : idnt ∘nt M.unit ≡ M.unit
-    pres-unit = ext λ Δ α → refl
-
-    pres-mult : idnt ∘nt M.mult ≡ M.mult ∘nt (idnt ◆ idnt)
-    pres-mult = ext λ Δ α →
-      M.μ Δ # α
-        ≡˘⟨ ap# (M.μ Δ) $ (M∘.F-id #ₚ Δ) #ₚ α ⟩
-      M.μ Δ # (((idnt ◆ idnt) # Δ) # α)
-        ∎
+    Endo-∘-functor : Functor (Endo ×ᶜ Endo) Endo
+    Endo-∘-functor = F∘-functor
+    module Endo-∘ = Functor Endo-∘-functor
 
-  hm : Hierarchy-map M M
-  hm .Hierarchy-map.nat = idnt
-  hm .Hierarchy-map.pres-unit = pres-unit
-  hm .Hierarchy-map.pres-mult = pres-mult
-
-{-
-Hierarchy-map-∘ : ∀ {o r} {M N O : Hierarchy-theory o r}
-  → Hierarchy-map N O
-  → Hierarchy-map M N
-  → Hierarchy-map M O
-Hierarchy-map-∘ {M = M} {N} {O} ν ξ = hm where
-  module M = Monad M
-  module N = Monad N
-  module O = Monad O
-  module ν = Hierarchy-map ν
-  module ξ = Hierarchy-map ξ
-
-  nat : M.M => O.M
-  nat = ν.nat ∘nt ξ.nat
-
-  pres-unit : nat ∘nt M.unit ≡ O.unit
-  pres-unit = ext λ Δ α →
-    ν.η Δ # (ξ.η Δ # (M.η Δ # α))
-      ≡⟨ ap# (ν.η Δ) $ (ξ.pres-unit #ₚ Δ) #ₚ α ⟩
-    ν.η Δ # (N.η Δ # α)
-      ≡⟨ (ν.pres-unit #ₚ Δ) #ₚ α ⟩
-    O.η Δ # α
-      ∎
+    -- The following code assumes this judgmental equality
+    _ : ∀ {M M' N N' : Functor SOrd SOrd} {α : M => M'} {β : N => N'} → Endo-∘.₁ (α , β) ≡ α ◆ β
+    _ = refl
 
-  pres-mult : nat ∘nt M.mult ≡ O.mult ∘nt (nat ◆ nat)
-  pres-mult = ext λ Δ α →
-    ν.η Δ # (ξ.η Δ # (M.μ Δ # α))
-      ≡⟨ ? ⟩
-    O.μ Δ # ((nat ◆ nat) # Δ # α)
+  record Hierarchy-hom (M N : Hierarchy-theory o r) : Type (lsuc o ⊔ lsuc r) where
+    no-eta-equality
+    module M = Monad M
+    module N = Monad N
+    field
+      nat : M.M => N.M
+    open _=>_ nat public
+    field
+      pres-unit : nat ∘nt M.unit ≡ N.unit
+      pres-mult : nat ∘nt M.mult ≡ N.mult ∘nt (nat ◆ nat)
+
+  module _ {M N : Hierarchy-theory o r} where
+    private
+      module M = Monad M
+      module N = Monad N
+
+    Hierarchy-hom-path : (ν ξ : Hierarchy-hom M N)
+      → ν .Hierarchy-hom.nat ≡ ξ .Hierarchy-hom.nat
+      → ν ≡ ξ
+    Hierarchy-hom-path ν ξ p i .Hierarchy-hom.nat = p i
+    Hierarchy-hom-path ν ξ p i .Hierarchy-hom.pres-unit =
+      is-prop→pathp
+        (λ i → Nat-is-set (p i ∘nt M.unit) N.unit)
+        (ν .Hierarchy-hom.pres-unit)
+        (ξ .Hierarchy-hom.pres-unit)
+        i
+    Hierarchy-hom-path ν ξ p i .Hierarchy-hom.pres-mult =
+      is-prop→pathp
+        (λ i → Nat-is-set (p i ∘nt M.mult) (N.mult ∘nt (p i ◆ p i)))
+        (ν .Hierarchy-hom.pres-mult)
+        (ξ .Hierarchy-hom.pres-mult)
+        i
+
+    abstract instance
+      H-Level-Hierarchy-hom : ∀ {n} → H-Level (Hierarchy-hom M N) (2 + n)
+      H-Level-Hierarchy-hom = basic-instance 2 $ Iso→is-hlevel 2 eqv (hlevel 2)
+        where unquoteDecl eqv = declare-record-iso eqv (quote Hierarchy-hom)
+
+    instance
+      Extensional-Hierarchy-hom
+        : ∀ {ℓ} ⦃ sa : Extensional (M.M => N.M) ℓ ⦄
+        → Extensional (Hierarchy-hom M N) ℓ
+      Extensional-Hierarchy-hom ⦃ sa ⦄ =
+        injection→extensional!
+          {f = Hierarchy-hom.nat}
+          (Hierarchy-hom-path _ _) sa
+
+      Funlike-Hierarchy-hom
+        : Funlike (Hierarchy-hom M N) (Poset o r) (λ Δ → Strictly-monotone (M.M # Δ) (N.M # Δ))
+      Funlike-Hierarchy-hom ._#_ = Hierarchy-hom.η
+
+  hierarchy-hom-id : ∀ {M : Hierarchy-theory o r} → Hierarchy-hom M M
+  hierarchy-hom-id {M = _} .Hierarchy-hom.nat       = idnt
+  hierarchy-hom-id {M = _} .Hierarchy-hom.pres-unit = Endo.idl _
+  hierarchy-hom-id {M = M} .Hierarchy-hom.pres-mult =
+    let module M = Monad M in
+    idnt ∘nt M.mult
+      ≡⟨ Endo.idl _ ⟩
+    M.mult
+      ≡˘⟨ Endo.idr _ ⟩
+    M.mult ∘nt idnt
+      ≡˘⟨ ap (M.mult ∘nt_) Endo-∘.F-id ⟩
+    M.mult ∘nt (idnt ◆ idnt)
       ∎
 
-  hm : Hierarchy-map M O
-  hm .Hierarchy-map.nat = nat
-  hm .Hierarchy-map.pres-unit = pres-unit
-  hm .Hierarchy-map.pres-mult = pres-mult
--}
+  hierarchy-hom-∘ : ∀ {M N O : Hierarchy-theory o r}
+    → Hierarchy-hom N O
+    → Hierarchy-hom M N
+    → Hierarchy-hom M O
+  hierarchy-hom-∘ {M = M} {N} {O} ν ξ = hm where
+    module M = Monad M
+    module N = Monad N
+    module O = Monad O
+    module ν = Hierarchy-hom ν
+    module ξ = Hierarchy-hom ξ
+
+    hm : Hierarchy-hom M O
+    hm .Hierarchy-hom.nat = ν.nat ∘nt ξ.nat
+    hm .Hierarchy-hom.pres-unit =
+      (ν.nat ∘nt ξ.nat) ∘nt M.unit
+        ≡˘⟨ Endo.assoc ν.nat ξ.nat M.unit ⟩
+      ν.nat ∘nt (ξ.nat ∘nt M.unit)
+        ≡⟨ ap (ν.nat ∘nt_) ξ.pres-unit ⟩
+      ν.nat ∘nt N.unit
+        ≡⟨ ν.pres-unit ⟩
+      O.unit
+        ∎
+    hm .Hierarchy-hom.pres-mult =
+      (ν.nat ∘nt ξ.nat) ∘nt M.mult
+        ≡˘⟨ Endo.assoc ν.nat ξ.nat M.mult ⟩
+      ν.nat ∘nt (ξ.nat ∘nt M.mult)
+        ≡⟨ ap (ν.nat ∘nt_) ξ.pres-mult ⟩
+      ν.nat ∘nt (N.mult ∘nt (ξ.nat ◆ ξ.nat))
+        ≡⟨ Endo.assoc ν.nat N.mult (ξ.nat ◆ ξ.nat) ⟩
+      (ν.nat ∘nt N.mult) ∘nt (ξ.nat ◆ ξ.nat)
+        ≡⟨ ap (_∘nt (ξ.nat ◆ ξ.nat)) ν.pres-mult ⟩
+      (O.mult ∘nt (ν.nat ◆ ν.nat)) ∘nt (ξ.nat ◆ ξ.nat)
+        ≡˘⟨ Endo.assoc O.mult (ν.nat ◆ ν.nat) (ξ.nat ◆ ξ.nat) ⟩
+      O.mult ∘nt ((ν.nat ◆ ν.nat) ∘nt (ξ.nat ◆ ξ.nat))
+        ≡˘⟨ ap (O.mult ∘nt_) $ Endo-∘.F-∘ (ν.nat , ν.nat) (ξ.nat , ξ.nat) ⟩
+      O.mult ∘nt ((ν.nat ∘nt ξ.nat) ◆ (ν.nat ∘nt ξ.nat))
+        ∎
 
 --------------------------------------------------------------------------------
 -- Misc. Definitions
diff --git a/src/Mugen/Cat/Instances/HierarchyTheories.agda b/src/Mugen/Cat/Instances/HierarchyTheories.agda
new file mode 100644
index 0000000..c4754b1
--- /dev/null
+++ b/src/Mugen/Cat/Instances/HierarchyTheories.agda
@@ -0,0 +1,20 @@
+module Mugen.Cat.Instances.HierarchyTheories where
+
+open import Mugen.Prelude
+open import Mugen.Order.StrictOrder
+open import Mugen.Cat.HierarchyTheory
+
+--------------------------------------------------------------------------------
+-- The Category of Hierarchy Theories
+
+open Precategory
+
+Hierarchy-theories : ∀ (o r : Level) → Precategory (lsuc (o ⊔ r)) (lsuc (o ⊔ r))
+Hierarchy-theories o r .Ob = Hierarchy-theory o r
+Hierarchy-theories o r .Hom = Hierarchy-hom
+Hierarchy-theories o r .Hom-set _ _ = hlevel 2
+Hierarchy-theories o r .id = hierarchy-hom-id
+Hierarchy-theories o r ._∘_ = hierarchy-hom-∘
+Hierarchy-theories o r .idr _ = ext λ _ _ → refl
+Hierarchy-theories o r .idl _ = ext λ _ _ → refl
+Hierarchy-theories o r .assoc _ _ _ = ext λ _ _ → refl
diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda
index a750b07..c77a609 100644
--- a/src/Mugen/Everything.agda
+++ b/src/Mugen/Everything.agda
@@ -23,12 +23,14 @@ import Mugen.Algebra.Displacement.Subalgebra
 import Mugen.Algebra.OrderedMonoid
 import Mugen.Cat.HierarchyTheory
 import Mugen.Cat.HierarchyTheory.McBride
+import Mugen.Cat.HierarchyTheory.McBrideFunctoriality
 import Mugen.Cat.HierarchyTheory.Universality
 import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding
 import Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbeddingNaturality
 import Mugen.Cat.HierarchyTheory.Universality.SubcategoryEmbedding
 import Mugen.Cat.Instances.Displacements
 import Mugen.Cat.Instances.Endomorphisms
+import Mugen.Cat.Instances.HierarchyTheories
 import Mugen.Cat.Instances.Indexed
 import Mugen.Cat.Instances.StrictOrders
 import Mugen.Cat.Monad