Require Export UniMath.Algebra.Domains_and_Fields.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.Groups.

Lemma isapropmultinvpair :
  ∏ (X : rig) (x : X), isaprop (multinvpair X x).
Proof.
  intros X x.
  apply isapropinvpair.
Qed.

Section fld_proj.

Context {X : fld}.

Definition zero_fld : X := 0%ring.
Definition one_fld : X := 1%ring.
Definition plus_fld (x y : X) : X := (x + y)%ring.
Definition opp_fld (x : X) : X := (- x)%ring.
Definition minus_fld (x y : X) : X := (x - y)%ring.
Definition mult_fld (x y : X) : X := (x × y)%ring.
Definition inv_fld (x : X) : X.
Proof.
  apply sumofmaps with (3 := fldchoice x) ; intro x'.
  - exact (pr1 x').
  - exact x.
Defined.
Definition div_fld (x y : X) : X := mult_fld x (inv_fld y).

End fld_proj.

Section fld_struct.

Context (X : fld).

Definition fld_to_gr1 : gr :=
  abgrtogr (pr1fld X).

Definition fld_to_monoid1 : monoid :=
  grtomonoid fld_to_gr1.

Definition fld_to_monoid2 : monoid :=
  ringmultmonoid (pr1fld X).

End fld_struct.