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