Go backward to A Rectangle Package Go up to Top Go forward to Bounded Quantification

A Figures Package

type FiguresWRT3[RectRep, CircleRep, PointRep] -
  {circlePackage: CircleWRT[CircleRep, PointRep],
   rectPackage: RectWRT[RectRep, PointRep],
   boundingRect: CircleRep -> RectRep}

type FIguresWRT1[PointRep] =
   exists RectRep. exists CircleRep.
      FigureWRT3[RectRep, CircleRep, PointRep]
type Figures = exists PointRep. FIgureWRT1[PointRep]
type FiguresModule = forall PointRep.
   PointWRT[PointRep] -> FiguresWRT1[PointRep]

value figuresModule: FIguresModule =
all[PointRep]
   fun(p: PointWRT[PointRep])
      pack[PointRep' = PointRep
         in FiguresWRT1[PointRep]]
      open circleModule[PointRep](p) as c[CircleRep] in
         open rectModule[PointRep](p) as r[RectRep] in
           {circlePackage = c, ...}