Nuprl Definition : bool-negation-equiv
bool-negation-equiv(X) == bijection-equiv(X;𝔹;𝔹;λb.(¬bb);λb.(¬bb))
Definitions occuring in Statement :
bijection-equiv: bijection-equiv(X;A;B;f;g),
bnot: ¬bb,
bool: 𝔹,
lambda: λx.A[x]
Definitions occuring in definition :
bnot: ¬bb,
lambda: λx.A[x],
bool: 𝔹,
bijection-equiv: bijection-equiv(X;A;B;f;g)
FDL editor aliases :
bool-negation-equiv
Latex:
bool-negation-equiv(X) == bijection-equiv(X;\mBbbB{};\mBbbB{};\mlambda{}b.(\mneg{}\msubb{}b);\mlambda{}b.(\mneg{}\msubb{}b))
Date html generated:
2017_02_21-AM-11_04_40
Last ObjectModification:
2017_02_10-PM-06_42_38
Theory : cubical!type!theory
Home
Index