Library HoTT.Classes.interfaces.rationals

Require 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 : ∀ (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 : ∀ {B} `{IsField B} `{!FieldCharacteristic B 0},
    IsSemiRingPreserving (rationals_to_field A B)
  ; rationals_initial : ∀ {B} `{IsField B} `{!FieldCharacteristic B 0}
    {h : A → B} `{!IsSemiRingPreserving h} x,
    rationals_to_field A B x = h x }.
#[export] Existing Instances rationals_field rationals_order rationals_to_field_mor.