Nuprl Definition : contr-witness
contr-witness(X; c; p) == cubical-pair(c;(λp))
Definitions occuring in Statement :
cubical-pair: cubical-pair(u;v),
cubical-lambda: (λb)
Definitions occuring in definition :
cubical-lambda: (λb),
cubical-pair: cubical-pair(u;v)
Latex:
contr-witness(X; c; p) == cubical-pair(c;(\mlambda{}p))
Date html generated:
2017_01_10-AM-08_56_00
Last ObjectModification:
2016_11_30-PM-06_41_19
Theory : cubical!type!theory
Home
Index