Require Import
  HoTT.Types.Arrow.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Export
  HoTT.Classes.interfaces.abstract_algebra.
Require Import HoTT.Classes.theory.rings.


Module SemiRings.

Class Operations
  := operations : sig (fun T => Plus T * Mult T * Zero T * One T)%type.

Definition BuildOperations (T : Type) `{Plus T} `{Mult T} `{Zero T} `{One T}
  : Operations
  := exist _ T (plus,mult,zero,one).

Coercion SR_carrier (s : Operations) : Type := s.1.
#[export] Instance SR_plus (s : Operations) : Plus s := fst (fst (fst s.2)).
#[export] Instance SR_mult (s : Operations) : Mult s := snd (fst (fst s.2)).
#[export] Instance SR_zero (s : Operations) : Zero s := snd (fst s.2).
#[export] Instance SR_one (s : Operations) : One s := snd s.2.

Arguments SR_plus !_ / _ _.
Arguments SR_mult !_ / _ _.
Arguments SR_zero !_ /.
Arguments SR_one !_ /.


Section contents.
Universe U V.
Context `{Funext} `{Univalence}.
Context (A B : Operations@{U V}).

Context (f : A -> B) `{!IsEquiv f} `{!IsSemiRingPreserving f}.

Lemma iso_same_semirings : A = B.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
A = B
Proof.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
A = B
apply path_sigma_uncurried.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
{p : A.1 = B.1 &
transport
  (fun T : Type =>
   (Plus T * Mult T * Zero T * One T)%type) p A.2 =
B.2}
destruct A as [TA [[[plA mlA] zA] uA]], B as [TB [[[plB mlB] zB] uB]];simpl in *.
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
{p : TA = TB &
transport
  (fun T : Type =>
   (Plus T * Mult T * Zero T * One T)%type) p
  (plA, mlA, zA, uA) = (plB, mlB, zB, uB)}
change plA with (@plus TA plA);change plB with (@plus TB plB);
change mlA with (@mult TA mlA);change mlB with (@mult TB mlB);
change zA with (@zero TA zA);change zB with (@zero TB zB);
change uA with (@one TA uA);change uB with (@one TB uB).
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
{p : TA = TB &
transport
  (fun T : Type =>
   (Plus T * Mult T * Zero T * One T)%type) p
  (plus, mult, 0, 1) = (plus, mult, 0, 1)}
exists (path_universe f).
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
transport
  (fun T : Type =>
   (Plus T * Mult T * Zero T * One T)%type)
  (path_universe f) (plus, mult, 0, 1) =
(plus, mult, 0, 1)
rewrite !transport_prod;simpl.
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
(transport Plus (path_universe f) plus,
transport Mult (path_universe f) mult,
transport Zero (path_universe f) 0,
transport One (path_universe f) 1) =
(plus, mult, 0, 1)
unfold Plus,Mult,Zero,One.
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
(transport (fun A : Type => A -> A -> A)
   (path_universe f) plus,
transport (fun A : Type => A -> A -> A)
  (path_universe f) mult,
transport idmap (path_universe f) 0,
transport idmap (path_universe f) 1) =
(plus, mult, 0, 1)
repeat apply path_prod;simpl;try
( apply path_forall;intros x;rewrite transport_arrow;
  apply path_forall;intros y;rewrite transport_arrow);
rewrite transport_path_universe, ?transport_path_universe_V.
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x + f^-1 y) = x + y
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x * f^-1 y) = x * y
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
f 0 = 0
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
f 1 = 1
-
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x + f^-1 y) = x + y rewrite (preserves_plus (f:=f)).
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x) + f (f^-1 y) = x + y
  apply ap011;apply eisretr.
-
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x * f^-1 y) = x * y rewrite (preserves_mult (f:=f)).
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x) * f (f^-1 y) = x * y
  apply ap011;apply eisretr.
-
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
f 0 = 0 exact preserves_0.
-
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
f 1 = 1 exact preserves_1.
Qed.

