Nuprl Definition : discrete-pair
discrete-pair(p) == λI,alpha. <p.1(alpha), p.2(alpha)>
Definitions occuring in Statement :
cubical-snd: p.2,
cubical-fst: p.1,
cubical-term-at: u(a),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
cubical-snd: p.2,
cubical-term-at: u(a),
cubical-fst: p.1,
pair: <a, b>,
lambda: λx.A[x]
FDL editor aliases :
discrete-pair
Latex:
discrete-pair(p) == \mlambda{}I,alpha. <p.1(alpha), p.2(alpha)>
Date html generated:
2017_02_21-AM-10_48_10
Last ObjectModification:
2017_02_20-AM-11_18_35
Theory : cubical!type!theory
Home
Index