Require ImportRequire Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders.

(* Universes:
  - i universe of origin type
  - j universe of target types
  - k universe of applied apart of target types
  - l universe of Field property of target types 
*)
Class RationalsToField@{i j k l} (A : Type@{i}) :=
  rationals_to_field : forall (B : Type@{j}) `{IsField@{j l k} B}
    `{!FieldCharacteristic B 0}, A -> B.

Arguments rationals_to_field A {_} B {_ _ _ _ _ _ _ _ _} _.


(* The Rationals are the initial field of characteristic 0. *)

Class Rationals A {Aap : Apart A} {Aplus Amult Azero Aone Aneg Arecip Ale Alt}
  `{U : !RationalsToField A} :=
  { rationals_field :: @IsDecField A Aplus Amult Azero Aone Aneg Arecip
  ; rationals_order :: FullPseudoSemiRingOrder Ale Alt
  ; rationals_to_field_mor :: forall {B} `{IsField B} `{!FieldCharacteristic B 0},
    IsSemiRingPreserving (rationals_to_field A B)
  ; rationals_initial : forall {B} `{IsField B} `{!FieldCharacteristic B 0}
    {h : A -> B} `{!IsSemiRingPreserving h} x,
    rationals_to_field A B x = h x }.