Cuando intento definir opK
Definition opK : forall A:Set,A -> A :=
fun (A:Set)(x:A)(y:A) => x.
(*opK = def [x][y] x *)
me dice Error: The type of this term is a product while it is expected to be "A0".
Que estoy haciendo mal?
Hola Pablo.
El término fun (A:Set) (x:A) (y:A) => x tendría tipo forall A:Set, A -> A -> A y no: forall A:Set, A -> A.
En realidad el tipo más general de este operador (K) podría tener dos Sets diferentes (A y B) y el término sería:
fun (A B:Set) (x:A) (y:B) => x
con tipo forall A B:Set, A -> B -> A
Saludos, Carlos