let object = Type

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