Nuprl Definition : p-type
PType == A,B:Type//(A ⇐⇒ B)
Definitions occuring in Statement :
quotient: x,y:A//B[x; y],
iff: P ⇐⇒ Q,
universe: Type
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
universe: Type,
iff: P ⇐⇒ Q
FDL editor aliases :
p-type
Latex:
PType == A,B:Type//(A \mLeftarrow{}{}\mRightarrow{} B)
Date html generated:
2020_05_20-AM-08_24_27
Last ObjectModification:
2018_10_15-PM-01_15_32
Theory : lattices
Home
Index