The intersection type ⌜⋂x:a. b⌝ is a primitive type.
The rules for it are:
Error :isectFormation
isectEquality
isect_memberFormation
isect_memberEquality
Error :isect_member_caseEquality
isectElimination
Error :isectUniverseElim
independent_isectElimination⋅


Home Index