Nuprl Definition : discrete-pair-inv
discrete-pair-inv(X;b) == cubical-pair(λI,alpha. (fst(b(alpha)));λI,alpha. (snd(b(alpha))))
Definitions occuring in Statement :
cubical-pair: cubical-pair(u;v),
cubical-term-at: u(a),
pi1: fst(t),
pi2: snd(t),
lambda: λx.A[x]
Definitions occuring in definition :
cubical-term-at: u(a),
pi2: snd(t),
lambda: λx.A[x],
pi1: fst(t),
cubical-pair: cubical-pair(u;v)
FDL editor aliases :
discrete-pair-inv
Latex:
discrete-pair-inv(X;b) == cubical-pair(\mlambda{}I,alpha. (fst(b(alpha)));\mlambda{}I,alpha. (snd(b(alpha))))
Date html generated:
2017_02_21-AM-10_48_37
Last ObjectModification:
2017_02_20-AM-11_46_43
Theory : cubical!type!theory
Home
Index