Horizontal composition does not compile anymore in later version of agda

[HuStmpHrrr]

In 2.5.4.2, horizontal composition of natural transformations doesn't compile anymore, due to failure of inference of metavariables. I am not sure whose problem it is. Any chance you can take a look?

[JacquesCarette]

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.

[p-pavel]

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))

[JacquesCarette]

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

[HuStmpHrrr]

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?

[JacquesCarette]

(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.

[JacquesCarette]

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