Nuprl Definition : is-equiv-witness
is-equiv-witness(G;A;c;p) == (λcontr-witness(G.A;c;p))
Definitions occuring in Statement :
contr-witness: contr-witness(X;c;p),
cubical-lambda: (λb),
cube-context-adjoin: X.A
Definitions occuring in definition :
cubical-lambda: (λb),
contr-witness: contr-witness(X;c;p),
cube-context-adjoin: X.A
FDL editor aliases :
is-equiv-witness
Latex:
is-equiv-witness(G;A;c;p) == (\mlambda{}contr-witness(G.A;c;p))
Date html generated:
2018_05_23-AM-09_42_00
Last ObjectModification:
2017_11_06-PM-06_13_36
Theory : cubical!type!theory
Home
Index