diff --git a/src/Felix/Homomorphism.agda b/src/Felix/Homomorphism.agda
index 21aef86..b40137c 100644
--- a/src/Felix/Homomorphism.agda
+++ b/src/Felix/Homomorphism.agda
@@ -39,7 +39,7 @@ record CategoryH
     F-∘³ : {a₀ a₁ a₂ a₃ : obj₁}
            {f₁ : a₀ ⇨₁ a₁}{f₂ : a₁ ⇨₁ a₂}{f₃ : a₂ ⇨₁ a₃}
          → Fₘ (f₃ ∘ f₂ ∘ f₁) ≈ Fₘ f₃ ∘ Fₘ f₂ ∘ Fₘ f₁
-    F-∘³ = F-∘ ; ∘≈ʳ F-∘
+    F-∘³ = trans ⦃ r = eq₂ ⦄ F-∘ (∘≈ʳ F-∘)
 
     F-∘⁴ : {a₀ a₁ a₂ a₃ a₄ : obj₁}
            {f₁ : a₀ ⇨₁ a₁}{f₂ : a₁ ⇨₁ a₂}{f₃ : a₂ ⇨₁ a₃}{f₄ : a₃ ⇨₁ a₄}