let object = Type

in  λ(m : object) →
    λ(field : ./Type m) →
        { additive =
            ../../Group/OrderedCommutative/extractPartiallyOrderedCommutativeGroup
              m
              field.additive
        , multiplicative = field.multiplicative
        }
      : ../PartiallyOrdered/Type m