Alex Gryzlov

* Implicit name clashes (for `j`) in `Free.FreeFunctor.foldPath` * `MonoidalCategory.StrictMonoidalCategory.tensorIsAssociativeMor` doesn't typecheck with ``` Can't solve constraint between: mapObj tensor (a, c) and a ``` * Pattern-matching lambdas in `MonoidalCategory.SymmetricMonoidalCategoryHelpers.swapFunctor`...

* Adding `unitCoherence` to `MonoidalCategory.SymmetricMonoidalCategory` causes the compiler to crash with `Segmentation fault (core dumped)`.

Looks like the upstream bug is fixed, is the proof going through now?

Wow, my master is really behind, feel free to squash :)

This also comes up when defining something like: ``` def prop/unit (A : type) (A/prop : is-prop A) (x0 : A) : equiv A unit = iso→equiv A unit (λ...

I've tried plugging that case with a filler like this: ``` def helper (A : type) (A/prop : is-prop A) (a : A) (i j : 𝕀) : type =...

@jonsterling Does this have something to do with the path/identity distinction, or is it something more prosaic? :)

I've tried adding the motive, but now the hole became something like a `j/k`-square, where the `j` side involves a function on `k`, and vice versa the `k` side depends...

Hm, it looks like that hole should be pluggable by `connection/both^1 type (uA a) (Au a) k j `, but it gives me a `"global variable name mismatch"` ¯\_(ツ)_/¯ EDIT:...

Ok I think I've narrowed down the construction of `P` to this helper : ``` def help (A : type) (abx : 𝕀 → A) (aby : [k] A [k=0...