Nuprl Definition : cubical-pair
cubical-pair(u;v) == λI,a. <u I a, v I a>
Wellformedness Lemmas :
cubical-pair_wf
Definitions occuring in Statement :
apply: f a
,
lambda: λx.A[x]
,
pair: <a, b>
Definitions occuring in definition :
lambda: λx.A[x]
,
pair: <a, b>
,
apply: f a
FDL editor aliases :
cubical-pair
cubical-pair
Latex:
cubical-pair(u;v) == \mlambda{}I,a. <u I a, v I a>
Date html generated:
2016_06_16-PM-05_46_19
Last ObjectModification:
2015_09_23-AM-09_30_52
Theory : cubical!sets
Home
Index