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.?

what exactly did you write?

@Gaëtan Gilbert Heres the relevant piece of text: ... {A B : UU} := ∑ (F : (A → B) → UU), ...

The error I get is "Found type "(A → B) → UU" where "?T" was expected".

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`

.

how's that different from what he wrote?

I might have misunderstood then, I though you were trying to get `total2 F`

Yea, unfortunately that doesn't fix things up

unimath expects to be run with -type-in-type (command line) or equivalently Unset Universe Checking.

Thank you so much @Gaëtan Gilbert ! This would have taken me forever to figure out. I'm a bit of a novice...

Raymond Baker has marked this topic as resolved.

Last updated: Jun 15 2024 at 08:01 UTC