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

piSort/funSort of IUniv should be blocked on the codomain #6074

Closed
plt-amy opened this issue Sep 2, 2022 · 0 comments
Closed

piSort/funSort of IUniv should be blocked on the codomain #6074

plt-amy opened this issue Sep 2, 2022 · 0 comments
Labels
cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp piSort Caused by or relating to the treatment of Π type sorts sorts Agda's sort system (see also piSort); univSort; Sort metas; Fibrancy type: bug Issues and pull requests about actual bugs
Milestone
2.6.3

Comments

@plt-amy
Copy link
Member

plt-amy commented Sep 2, 2022

... I think those are the right words in the title, at least, I haven't investigated yet. But consider:

open import Agda.Primitive.Cubical

_ : Set
_ = I → ?

this is a hard type error, but I → Nat (e.g.) has type set. So really this should be fine, with a postponed funSort IUniv ... = Set constraint?
@plt-amy plt-amy added type: bug Issues and pull requests about actual bugs sorts Agda's sort system (see also piSort); univSort; Sort metas; Fibrancy cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp piSort Caused by or relating to the treatment of Π type sorts labels Sep 2, 2022
@plt-amy plt-amy closed this as completed in 6da779f Sep 2, 2022
@plt-amy plt-amy mentioned this issue Sep 13, 2022
Closed
@andreasabel andreasabel added this to the 2.6.3 milestone Oct 24, 2022
@andreasabel andreasabel mentioned this issue Oct 24, 2022
Closed
@asr asr changed the title piSort/funSort of IUniv should be blocked on the codomain piSort/funSort of IUniv should be blocked on the codomain Jan 23, 2023
@asr asr changed the title piSort/funSort of IUniv should be blocked on the codomain piSort/funSort of IUniv should be blocked on the codomain Jan 23, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp piSort Caused by or relating to the treatment of Π type sorts sorts Agda's sort system (see also piSort); univSort; Sort metas; Fibrancy type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
2.6.3
Development

No branches or pull requests
2 participants
@andreasabel @plt-amy