Tim Baumann

I'm getting the "invalid non-exhaustive set of equations" error for the `directed_associator_coherence_thm` lemma that is commented out at the end of [this file](https://github.com/semorrison/lean-monoidal-categories/blob/01ae68a488b0976bf17fd7a44aee28c17cc0cbbd/coherence_thm.lean). Here's a version that is cleaned up...

When I run ```bash $ env TRAVIS_BUILD_DIR=/home/Projects/HoTT-Agda agda --library-file=travis-script/libraries --without-K --rewriting theorems/index1.agda ``` I get the following error: ``` [...] Checking cohomology.SpectrumModel (/home/Projects/HoTT-Agda/theorems/cohomology/SpectrumModel.agda). Checking groups.SuspAdjointLoop (/home/Projects/HoTT-Agda/theorems/groups/SuspAdjointLoop.agda). Checking groups.FromSusp (/home/Projects/HoTT-Agda/theorems/groups/FromSusp.agda). An...

The/One problematic definition is ``` abstract C-additive-is-equiv : is-equiv (GroupHom.f (Πᴳ-fanout (C-fmap n ∘ ⊙bwin {X = X}))) C-additive-is-equiv = transport is-equiv (λ= $ Trunc-elim (λ _ → idp)) ((ac...

The commit above solves this issue by giving two implicit arguments of `transport` explicitly instead of letting Agda infer them.

Apart from `homotopy.GroupSetsRepresentCovers`, which is stubbornly resisting my attempts, all modules typecheck successfully with Agda 2.5.4 now.

Also `homotopy.3x3.PushoutPushout` doesn't check in a reasonable amount of time with 2.5.4 (I've abborted typechecking after the process ran for one hour).

@favonia Yes, it is a workaround for a bug that causes Agda 2.5.4 to not apply available rewriting rules. I don't have any good insight into what the specific circumstances...

Yes, that's possible

Here's the Agda issue for the internal error in InstanceArguments: https://github.com/agda/agda/issues/3125

I've tried getting my `cup-products` branch working with 2.5.4, but there again is a module that seems to get Agda into an infinite loop: More specifically, checking [the term in...