`sigT`

for one variable looks like `{x:A & P x}`

, right?

How can we extend it to more than one variable (disregarding the fact that we got `sigT2`

. To find out how it can be extended to `sigTn`

)?

I was trying to have something like `{a b | (fun a b => a < b)}`

How would it look like?

Is it like

```
{a:nat &
{b:nat & (fun b => a < b)}
}
```

Is the following definition OK?

```
Definition X : {a:nat & {b: nat & {c: nat | a + b = c}}}.
now exists 3, 4, 7.
Defined.
Compute projT1 X.
```

Thanks!

So, for the `a < b`

example, we can do like

```
Definition X : {a:nat & {b: nat | a < b}}.
```

right?

You can also use `{'(a,b) & a < b}`

.

That worked as well. Thanks.

Can have multiple values like `Definition X'' : {'(a,b,c) & (a<b<c)}.`

as well.

Makes it concise and handy.

Julin S has marked this topic as resolved.

Last updated: Jun 18 2024 at 08:01 UTC