agda
Yoneda is broken
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?
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.
It is very likely. I indeed have 2.0 on both machines... So it's me! Good to know.
You might be able to pull PR #452 into your development, and that might work. Or revert to 1.7.
You probably mean #352 but it seems I can't pull it locally (it's a work in progress)