Raymond Baker (Feb 07 2022 at 13:00): Raymond Baker (Feb 07 2022 at 13:00):I'm working with the UniMath Sigma types. I'm trying to write a statement that involves a sigma type binding a function F : A -> UU, where A is an already declared point of the universe. However, I keep getting an error that says the Sigma binder is expecting a type instead of F. I'm not to versed on the intricacies of how the UniMath Sigma type is defined but I think this error may have to do with F : A -> UU being a type family. Is there a way to get F : A -> UU recognized as the term to be bound.?
Gaëtan Gilbert (Feb 07 2022 at 13:02):what exactly did you write?
Raymond Baker (Feb 07 2022 at 13:14):@Gaëtan Gilbert Heres the relevant piece of text: ... {A B : UU} := ∑ (F : (A → B) → UU), ...
Raymond Baker (Feb 07 2022 at 13:15):The error I get is "Found type "(A → B) → UU" where "?T" was expected".
Ali Caglayan (Feb 07 2022 at 13:22):I think ∑ is a notation, so you want to write ∑ (x : A), P x. The actual sigma type underneath is called total2 so this would become total2 P.
Gaëtan Gilbert (Feb 07 2022 at 13:23):how's that different from what he wrote?
Ali Caglayan (Feb 07 2022 at 13:23):I might have misunderstood then, I though you were trying to get total2 F
Raymond Baker (Feb 07 2022 at 18:56):Yea, unfortunately that doesn't fix things up
Gaëtan Gilbert (Feb 07 2022 at 21:55):unimath expects to be run with -type-in-type (command line) or equivalently Unset Universe Checking.
Raymond Baker (Feb 08 2022 at 00:59):Thank you so much @Gaëtan Gilbert ! This would have taken me forever to figure out. I'm a bit of a novice...
Notification Bot (Feb 08 2022 at 00:59):Raymond Baker has marked this topic as resolved.
Last updated: Oct 03 2023 at 21:01 UTC