let object = Type

in  λ(m : object) →
    λ(group : ./Type m) →
      group.{ eq, unit, inverse, le, product } : ../PartiallyOrdered/Type m