Category & Functor need to be marked with eta-equality to satisfy 2.5.4.2
p-pavel opened this issue · 4 comments
I don't know is this type checker behaviour correct. The documentation states:
By default, all (inductive) record types enjoy eta-equality if the positivity checker has confirmed it is safe to have it. The keywords eta-equality/no-eta-equality enable/disable eta rules for the record type being declared.
But without eta-equality keyword
Category.op (Category.op c) ≢ c
and same for Functor.
For example this breaks DinaturalTransformation.agda
Yes, I suspected that this was the issue. This seems to be a regression. Trying to remove the parts that are not relevant to make a good bug report was what blocked me from doing so.
Should I add eta-equality to the Category and Functor declarations for now?
For me it is an issue with type checker but marking those records won't hurt.
Yes please. I agree, it won't hurt.
From some investigation, this was caused by some interactions between irrelevance and eta. In the new library, proofs are relevant, so this is a non-issue. [And op op is not longer the identity on the nose, so coherence morphisms need to be inserted anyways]