Horizontal composition does not compile anymore in later version of agda about categories HOT 6 CLOSED

I noticed that some time back, but have not had a chance to dig in. Thanks for the bump, it helps hike the priority. The fix isn't entirely straightforward, and I'd like to report it as a regression too.

from categories.

I'm currently trying to bring the library up to date with current stdlib and Agda.

Talking about natural transformations -- the problem is with the signature of assoc₀ -- type checker can't infer an implicit parameter for ∘₀.

I don't understand how it used to compile before -- inferring the parameter requires functor composition ({F = H ∘F F} {I ∘F G} ):

.assoc₀ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃} 
            {C₀ : Category o₀ ℓ₀ e₀} {C₁ : Category o₁ ℓ₁ e₁} {C₂ : Category o₂ ℓ₂ e₂} {C₃ : Category o₃ ℓ₃ e₃} 
            {F G : Functor C₀ C₁} {H I : Functor C₁ C₂} {J K : Functor C₂ C₃}
        → {X : NaturalTransformation F G} → {Y : NaturalTransformation H I} → {Z : NaturalTransformation J K}
        → (Z ∘₀ Y) ∘₀ X ≡ (_∘₀_   {F = H ∘F F} {I ∘F G} Z  (_∘₀_ {C = C₀} {C₁} {C₂} Y  X))

from categories.

And it's even worse in 1.0, it crashes because of irrelevance.

from categories.

I am wondering by how much is it broken? is it worth fixing or better start another category theory library from scratch, potentially taking advantages of 2.6?

from categories.

(posting this here too, as a PR is not the best place for a discussion)
Super broken - I encounter hard errors from Agda, a la

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:289

on quite a few files. I think "from scratch" is now the way to go.

from categories.

This library can now be declared obsolete, so closing this as irrelevant.

from categories.