let Order = ../Group/Ordered/Order

in    { eq = λ(_ : {}) → λ(_ : {}) → True
      , unit = λ(_ : {}) → {=}
      , inverse = λ(_ : {}) → {=}
      , le = λ(_ : {}) → λ(_ : {}) → True
      , product = λ(_ : { _1 : {}, _2 : {} }) → {=}
      , compare = λ(_ : {}) → λ(_ : {}) → Order.EQ
      }
    : ../Group/Ordered/Type {}