Leyendo la letra me surge la siguiente duda:
¿ A qué se refiere con versión paramétrica ?
¿Implica hacer las definiciones de la forma Definition X : A -> B -> ... := ... . ?
Gracias !
Hola.
Se refiere a cuantificar sobre los sets, permitiendo instanciarlos en aplicaciones posteriores. Por ejemplo, la versión paramétrica del operador I podría ser:
Definition I : forall A:Set, A -> A :=
fun (A:Set) (x:A) => x.
Saludos, Carlos