A Rectangle Package

type RectWRT2[RectRep, PointRep] =
  {pointPackage: PointWRT[PointRep],
   mkrect: (PointRep x PointRep) $->$ RectRep, ...}

type RectWRT1[PointRep] =
   exists RectRep. RectWRT2[RectRep, PointRep]
type Rect = exists PointRep. RectWRT1[PointRep]
type RectModule = forall PointRep.
   PointWRT[PointRep] $->$ RectWRT1[PointRep]

value rectModule: RectModule =
all[PointRep]
   fun(p: PointWRT[PointRep])
      pack[PointRep' = PointRep
         in RectWRT1[PointRep']]
     {pointPackage = p,
      mkrect = fun(tl: PointRep, br: PointRep) ...}