Nuprl Definition : type-functor-product
p * q == let F,MF = p in let G,MG = q in <λT.(F T × (G T)), λf,p. let x,y = p in <MF f x, MG f y>>
Definitions occuring in Statement :
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
product: x:A × B[x]
Definitions occuring in definition :
product: x:A × B[x],
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
apply: f a
Latex:
p * q == let F,MF = p in let G,MG = q in <\mlambda{}T.(F T \mtimes{} (G T)), \mlambda{}f,p. let x,y = p in <MF f x, MG f y>>
Date html generated:
2016_05_15-PM-01_44_45
Last ObjectModification:
2015_09_23-AM-07_37_01
Theory : basic
Home
Index