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:
2019_10_31-AM-07_19_40
Last ObjectModification:
2018_10_15-PM-01_15_32
Theory : lattices
Home
Index