Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Presheaf definition leads to unsolved metavariable for base category #1010

Open
jpoiret opened this issue Jun 8, 2023 · 3 comments
Open

Presheaf definition leads to unsolved metavariable for base category #1010

jpoiret opened this issue Jun 8, 2023 · 3 comments

Comments

@jpoiret
Copy link
Contributor

jpoiret commented Jun 8, 2023 •
edited
Loading

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 agda/agda#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.
@jpoiret jpoiret mentioned this issue Jun 20, 2023
Merged
@felixwellen felixwellen mentioned this issue Jun 20, 2023
Closed
@maxsnew
Copy link
Collaborator

maxsnew commented Jun 21, 2023

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
Copy link
Contributor Author

jpoiret commented Jun 23, 2023

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

@maxsnew
Copy link
Collaborator

maxsnew commented May 9, 2024

has this been fixed upstream?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@maxsnew @jpoiret