Nuprl Definition : closed-type-to-type
closed-type-to-type(T) == let A,F = T in <λI,a. (A I), λI,J,f,a,u. (F I J f u)>
Definitions occuring in Statement :
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
spread: spread def,
pair: <a, b>,
lambda: λx.A[x],
apply: f a
FDL editor aliases :
closed-type-to-type
Latex:
closed-type-to-type(T) == let A,F = T in <\mlambda{}I,a. (A I), \mlambda{}I,J,f,a,u. (F I J f u)>
Date html generated:
2020_05_20-PM-01_50_47
Last ObjectModification:
2020_03_20-AM-10_31_15
Theory : cubical!type!theory
Home
Index