## Stream: Coq users

### Topic: ✔ UniMath Sigma Types Wont Bind a Family of Type

#### 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: Jun 15 2024 at 08:01 UTC