Given a `{set A+B}`

value, is there a way to filter it to get a value of type `{set A}`

?

Kind of like this list version?

```
Fixpoint getLeft {A B: Type} (l: seq (A + B)): seq A :=
match l with
| [::] => [::]
| (inl a) :: l' => a :: getLeft l'
| _ :: l' => getLeft l'
end.
```

But since we can't do pattern match on sets, I wasn't sure how to go about this.

Tried like ` [set x in ab | is_inl x]. `

but that's still `{set A+B}`

.

Mathematically, this would be the union, for `x`

in `ab`

, of `\{a\}`

if `x`

is `inl a`

and `\emptyset`

otherwise.

Nevertheless, if you know an element of `A`

, it is probably better to filter the set (as you did) and map its element by sending `inr _`

to your distinguished element of `A`

.

Quentin's right, and you can also write it in one go: given `X : {set A + B}`

you can probably write `[set a | inl a \in X]`

.

also known as `inl @^-1: X`

(the preimage of `X`

by `inl`

)

Thanks!

What does `\{a\}`

mean? It's not latex stuff, is it?

if you know an element of A, it is probably better to filter the set (as you did) and map its element by sending inr _ to your distinguished element of A.

I didn't get this part. Why do we need to have a particular element of `A`

?

Ah, yes, sorry, it is indeed LaTeX stuff, you can ignore the backslashes, I meant the singleton containing `a`

.

You would do your map with a function from `A+B`

to `A`

. This function does not know that your set contains only elements of the form `inl _`

, so you need to define where to send inputs of the form `inr _`

, hence the distinguished element of `A`

.

Last updated: Jul 23 2024 at 20:01 UTC