Nuprl Definition : e-type
EType == A,B:Type//A ≡ B
Definitions occuring in Statement :
quotient: x,y:A//B[x; y],
ext-eq: A ≡ B,
universe: Type
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
universe: Type,
ext-eq: A ≡ B
FDL editor aliases :
e-type
Latex:
EType == A,B:Type//A \mequiv{} B
Date html generated:
2020_05_20-AM-08_24_24
Last ObjectModification:
2018_10_12-PM-00_18_24
Theory : lattices
Home
Index