Un "ensemble" en logique d'ordre supérieur...

Zlotz

Bonjour à tous
En logique d'ordre supérieur on peut modéliser un ensemble par une fonction à valeurs dans le type des propositions. Par exemple le singleton {0} peut être vu comme la fonction f : <type de 0> -> Prop telle que le seul antécédent de True est 0.

Mais cette façon de faire ne permet pas de créer un ensemble dont les éléments ont des types différents. Par exemple, l'ensemble ne contenant que 0 et {0} ne peut être modélisé par une fonction f : T -> Prop puisqu'aucun type T ne convient.

Ma question est : est-il possible de modéliser en logique d'ordre supérieur des ensembles contenant des objets de types différents ?