Yoneda is broken

[tetrapharmakon]

The following code containing only a few imports

open import Categories.Category.Core 
open import Level

module Categories.Adjoint.Duploid {o l e} {C D : Category o l e} where

open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.NaturalTransformation
open import Categories.Adjoint
open import Categories.Adjoint.Properties using (adjoint⇒monad; adjoint⇒comonad)
import Categories.Morphism.Reasoning as MR

yields an error

src/Categories/Yoneda.agda:80,25-43
Functor.F₁ F (Category.id C.op) ⟨$⟩ _x_256 != η y a ⟨$⟩ id of type
Setoid.Carrier (Functor.F₀ F a)
when checking that the expression F.identity SE.refl has type
(Functor.F₀ F a Setoid.≈ η y a ⟨$⟩ id) x

More precisely, importing Categories.Adjoint.Properties raises the problem.

On a different machine, a few hours before, a similar error was thrown (same file, but different: it said that yoneda-inverse didn't have the fields f, f^{-1}, etc, but instead to, from, to-cong, from-cong and inverse). Considering the issue is present on two different machines, I doubt this has to do with my local version of the repo, so... what happened?

[JacquesCarette]

Wild guess (don't have time to look at the details right now): you have a different version of stdlib. 1.7 and 2.0 are very different, and agda-categories only works for sure with 1.7. There's a PR with 2.0 compatibility, but it won't get pulled in until 2.0 is shipped.

[tetrapharmakon]

It is very likely. I indeed have 2.0 on both machines... So it's me! Good to know.

[JacquesCarette]

You might be able to pull PR #452 into your development, and that might work. Or revert to 1.7.

[tetrapharmakon]

You probably mean #352 but it seems I can't pull it locally (it's a work in progress)

[JacquesCarette]

Typo, yes. git merge the commits?

[JacquesCarette]

So can I close this issue?