Yoneda is broken #396
Description
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?