Nuprl Definition : discrete-function-inv
discrete-function-inv(X; b) == (λλI,alpha. (b(fst(alpha)) q(alpha)))
Definitions occuring in Statement :
cubical-lambda: (λb),
cc-snd: q,
cubical-term-at: u(a),
pi1: fst(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
cc-snd: q,
cubical-term-at: u(a),
pi1: fst(t),
apply: f a,
lambda: λx.A[x],
cubical-lambda: (λb)
Latex:
discrete-function-inv(X; b) == (\mlambda{}\mlambda{}I,alpha. (b(fst(alpha)) q(alpha)))
Date html generated:
2017_02_21-AM-10_46_08
Last ObjectModification:
2017_02_15-PM-03_12_22
Theory : cubical!type!theory
Home
Index