Lemma iso_leibnitz : forall P : Operations -> Type, P A -> P B.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
forall P : Operations -> Type, P A -> P B
Proof.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
forall P : Operations -> Type, P A -> P B
intros P;apply transport.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsSemiRingPreserving0: IsSemiRingPreserving f
P: Operations -> Type
A = B
(* Coq pre 8.8 produces phantom universes, see GitHub Coq/Coq#1033. *)
first [exact iso_same_semirings|exact iso_same_semirings@{V V}].
Qed.

End contents.

End SemiRings.

Module Rings.

Class Operations
  := operations : sig (fun T => Plus T * Mult T * Zero T * One T * Negate T)%type.

Definition BuildOperations (T : Type)
  `{Plus T} `{Mult T} `{Zero T} `{One T} `{Negate T}
  : Operations
  := exist _ T (plus,mult,zero,one,negate).

Coercion R_carrier (s : Operations) : Type := s.1.
#[export] Instance R_plus (s : Operations) : Plus s := fst (fst (fst (fst s.2))).
#[export] Instance R_mult (s : Operations) : Mult s := snd (fst (fst (fst s.2))).
#[export] Instance R_zero (s : Operations) : Zero s := snd (fst (fst s.2)).
#[export] Instance R_one (s : Operations) : One s := snd (fst s.2).
#[export] Instance R_negate (s : Operations) : Negate s := snd s.2.

Arguments R_plus !_ / _ _.
Arguments R_mult !_ / _ _.
Arguments R_zero !_ /.
Arguments R_one !_ /.
Arguments R_negate !_ / _.

Section contents.
Universe U V.
Context `{Funext} `{Univalence}.
Context (A B : Operations@{U V}).

(* NB: we need to know they're rings for preserves_negate *)
Context (f : A -> B) `{!IsEquiv f} `{!IsCRing A} `{!IsCRing B} `{!IsSemiRingPreserving f}.

Lemma iso_same_rings : A = B.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsCRing0: IsCRing A
IsCRing1: IsCRing B
IsSemiRingPreserving0: IsSemiRingPreserving f
A = B
Proof.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsCRing0: IsCRing A
IsCRing1: IsCRing B
IsSemiRingPreserving0: IsSemiRingPreserving f
A = B
apply path_sigma_uncurried.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsCRing0: IsCRing A
IsCRing1: IsCRing B
IsSemiRingPreserving0: IsSemiRingPreserving f
{p : A.1 = B.1 &
transport
  (fun T : Type =>
   (Plus T * Mult T * Zero T * One T * Negate T)%type)
  p A.2 = B.2}
destruct A as [TA [[[[plA mlA] zA] uA] nA]],
  B as [TB [[[[plB mlB] zB] uB] nB]];simpl in *.
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
{p : TA = TB &
transport
  (fun T : Type =>
   (Plus T * Mult T * Zero T * One T * Negate T)%type)
  p (plA, mlA, zA, uA, nA) = (plB, mlB, zB, uB, nB)}
change plA with (@plus TA plA);change plB with (@plus TB plB);
change mlA with (@mult TA mlA);change mlB with (@mult TB mlB);
change zA with (@zero TA zA);change zB with (@zero TB zB);
change uA with (@one TA uA);change uB with (@one TB uB);
change nA with (@negate TA nA);change nB with (@negate TB nB).
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
{p : TA = TB &
transport
  (fun T : Type =>
   (Plus T * Mult T * Zero T * One T * Negate T)%type)
  p (plus, mult, 0, 1, negate) =
(plus, mult, 0, 1, negate)}
exists (path_universe f).
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
transport
  (fun T : Type =>
   (Plus T * Mult T * Zero T * One T * Negate T)%type)
  (path_universe f) (plus, mult, 0, 1, negate) =
(plus, mult, 0, 1, negate)
rewrite !transport_prod;simpl.
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
(transport Plus (path_universe f) plus,
transport Mult (path_universe f) mult,
transport Zero (path_universe f) 0,
transport One (path_universe f) 1,
transport Negate (path_universe f) negate) =
(plus, mult, 0, 1, negate)
unfold Plus,Mult,Zero,One,Negate.
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
(transport (fun A : Type => A -> A -> A)
   (path_universe f) plus,
transport (fun A : Type => A -> A -> A)
  (path_universe f) mult,
transport idmap (path_universe f) 0,
transport idmap (path_universe f) 1,
transport (fun A : Type => A -> A) (path_universe f)
  negate) = (plus, mult, 0, 1, negate)
repeat apply path_prod;simpl;try
( apply path_forall;intros x;rewrite transport_arrow;
  try (apply path_forall;intros y;rewrite transport_arrow));
rewrite transport_path_universe, ?transport_path_universe_V.
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x + f^-1 y) = x + y
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x * f^-1 y) = x * y
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
f 0 = 0
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
f 1 = 1
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
x: TB
f (- f^-1 x) = - x
-
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x + f^-1 y) = x + y rewrite (preserves_plus (f:=f)).
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x) + f (f^-1 y) = x + y
  apply ap011;apply eisretr.
-
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x * f^-1 y) = x * y rewrite (preserves_mult (f:=f)).
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
x, y: TB
f (f^-1 x) * f (f^-1 y) = x * y
  apply ap011;apply eisretr.
-
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
f 0 = 0 exact preserves_0.
-
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
f 1 = 1 exact preserves_1.
-
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
x: TB
f (- f^-1 x) = - x rewrite (preserves_negate (f:=f)).
H: Funext
H0: Univalence
A, B: Operations
TA: Type
plA: Plus TA
mlA: Mult TA
zA: Zero TA
uA: One TA
nA: Negate TA
TB: Type
plB: Plus TB
mlB: Mult TB
zB: Zero TB
uB: One TB
nB: Negate TB
f: TA -> TB
IsEquiv0: IsEquiv f
IsCRing0: IsCRing TA
IsCRing1: IsCRing TB
IsSemiRingPreserving0: IsSemiRingPreserving f
x: TB
- f (f^-1 x) = - x
  apply ap,eisretr.
Qed.

Lemma iso_leibnitz : forall P : Operations -> Type, P A -> P B.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsCRing0: IsCRing A
IsCRing1: IsCRing B
IsSemiRingPreserving0: IsSemiRingPreserving f
forall P : Operations -> Type, P A -> P B
Proof.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsCRing0: IsCRing A
IsCRing1: IsCRing B
IsSemiRingPreserving0: IsSemiRingPreserving f
forall P : Operations -> Type, P A -> P B
intros P;apply transport.
H: Funext
H0: Univalence
A, B: Operations
f: A -> B
IsEquiv0: IsEquiv f
IsCRing0: IsCRing A
IsCRing1: IsCRing B
IsSemiRingPreserving0: IsSemiRingPreserving f
P: Operations -> Type
A = B
(* Coq pre 8.8 produces phantom universes, see GitHub Coq/Coq#1033. *)
first [exact iso_same_rings|exact iso_same_rings@{V V}].
Qed.

End contents.

End Rings.