Has type

Stream: new members

[Daniel Dávalos]

How can I define if an element has a type $\alpha$ or $\beta$?
I want to write something this

def preset {\alpha : Type} {\beta : Type} {\gamma : Type} (t : ? ) : Set \gamma :=
   if (t : \alpha)? then do_something t else do_else t

[Martin Dvořák]

docs#Sum