Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import
HoTT.Classes.interfaces.abstract_algebra
HoTT.Classes.theory.dec_fields.ModuleFrac.Sectioncontents.UniverseUR.Context `{Funext} `{Univalence} (R:Type@{UR})
`{IsIntegralDomain R} `{DecidablePaths R}.RecordFrac@{} : Type
:= frac { num: R; den: R; den_ne_0: PropHolds (den <> 0) }.(* We used to have [den] and [den_nonzero] bundled, which did work relatively nicely with Program, but the extra messyness in proofs etc turned out not to be worth it. *)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsHSet Frac
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsHSet Frac
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
{_ : R & {d : R & d <> 0}} <~> Frac
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R E: {_ : R & {d : R & d <> 0}} <~> Frac
IsHSet Frac
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
{_ : R & {d : R & d <> 0}} <~> Frac
issig.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R E: {_ : R & {d : R & d <> 0}} <~> Frac
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Cast R Frac
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Cast R Frac
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: R
Frac
apply (frac x 1 _).Defined.Global InstanceFrac_0@{} : Zero Frac := ('0 : Frac).Global InstanceFrac_1@{} : One Frac := ('1 : Frac).
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Plus Frac
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Plus Frac
intros q r; refine (frac (num q * den r + num r * den q) (den q * den r) _).Defined.Definitionequiv@{} := funxy => num x * den y = num y * den x.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
EquivRel equiv
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
EquivRel equiv
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Reflexive equiv
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Symmetric equiv
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Transitive equiv
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Reflexive equiv
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
equiv x x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
num x * den x = num x * den x
reflexivity.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Symmetric equiv
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: Frac
equiv x y -> equiv y x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: Frac
num x * den y = num y * den x ->
num y * den x = num x * den y
applysymmetry.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Transitive equiv
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac
equiv x y -> equiv y z -> equiv x z
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac
num x * den y = num y * den x ->
num y * den z = num z * den y ->
num x * den z = num z * den x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac E1: num x * den y = num y * den x E2: num y * den z = num z * den y
num x * den z = num z * den x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac E1: num x * den y = num y * den x E2: num y * den z = num z * den y
PropHolds (den y <> 0)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac E1: num x * den y = num y * den x E2: num y * den z = num z * den y
den y * (num x * den z) = den y * (num z * den x)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac E1: num x * den y = num y * den x E2: num y * den z = num z * den y
PropHolds (den y <> 0)
solve_propholds.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac E1: num x * den y = num y * den x E2: num y * den z = num z * den y
den y * (num x * den z) = den y * (num z * den x)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac E1: num x * den y = num y * den x E2: num y * den z = num z * den y
num x * den y * den z = num z * den y * den x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac E1: num x * den y = num y * den x E2: num y * den z = num z * den y
num y * den x * den z = num y * den z * den x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac E1: num x * den y = num y * den x E2: num y * den z = num z * den y
num y * (den x * den z) = num y * (den z * den x)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac E1: num x * den y = num y * den x E2: num y * den z = num z * den y
num y * (den z * den x) = num y * (den z * den x)
reflexivity.Qed.Global Instanceequiv_dec@{} : forallxy: Frac, Decidable (equiv x y)
:= funxy => decide_rel (=) (num x * den y) (num y * den x).
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num (q1 + r1) * den (q2 + r2) =
num (q2 + r2) * den (q1 + r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
(num q1 * den r1 + num r1 * den q1) *
(den q2 * den r2) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q1 * den r1 * (den q2 * den r2) +
num r1 * den q1 * (den q2 * den r2) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q1 * (den r1 * (den q2 * den r2)) +
num r1 * den q1 * (den q2 * den r2) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q1 * (den q2 * (den r1 * den r2)) +
num r1 * den q1 * (den q2 * den r2) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * den q1 * (den r1 * den r2) +
num r1 * den q1 * (den q2 * den r2) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * den q1 * (den r1 * den r2) +
num r1 * (den q1 * den r2 * den q2) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * den q1 * (den r1 * den r2) +
num r1 * den r2 * (den q1 * den q2) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * den q1 * (den r1 * den r2) +
num r2 * den r1 * (den q1 * den q2) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * (den q1 * den r2 * den r1) +
num r2 * den r1 * (den q1 * den q2) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * den r2 * (den q1 * den r1) +
num r2 * den r1 * (den q1 * den q2) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * den r2 * (den q1 * den r1) +
num r2 * (den q2 * (den r1 * den q1)) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * den r2 * (den q1 * den r1) +
num r2 * den q2 * (den q1 * den r1) =
(num q2 * den r2 + num r2 * den q2) *
(den q1 * den r1)
applysymmetry;apply plus_mult_distr_r.Qed.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac, equiv (pl q r) (pl r q)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac, equiv (pl q r) (pl r q)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac
(num q * den r + num r * den q) * (den r * den q) =
(num r * den q + num q * den r) * (den q * den r)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac
(num r * den q + num q * den r) * (den q * den r) =
(num r * den q + num q * den r) * (den q * den r)
reflexivity.Qed.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
(num q * (den r * den t) +
(num r * den t + num t * den r) * den q) *
(den q * den r * den t) =
((num q * den r + num r * den q) * den t +
num t * (den q * den r)) * (den q * (den r * den t))
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num q * (den r * den t) +
(num r * den t + num t * den r) * den q =
(num q * den r + num r * den q) * den t +
num t * (den q * den r)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num q * (den r * den t) +
(num r * den t * den q + num t * den r * den q) =
(num q * den r + num r * den q) * den t +
num t * (den q * den r)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num q * (den r * den t) +
(num r * den t * den q + num t * den r * den q) =
num q * den r * den t + num r * den q * den t +
num t * (den q * den r)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num q * (den r * den t) + num r * den t * den q +
num t * den r * den q =
num q * den r * den t + num r * den q * den t +
num t * (den q * den r)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num q * (den r * den t) = num q * den r * den t
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num r * den t * den q = num r * den q * den t
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num t * den r * den q = num t * (den q * den r)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num q * (den r * den t) = num q * den r * den t
apply associativity.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num r * den t * den q = num r * den q * den t
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num r * (den t * den q) = num r * (den q * den t)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num r * (den q * den t) = num r * (den q * den t)
reflexivity.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num (q1 * r1) * den (q2 * r2) =
num (q2 * r2) * den (q1 * r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q1 * num r1 * (den q2 * den r2) =
num q2 * num r2 * (den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q1 * (num r1 * den q2 * den r2) =
num q2 * num r2 * (den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q1 * den q2 * (num r1 * den r2) =
num q2 * num r2 * (den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * den q1 * (num r2 * den r1) =
num q2 * num r2 * (den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * (num r2 * den q1 * den r1) =
num q2 * num r2 * (den q1 * den r1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q1, q2: Frac Eq: num q1 * den q2 = num q2 * den q1 r1, r2: Frac Er: num r1 * den r2 = num r2 * den r1
num q2 * (num r2 * (den q1 * den r1)) =
num q2 * (num r2 * (den q1 * den r1))
reflexivity.Qed.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Negate Frac
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Negate Frac
intros q;refine (frac (- num q) (den q) _).Defined.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac, equiv q r -> equiv (- q) (- r)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac, equiv q r -> equiv (- q) (- r)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q
- num q * den r = - num r * den q
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q
- (num q * den r) = - (num r * den q)
rewrite E;reflexivity.Qed.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
~ equiv x 0 <-> num x <> 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
~ equiv x 0 <-> num x <> 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac E: ~ equiv x 0 F: num x = 0
equiv x 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac E: num x <> 0 F: equiv x 0
num x = 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac E: ~ equiv x 0 F: num x = 0
equiv x 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac E: ~ equiv x 0 F: num x = 0
num x * den 0 = num 0 * den x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac E: ~ equiv x 0 F: num x = 0
0 * den 0 = num 0 * den x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac E: ~ equiv x 0 F: num x = 0
0 * 1 = 0 * den x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac E: ~ equiv x 0 F: num x = 0
0 = 0
reflexivity.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac E: num x <> 0 F: equiv x 0
num x = 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac E: num x <> 0 F: num x * 1 = 0 * den x
num x = 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac E: num x <> 0 F: num x = 0
num x = 0
trivial.Qed.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
equiv (0 + x) x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
equiv (0 + x) x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
(0 * den x + num x * 1) * den x = num x * (1 * den x)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
num x * den x = num x * den x
reflexivity.Qed.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
equiv (x + 0) x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
equiv (x + 0) x
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
(num x * 1 + 0 * den x) * den x = num x * (den x * 1)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
num x * den x = num x * den x
reflexivity.Qed.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
equiv (- x + x) 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
equiv (- x + x) 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
(- num x * den x + num x * den x) * 1 =
0 * (den x * den x)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
- num x * den x + num x * den x = 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
(- num x + num x) * den x = 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac
0 * den x = 0
apply mult_0_l.Qed.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
equiv (ml q (ml r t)) (ml (ml q r) t)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
equiv (ml q (ml r t)) (ml (ml q r) t)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num q * (num r * num t) * (den q * den r * den t) =
num q * num r * num t * (den q * (den r * den t))
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r, t: Frac
num q * num r * num t * (den q * den r * den t) =
num q * num r * num t * (den q * den r * den t)
reflexivity.Qed.Instancedec_rec@{} : DecRecip Frac := funx =>
match decide_rel (=) (num x) 0with
| inl _ => 0
| inr P => frac (den x) (num x) P
end.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac, equiv q r -> equiv (/ q) (/ r)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac, equiv q r -> equiv (/ q) (/ r)
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q
num
match decide_rel paths (num q) 0with
| inl _ => 0
| inr P =>
{| num := den q; den := num q; den_ne_0 := P |}
end *
den
match decide_rel paths (num r) 0with
| inl _ => 0
| inr P =>
{| num := den r; den := num r; den_ne_0 := P |}
end =
num
match decide_rel paths (num r) 0with
| inl _ => 0
| inr P =>
{| num := den r; den := num r; den_ne_0 := P |}
end *
den
match decide_rel paths (num q) 0with
| inl _ => 0
| inr P =>
{| num := den q; den := num q; den_ne_0 := P |}
end
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q E1: num q = 0 E2: num r = 0
0 * 1 = 0 * 1
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q E1: num q = 0 E2: num r <> 0
0 * num r = den r * 1
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q E1: num q <> 0 E2: num r = 0
den q * 1 = 0 * num q
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q E1: num q <> 0 E2: num r <> 0
den q * num r = den r * num q
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q E1: num q = 0 E2: num r = 0
0 * 1 = 0 * 1
trivial.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q E1: num q = 0 E2: num r <> 0
0 * num r = den r * 1
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: 0 = num r * den q E1: num q = 0 E2: num r <> 0
0 * num r = den r * 1
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: 0 = num r * den q E1: num q = 0
num r = 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: 0 = num r * den q E1: num q = 0
num r * den q = 0 * den q
rewrite mult_0_l;applysymmetry,E.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q E1: num q <> 0 E2: num r = 0
den q * 1 = 0 * num q
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = 0 E1: num q <> 0 E2: num r = 0
den q * 1 = 0 * num q
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = 0 E2: num r = 0
num q = 0
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = 0 E2: num r = 0
num q * den r = 0 * den r
rewrite mult_0_l;trivial.
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q E1: num q <> 0 E2: num r <> 0
den q * num r = den r * num q
H: Funext H0: Univalence R: Type Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac E: num q * den r = num r * den q E1: num q <> 0 E2: num r <> 0
R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H: IsIntegralDomain R1 H0: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H1: IsIntegralDomain R2 H2: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x: Frac R1
Frac R2
R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H: IsIntegralDomain R1 H0: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H1: IsIntegralDomain R2 H2: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x: Frac R1
Frac R2
R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H: IsIntegralDomain R1 H0: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H1: IsIntegralDomain R2 H2: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x: Frac R1
PropHolds (f (den x) <> 0)
R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H: IsIntegralDomain R1 H0: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H1: IsIntegralDomain R2 H2: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x: Frac R1
PropHolds (den x <> 0)
apply (den_ne_0 x).Defined.
R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H: IsIntegralDomain R1 H0: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H1: IsIntegralDomain R2 H2: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H: IsIntegralDomain R1 H0: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H1: IsIntegralDomain R2 H2: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H: IsIntegralDomain R1 H0: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H1: IsIntegralDomain R2 H2: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f q, r: Frac R1 E: num q * den r = num r * den q
f (num q) * f (den r) = f (num r) * f (den q)
R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H: IsIntegralDomain R1 H0: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H1: IsIntegralDomain R2 H2: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f q, r: Frac R1 E: num q * den r = num r * den q
f (num q * den r) = f (num r * den q)
apply ap,E.Qed.Endmorphisms.EndFrac.Import Frac.ModuleFracField.Sectioncontents.(* NB: we need a separate IsHSet instance so we don't need to depend on everything to define F. *)UniverseUR.Context `{Funext} `{Univalence} {R:Type@{UR} } `{IsHSet R} `{IsIntegralDomain R}
`{DecidablePaths R}.Local Existing Instanceden_ne_0.(* Add Ring R: (stdlib_ring_theory R). *)DefinitionF@{} := quotient equiv.Global Instanceclass@{} : Cast (Frac R) F := class_of _.(* injection from R *)Global Instanceinject@{} : Cast R F := Compose class (Frac_inject _).Definitionpath@{} {x y} : equiv x y -> ' x = ' y := related_classes_eq _.DefinitionF_rect@{i} (P : F -> Type@{i}) {sP : forallx, IsHSet (P x)}
(dclass : forallx : Frac R, P (' x))
(dequiv : forallxyE, (path E) # (dclass x) = (dclass y))
: forallq, P q
:= quotient_ind equiv P dclass dequiv.DefinitionF_computeP {sP} dclassdequivx
: @F_rect P sP dclass dequiv (' x) = dclass x := 1.DefinitionF_compute_pathP {sP} dclassdequivqr (E : equiv q r)
: apD (@F_rect P sP dclass dequiv) (path E) = dequiv q r E
:= quotient_ind_compute_path _ _ _ _ _ _ _ _.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> Type sP: forallx : F, IsHProp (P x) dclass: forallx : Frac R, P (' x)
forallx : F, P x
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> Type sP: forallx : F, IsHProp (P x) dclass: forallx : Frac R, P (' x)
forallx : F, P x
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> Type sP: forallx : F, IsHProp (P x) dclass: forallx : Frac R, P (' x)
forall (xy : Frac R) (E : equiv x y),
transport P (path E) (dclass x) = dclass y
intros;apply path_ishprop.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> Type sP: is_mere_relation F P dclass: forallxy : Frac R, P (' x) (' y)
forallxy : F, P x y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> Type sP: is_mere_relation F P dclass: forallxy : Frac R, P (' x) (' y)
forallxy : F, P x y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> Type sP: is_mere_relation F P dclass: forallxy : Frac R, P (' x) (' y)
forallx : F, IsHProp (forally : F, P x y)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> Type sP: is_mere_relation F P dclass: forallxy : Frac R, P (' x) (' y)
forall (x : Frac R) (y : F), P (' x) y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> Type sP: is_mere_relation F P dclass: forallxy : Frac R, P (' x) (' y)
forallx : F, IsHProp (forally : F, P x y)
intros;apply istrunc_forall@{UR i j}.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> Type sP: is_mere_relation F P dclass: forallxy : Frac R, P (' x) (' y)
forall (x : Frac R) (y : F), P (' x) y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> Type sP: is_mere_relation F P dclass: forallxy : Frac R, P (' x) (' y) x: Frac R
forally : F, P (' x) y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> Type sP: is_mere_relation F P dclass: forallxy : Frac R, P (' x) (' y) x, y: Frac R
P (' x) (' y)
apply dclass.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> F -> Type sP: forallxyz : F, IsHProp (P x y z) dclass: forallxyz : Frac R, P (' x) (' y) (' z)
forallxyz : F, P x y z
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> F -> Type sP: forallxyz : F, IsHProp (P x y z) dclass: forallxyz : Frac R, P (' x) (' y) (' z)
forallxyz : F, P x y z
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> F -> Type sP: forallxyz : F, IsHProp (P x y z) dclass: forallxyz : Frac R, P (' x) (' y) (' z)
forallx : F, IsHProp (forallyz : F, P x y z)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> F -> Type sP: forallxyz : F, IsHProp (P x y z) dclass: forallxyz : Frac R, P (' x) (' y) (' z)
forall (x : Frac R) (yz : F), P (' x) y z
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> F -> Type sP: forallxyz : F, IsHProp (P x y z) dclass: forallxyz : Frac R, P (' x) (' y) (' z)
forallx : F, IsHProp (forallyz : F, P x y z)
intros;apply istrunc_forall@{UR j j}.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> F -> Type sP: forallxyz : F, IsHProp (P x y z) dclass: forallxyz : Frac R, P (' x) (' y) (' z)
forall (x : Frac R) (yz : F), P (' x) y z
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> F -> Type sP: forallxyz : F, IsHProp (P x y z) dclass: forallxyz : Frac R, P (' x) (' y) (' z) x: Frac R
forallyz : F, P (' x) y z
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R P: F -> F -> F -> Type sP: forallxyz : F, IsHProp (P x y z) dclass: forallxyz : Frac R, P (' x) (' y) (' z) x: Frac R
forallx0y : Frac R, P (' x) (' x0) (' y)
auto.Qed.DefinitionF_rec@{i} {T : Type@{i} } {sT : IsHSet T}
: forall (dclass : Frac R -> T)
(dequiv : forallxy, equiv x y -> dclass x = dclass y),
F -> T
:= quotient_rec equiv.DefinitionF_rec_computeTsTdclassdequivx
: @F_rec T sT dclass dequiv (' x) = dclass x
:= 1.DefinitionF_rec2@{i j} {T:Type@{i} } {sT : IsHSet T}
: forall (dclass : Frac R -> Frac R -> T)
(dequiv : forallx1x2, equiv x1 x2 -> forally1y2, equiv y1 y2 ->
dclass x1 y1 = dclass x2 y2),
F -> F -> T
:= @quotient_rec2@{UR UR UR j i} _ _ _ _ _ (Build_HSet _).DefinitionF_rec2_compute {TsT} dclassdequivxy
: @F_rec2 T sT dclass dequiv (' x) (' y) = dclass x y
:= 1.(* Relations, operations and constants *)Global InstanceF0@{} : Zero F := ('0 : F).Global InstanceF1@{} : One F := ('1 : F).
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Plus F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Plus F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x1, x2: Frac R X: equiv x1 x2 y1, y2: Frac R X0: equiv y1 y2
' pl R x1 y1 = ' pl R x2 y2
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x1, x2: Frac R X: equiv x1 x2 y1, y2: Frac R X0: equiv y1 y2
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Negate F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Negate F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallxy : Frac R,
equiv x y -> ' neg R x = ' neg R y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: Frac R X: equiv x y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Mult F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Mult F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx1x2 : Frac R,
equiv x1 x2 ->
forally1y2 : Frac R,
equiv y1 y2 -> ' ml R x1 y1 = ' ml R x2 y2
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x1, x2: Frac R X: equiv x1 x2 y1, y2: Frac R X0: equiv y1 y2
' ml R x1 y1 = ' ml R x2 y2
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x1, x2: Frac R X: equiv x1 x2 y1, y2: Frac R X0: equiv y1 y2
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Commutative Fplus
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Commutative Fplus
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallxy : F, Fplus x y = Fplus y x
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsCRing F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsCRing F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsHSet F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Associative plus
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
LeftIdentity plus 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
RightIdentity plus 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
LeftInverse plus negate 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
RightInverse plus negate 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Commutative plus
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsHSet F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Associative mult
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
LeftIdentity mult 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
RightIdentity mult 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Commutative mult
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
LeftDistribute mult plus
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsHSet F
apply _.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Associative plus
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallxyz : F, x + (y + z) = x + y + z
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallxyz : Frac R,
' x + (' y + ' z) = ' x + ' y + ' z
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y, z: Frac R
equiv (pl R x (pl R y z)) (pl R (pl R x y) z)
apply Frac.pl_assoc.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
LeftIdentity plus 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forally : F, 0 + y = y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : Frac R, 0 + ' x = ' x
intros;apply path, Frac.pl_0_l.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
RightIdentity plus 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : F, x + 0 = x
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : Frac R, ' x + 0 = ' x
intros;apply path, Frac.pl_0_r.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
LeftInverse plus negate 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : F, - x + x = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : Frac R, - ' x + ' x = 0
intros;apply path, Frac.pl_neg_l.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
RightInverse plus negate 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: F
x - x = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: F
- x + x = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : Frac R, - ' x + ' x = 0
intros;apply path, Frac.pl_neg_l.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Commutative plus
apply _.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsHSet F
apply _.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Associative mult
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallxyz : Frac R,
' x * (' y * ' z) = ' x * ' y * ' z
intros;apply path, Frac.ml_assoc.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
LeftIdentity mult 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forally : F, 1 * y = y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : Frac R, 1 * ' x = ' x
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac R
equiv (ml R (Frac_inject R 1) x) x
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac R
1 * num x * den x = num x * (1 * den x)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac R
num x * den x = num x * den x
reflexivity.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
RightIdentity mult 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : F, x * 1 = x
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : Frac R, ' x * 1 = ' x
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac R
equiv (ml R x (Frac_inject R 1)) x
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac R
num x * 1 * den x = num x * (den x * 1)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac R
num x * den x = num x * den x
reflexivity.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Commutative mult
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallxy : Frac R, ' x * ' y = ' y * ' x
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: Frac R
equiv (ml R x y) (ml R y x)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: Frac R
num x * num y * (den y * den x) =
num y * num x * (den x * den y)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: Frac R
num x * num y * (den x * den y) =
num x * num y * (den x * den y)
reflexivity.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
LeftDistribute mult plus
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallabc : F, a * (b + c) = a * b + a * c
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallxyz : Frac R,
' x * (' y + ' z) = ' x * ' y + ' x * ' z
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
equiv (ml R a (pl R b c)) (pl R (ml R a b) (ml R a c))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
num a * (num b * den c + num c * den b) *
(den a * den b * (den a * den c)) =
(num a * num b * (den a * den c) +
num a * num c * (den a * den b)) *
(den a * (den b * den c))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
num a *
((num b * den c + num c * den b) *
(den a * den b * (den a * den c))) =
(num a * (num b * (den a * den c)) +
num a * (num c * (den a * den b))) *
(den a * (den b * den c))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
num a *
((num b * den c + num c * den b) *
(den a * den b * (den a * den c))) =
num a *
(num b * (den a * den c) + num c * (den a * den b)) *
(den a * (den b * den c))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
num a *
((num b * den c + num c * den b) *
(den a * den b * (den a * den c))) =
num a *
((num b * (den a * den c) + num c * (den a * den b)) *
(den a * (den b * den c)))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
(num b * den c + num c * den b) *
(den a * den b * (den a * den c)) =
(num b * (den a * den c) + num c * (den a * den b)) *
(den a * (den b * den c))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
(num b * den c + num c * den b) *
(den b * den a * (den c * den a)) =
(num b * (den c * den a) + num c * (den b * den a)) *
(den a * (den b * den c))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
(num b * den c + num c * den b) *
(den b * den a * (den c * den a)) =
(num b * den c * den a + num c * den b * den a) *
(den a * (den b * den c))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
(num b * den c + num c * den b) *
(den b * den a * (den c * den a)) =
(num b * den c + num c * den b) * den a *
(den a * (den b * den c))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
(num b * den c + num c * den b) *
(den b * den a * (den c * den a)) =
(num b * den c + num c * den b) *
(den a * (den a * (den b * den c)))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
den b * den a * (den c * den a) =
den a * (den a * (den b * den c))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
den a * (den b * (den c * den a)) =
den a * (den a * (den b * den c))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
den b * (den c * den a) = den a * (den b * den c)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R a, b, c: Frac R
den b * (den c * den a) = den b * den c * den a
apply associativity.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
DecRecip F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
DecRecip F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallxy : Frac R,
equiv x y -> ' dec_rec R x = ' dec_rec R y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: Frac R X: equiv x y
' dec_rec R x = ' dec_rec R y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: Frac R X: equiv x y
equiv (dec_rec R x) (dec_rec R y)
apply Frac.dec_recip_respect;trivial.Defined.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac R, ' q = ' r -> equiv q r
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac R, ' q = ' r -> equiv q r
apply classes_eq_related@{UR UR Ularge UR Ularge};apply _.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac R, ~ equiv q r -> ' q <> ' r
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac R, ~ equiv q r -> ' q <> ' r
intros q r E1 E2;apply E1;apply classes_eq_related, E2.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac R, ' q <> ' r -> ~ equiv q r
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac R, ' q <> ' r -> ~ equiv q r
intros q r E1 E2;apply E1,path,E2.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
/ 0 = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
/ 0 = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
Fdec_rec 0 = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
' dec_rec R (Frac_inject R 0) = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
' match decide_rel paths 00with
| inl _ => 0
| inr P => {| num := 1; den := 0; den_ne_0 := P |}
end = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
' 0 = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R E: 0 <> 0
' {| num := 1; den := 0; den_ne_0 := E |} = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
' 0 = 0
reflexivity.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R E: 0 <> 0
' {| num := 1; den := 0; den_ne_0 := E |} = 0
destruct E;reflexivity.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallq : Frac R, ' q <> 0 -> num q <> 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallq : Frac R, ' q <> 0 -> num q <> 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: ~ equiv q (Frac_inject R 0)
num q <> 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: num q <> 0
num q <> 0
trivial.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forall (q : Frac R) (E : ' q <> 0),
/ ' q =
' {|
num := den q;
den := num q;
den_ne_0 := dec_recip_nonzero_aux q E
|}
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forall (q : Frac R) (E : ' q <> 0),
/ ' q =
' {|
num := den q;
den := num q;
den_ne_0 := dec_recip_nonzero_aux q E
|}
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: ' q <> 0
/ ' q =
' {|
num := den q;
den := num q;
den_ne_0 := dec_recip_nonzero_aux q E
|}
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: ' q <> 0
equiv (dec_rec R q)
{|
num := den q;
den := num q;
den_ne_0 := dec_recip_nonzero_aux q E
|}
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: ' q <> 0
num (dec_rec R q) * num q = den q * den (dec_rec R q)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: ' q <> 0
num
match decide_rel paths (num q) 0with
| inl _ => 0
| inr P =>
{| num := den q; den := num q; den_ne_0 := P |}
end * num q =
den q *
den
match decide_rel paths (num q) 0with
| inl _ => 0
| inr P =>
{| num := den q; den := num q; den_ne_0 := P |}
end
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: num q <> 0
num
match decide_rel paths (num q) 0with
| inl _ => 0
| inr P =>
{| num := den q; den := num q; den_ne_0 := P |}
end * num q =
den q *
den
match decide_rel paths (num q) 0with
| inl _ => 0
| inr P =>
{| num := den q; den := num q; den_ne_0 := P |}
end
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E, n: num q <> 0
num {| num := den q; den := num q; den_ne_0 := n |} *
num q =
den q *
den {| num := den q; den := num q; den_ne_0 := n |}
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E, n: num q <> 0
den q * num q = den q * num q
reflexivity.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsDecField F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsDecField F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
PropHolds (1 <> 0)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
/ 0 = 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : F, x <> 0 -> x / x = 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
PropHolds (1 <> 0)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
1 <> 0
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
~ equiv (Frac_inject R 1) (Frac_inject R 0)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
1 * 1 <> 0 * 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
1 <> 0
solve_propholds.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
/ 0 = 0
apply dec_recip_0.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : F, x <> 0 -> x / x = 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallx : Frac R, ' x <> 0 -> ' x / ' x = 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac R E: ' x <> 0
' x / ' x = 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac R E: ' x <> 0
' x *
' {|
num := den x;
den := num x;
den_ne_0 := dec_recip_nonzero_aux x E
|} = 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac R E: ' x <> 0
num x * den x * 1 = 1 * (den x * num x)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x: Frac R E: ' x <> 0
num x * den x = den x * num x
apply mult_comm.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac R, Decidable (class q = class r)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallqr : Frac R, Decidable (class q = class r)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac R
Decidable (class q = class r)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac R E: equiv q r
Decidable (class q = class r)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac R E: ~ equiv q r
Decidable (class q = class r)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac R E: equiv q r
Decidable (class q = class r)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac R E: equiv q r
class q = class r
apply path,E.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac R E: ~ equiv q r
Decidable (class q = class r)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac R E: ~ equiv q r
class q <> class r
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac R E: ~ equiv q r E': class q = class r
Empty
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q, r: Frac R E: ~ equiv q r E': class q = class r
equiv q r
apply (classes_eq_related _ _ E').Defined.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
DecidablePaths F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
DecidablePaths F
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallxy : F, Decidable (x = y)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
forallxy : Frac R, Decidable (' x = ' y)
apply dec_class.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
' q = ' num q / ' den q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
' q = ' num q / ' den q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
equiv q
(ml R (Frac_inject R (num q))
(dec_rec R (Frac_inject R (den q))))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
num q *
den
(ml R (Frac_inject R (num q))
(dec_rec R (Frac_inject R (den q)))) =
num
(ml R (Frac_inject R (num q))
(dec_rec R (Frac_inject R (den q)))) * den q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
num q * (1 * den (dec_rec R (Frac_inject R (den q)))) =
num q * num (dec_rec R (Frac_inject R (den q))) *
den q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
num q * den (dec_rec R (Frac_inject R (den q))) =
num q * num (dec_rec R (Frac_inject R (den q))) *
den q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
num q *
den
match
decide_rel paths (num (Frac_inject R (den q))) 0with
| inl _ => 0
| inr P =>
{|
num := den (Frac_inject R (den q));
den := num (Frac_inject R (den q));
den_ne_0 := P
|}
end =
num q *
num
match
decide_rel paths (num (Frac_inject R (den q))) 0with
| inl _ => 0
| inr P =>
{|
num := den (Frac_inject R (den q));
den := num (Frac_inject R (den q));
den_ne_0 := P
|}
end * den q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
num q *
den
match decide_rel paths (den q) 0with
| inl _ => 0
| inr P =>
{| num := 1; den := den q; den_ne_0 := P |}
end =
num q *
num
match decide_rel paths (den q) 0with
| inl _ => 0
| inr P =>
{| num := 1; den := den q; den_ne_0 := P |}
end * den q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: den q = 0
num q * 1 = num q * 0 * den q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: den q <> 0
num q * den q = num q * 1 * den q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: den q = 0
num q * 1 = num q * 0 * den q
destruct (den_ne_0 q E).
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: den q <> 0
num q * den q = num q * 1 * den q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: den q <> 0
num q * den q = num q * den q
reflexivity.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
/ ' q = ' den q / ' num q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
/ ' q = ' den q / ' num q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
num (dec_rec R q) *
(1 * den (dec_rec R (Frac_inject R (num q)))) =
den q * num (dec_rec R (Frac_inject R (num q))) *
den (dec_rec R q)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R
num
match decide_rel paths (num q) 0with
| inl _ => 0
| inr P =>
{| num := den q; den := num q; den_ne_0 := P |}
end *
(1 *
den
match decide_rel paths (num q) 0with
| inl _ => 0
| inr P =>
{| num := 1; den := num q; den_ne_0 := P |}
end) =
den q *
num
match decide_rel paths (num q) 0with
| inl _ => 0
| inr P =>
{| num := 1; den := num q; den_ne_0 := P |}
end *
den
match decide_rel paths (num q) 0with
| inl _ => 0
| inr P =>
{| num := den q; den := num q; den_ne_0 := P |}
end
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: num q = 0
0 * (1 * 1) = den q * 0 * 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: num q <> 0
den q * (1 * num q) = den q * 1 * num q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: num q = 0
0 * (1 * 1) = den q * 0 * 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: num q = 0
0 = 0
reflexivity.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: num q <> 0
den q * (1 * num q) = den q * 1 * num q
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R q: Frac R E: num q <> 0
den q * num q = den q * num q
reflexivity.Qed.(* A final word about inject *)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsSemiRingPreserving (cast R F)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsSemiRingPreserving (cast R F)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsSemiGroupPreserving (cast R F)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsSemiGroupPreserving (cast R F)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsSemiGroupPreserving (cast R F)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R
' sg_op x y = sg_op (' x) (' y)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R
equiv (Frac_inject R (sg_op x y))
(pl R (Frac_inject R x) (Frac_inject R y))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R
(x + y) * (1 * 1) = (x * 1 + y * 1) * 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R
x + y = x + y
reflexivity.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsSemiGroupPreserving (cast R F)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R
' sg_op x y = sg_op (' x) (' y)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R
equiv (Frac_inject R (sg_op x y))
(ml R (Frac_inject R x) (Frac_inject R y))
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R
x * y * (1 * 1) = x * y * 1
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R
x * y = x * y
reflexivity.Qed.
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsInjective (cast R F)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsInjective (cast R F)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R
IsInjective (cast R F)
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R E: ' x = ' y
x = y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R E: equiv (Frac_inject R x) (Frac_inject R y)
x = y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R E: num (Frac_inject R x) * den (Frac_inject R y) =
num (Frac_inject R y) * den (Frac_inject R x)
x = y
H: Funext H0: Univalence R: Type IsHSet0: IsHSet R Aplus: Plus R Amult: Mult R Azero: Zero R Aone: One R Anegate: Negate R H1: IsIntegralDomain R H2: DecidablePaths R x, y: R E: x * 1 = y * 1
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
F R1 -> F R2
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
F R1 -> F R2
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
forallxy : Frac R1,
equiv x y -> class (lift f x) = class (lift f y)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
IsSemiRingPreserving lift
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
IsSemiRingPreserving lift
(* This takes a few seconds. *)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
forallxy : F R1,
lift (sg_op x y) = sg_op (lift x) (lift y)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
lift mon_unit = mon_unit
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
forallxy : F R1,
lift (sg_op x y) = sg_op (lift x) (lift y)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
lift mon_unit = mon_unit
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
forallxy : F R1,
lift (sg_op x y) = sg_op (lift x) (lift y)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1
class (Frac.lift f (pl R1 x y)) =
sg_op (class (Frac.lift f x)) (class (Frac.lift f y))
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1
equiv (Frac.lift f (pl R1 x y))
(pl R2 (Frac.lift f x) (Frac.lift f y))
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1
f (num x * den y + num y * den x) *
(f (den x) * f (den y)) =
(f (num x) * f (den y) + f (num y) * f (den x)) *
f (den x * den y)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1
f ((num x * den y + num y * den x) * (den x * den y)) =
f ((num x * den y + num y * den x) * (den x * den y))
reflexivity.
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
lift mon_unit = mon_unit
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
class (Frac.lift f (Frac_inject R1 0)) = mon_unit
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
equiv (Frac.lift f (Frac_inject R1 0))
(Frac_inject R2 0)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
f 0 * 1 = 0 * f 1
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
0 * 1 = 0 * f 1
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
0 = 0
reflexivity.
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
forallxy : F R1,
lift (sg_op x y) = sg_op (lift x) (lift y)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1
class (Frac.lift f (ml R1 x y)) =
sg_op (class (Frac.lift f x)) (class (Frac.lift f y))
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1
equiv (Frac.lift f (ml R1 x y))
(ml R2 (Frac.lift f x) (Frac.lift f y))
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1
f (num x * num y) * (f (den x) * f (den y)) =
f (num x) * f (num y) * f (den x * den y)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1
f (num x * num y * (den x * den y)) =
f (num x * num y * (den x * den y))
reflexivity.
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
lift mon_unit = mon_unit
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
class (Frac.lift f (Frac_inject R1 1)) = mon_unit
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
equiv (Frac.lift f (Frac_inject R1 1))
(Frac_inject R2 1)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
f 1 * 1 = 1 * f 1
apply commutativity.Qed.
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
IsInjective lift
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
IsInjective lift
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
forallxy : F R1, lift x = lift y -> x = y
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f
forallxy : Frac R1,
lift (' x) = lift (' y) -> ' x = ' y
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1 E: lift (' x) = lift (' y)
' x = ' y
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1 E: class (Frac.lift f x) = class (Frac.lift f y)
' x = ' y
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1 E: equiv (Frac.lift f x) (Frac.lift f y)
' x = ' y
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1 E: f (num x) * f (den y) = f (num y) * f (den x)
' x = ' y
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1 E: f (num x) * f (den y) = f (num y) * f (den x)
equiv x y
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1 E: f (num x) * f (den y) = f (num y) * f (den x)
num x * den y = num y * den x
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1 E: f (num x) * f (den y) = f (num y) * f (den x)
f (num x * den y) = f (num y * den x)
H: Funext H0: Univalence R1: Type Aplus: Plus R1 Amult: Mult R1 Azero: Zero R1 Aone: One R1 Anegate: Negate R1 H1: IsIntegralDomain R1 H2: DecidablePaths R1 R2: Type Aplus0: Plus R2 Amult0: Mult R2 Azero0: Zero R2 Aone0: One R2 Anegate0: Negate R2 H3: IsIntegralDomain R2 H4: DecidablePaths R2 f: R1 -> R2 IsSemiRingPreserving0: IsSemiRingPreserving f IsInjective0: IsInjective f x, y: Frac R1 E: f (num x) * f (den y) = f (num y) * f (den x)