I see. Thank you Ana and Paolo. I thought about how to use a function taking `{T : choiceType} (x : T)`

to be able to write `sg nat nat`

. Since a particular `nat`

value has to be given to the function for it to recreate `T`

, I don't think it's possible. I came up with this simple notation instead.

```
Notation sgn := (sg [choiceType of nat] [choiceType of nat]).
```

I think that'll be enough for now. Thank you.

Ricardo has marked this topic as resolved.

Last updated: Jan 29 2023 at 19:02 UTC