Nuprl Definition : isect def
The intersection of a family of types is a new primitive type.
Its partial equivalence relation is the intersection of all the
partial equivalence relations in the family.
Thus, u = v in ⋂x:A. B[x] just when u = v in B[x] for every ⌜x ∈ A⌝.
Viewed a proposition, the intersection type can be seen as
"uniform" universal quantification, ⌜∀[x:A]. B[x]⌝⋅
⋂x:A. B[x] == PRIMITIVE
Rules referencing :
isectEquality,
isect_memberFormation,
isect_memberEquality,
isect_member_caseEquality,
isectElimination,
independent_isectElimination,
callbyvalueApplyCases,
exceptionApplyCases
FDL editor aliases :
isect
given
Latex:
\mcap{}x:A. B[x] == PRIMITIVE
Date html generated:
2016_07_08-PM-04_46_24
Last ObjectModification:
2015_10_29-PM-07_03_30
Theory : core_1
Home
Index