Un término del tipo A×B contiene ¿cuántas componentes?
Un producto guarda un par.
El constructor del producto A×B recibe un término de A y un término de B.
Los guarda como un par ordenado (a,b), incluso si A y B coinciden.
Por tanto tiene 2 componentes; eso no significa que el tipo producto tenga solo dos elementos.
¿λx.x tiene tipo A→A? Responde sí/no.
Comprueba entrada y salida.
Introducimos x:A como entrada hipotética.
El cuerpo x ya tiene tipo A, que es el tipo de salida requerido.
La respuesta es sí.
¿Cuántos booleanos hay en el tipo Bool usual?
Sus constructores son true y false.
Tomamos el tipo inductivo Bool usual, con constructores true y false sin campos adicionales.
Son constructores distintos y el principio de análisis de Bool reduce cualquier caso a una de esas dos posibilidades.
En ese sentido habitual hay exactamente 2 booleanos.
Construye A→(B→A).
La segunda entrada puede ignorarse.
Introducimos b:B y devolvemos a, que sigue disponible y conserva su tipo A.
No se requiere usar b.
Explica la diferencia entre demostrar ∃n:P(n) y escribir un nombre de variable n.
Una existencia constructiva contiene también evidencia.
Una existencia sobre naturales exige un testigo concreto n:N en el marco constructivo considerado.
Además se requiere evidencia de P(n), vinculada precisamente a ese valor.
Nombrar una variable n solo abre una hipótesis de contexto; sin testigo cerrado ni evidencia no se ha construido la existencia.