Possible workaround instance search issue

conal · Jan 17, 2024 · e67c9a7 · e67c9a7
1 parent 6dd2c40
commit e67c9a7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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₄}