search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
442 stars 134 forks source link

Presheaf definition leads to unsolved metavariable for base category #1010

Open jpoiret opened 1 year ago

jpoiret commented 1 year ago

Hi everyone,

Since Presheaf C ... is defined as Functor (C ^op) (SETS ...), C can't be inferred from an argument P : Presheaf C .... This is because Agda 2.6.3 can't solve sym _A = B for paths _A and B, so can't deduce the original ⋆Assoc. This should be fixed in https://github.com/agda/agda/pull/6645, but in the meantime, should we refactor Presheaves to have Copresheaves as the primary type on which everything is defined? This way, there's no reason to have to solve _C ^op = C.

maxsnew commented 1 year ago

Have you tried out agda HEAD to see that it is fixed? I don't think we should bother making a big change if we know it's fixed in the next version of Agda anyway.

jpoiret commented 1 year ago

Not yet, but I do expect this to work on latest HEAD.

maxsnew commented 2 months ago

has this been fixed upstream?