From HoTT.Classes Require Import
     interfaces.canonical_names
     interfaces.orders
     interfaces.rationals
     theory.rationals.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Monomorphic Universe UQ.
Parameters (Q : Type@{UQ}) (Qap : Apart@{UQ UQ} Q)
  (Qplus : Plus Q) (Qmult : Mult Q)
  (Qzero : Zero Q) (Qone : One Q) (Qneg : Negate Q) (Qrecip : DecRecip Q)
  (Qle : Le@{UQ UQ} Q) (Qlt : Lt@{UQ UQ} Q)
  (QtoField : RationalsToField@{UQ UQ UQ UQ} Q)
  (Qrats : Rationals@{UQ UQ UQ UQ UQ UQ UQ UQ UQ UQ} Q)
  (Qtrivialapart : TrivialApart Q) (Qdec : DecidablePaths Q)
  (Qmeet : Meet Q) (Qjoin : Join Q) (Qlattice : LatticeOrder Qle)
  (Qle_total : TotalRelation (@le Q _))
  (Qabs : Abs Q).
(* I don't even want to know why this is necessary. *)
Parameter Qenum : Enumerable Q.
Notation "Q+" := (Qpos Q).

Global Existing Instances Qap Qplus Qmult Qzero Qone Qneg Qrecip
         Qle Qlt QtoField Qrats Qtrivialapart Qdec
         Qmeet Qjoin Qlattice Qle_total Qabs Qenum.