Timings for rationals.v
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 : 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 }.
#[export] Existing Instances rationals_field rationals_order rationals_to_field_mor.