Library UniMath.Algebra.BinaryOperations
Algebra 1. Part A. Generalities. Vladimir Voevodsky. Aug. 2011 -.
Contents
- Sets with one and two binary operations
- Unary operations
- Binary operations
- General definitions
- Standard conditions on one binary operation on a set
- Elements with inverses
- Group operations
- Standard conditions on a pair of binary operations on a set
- Sets with one binary operation
- General definitions
- Functions compatible with a binary operation (homomorphism) and their properties
- Transport of properties of a binary operation
- Subobject
- Relations compatible with a binary operation and quotient objects
- Relations inversely compatible with a binary operation
- Homomorphisms and relations
- Quotient relations
- Direct products
- Sets with two binary operations
- General definitions
- Functions compatible with a pair of binary operation (homomorphisms) and their properties
- Transport of properties of a pair of binary operations
- Subobjects
- Quotient objects
- Direct products
- Infinitary operations
Preamble
Require Export UniMath.Foundations.Sets.
Require Export UniMath.MoreFoundations.Propositions.
Local Open Scope logic.
Definition islcancelable {X : UU} (opp : binop X) (x : X) : UU := isincl (λ x0 : X, opp x x0).
Definition lcancel {X : UU} {opp : binop X} {x : X} (H_x : islcancelable opp x) (y z : X) :
opp x y = opp x z -> y = z.
Show proof.
Definition isrcancelable {X : UU} (opp : binop X) (x : X) : UU := isincl (λ x0 : X, opp x0 x).
Definition rcancel {X : UU} {opp : binop X} {x : X} (H_x : isrcancelable opp x) (y z : X) :
opp y x = opp z x -> y = z.
Show proof.
Definition iscancelable {X : UU} (opp : binop X) (x : X) : UU :=
(islcancelable opp x) × (isrcancelable opp x).
Definition islinvertible {X : UU} (opp : binop X) (x : X) : UU := isweq (λ x0 : X, opp x x0).
Definition isrinvertible {X : UU} (opp : binop X) (x : X) : UU := isweq (λ x0 : X, opp x0 x).
Definition isinvertible {X : UU} (opp : binop X) (x : X) : UU :=
(islinvertible opp x) × (isrinvertible opp x).
Definition binop_weq_fwd {X Y : UU} (H : X ≃ Y) :
binop X → binop Y :=
λ (opp : binop X) (x y : Y), H (opp (invmap H x) (invmap H y)).
Definition binop_weq_bck {X Y : UU} (H : X ≃ Y) :
binop Y → binop X :=
λ (opp : binop Y) (x y : X), invmap H (opp (H x) (H y)).
Definition isassoc {X : UU} (opp : binop X) : UU :=
∏ x x' x'', paths (opp (opp x x') x'') (opp x (opp x' x'')).
Lemma isapropisassoc {X : hSet} (opp : binop X) : isaprop (isassoc opp).
Show proof.
apply impred. intro x.
apply impred. intro x'.
apply impred. intro x''.
simpl. apply (setproperty X).
apply impred. intro x'.
apply impred. intro x''.
simpl. apply (setproperty X).
Compare to CategoryTheory.Categories.assoc4
Lemma assoc4 {X : UU} (opp : binop X) (isa : isassoc opp) :
∏ w x y z : X, opp (opp (opp w x) y) z = opp (opp w (opp x y)) z.
Show proof.
∏ w x y z : X, opp (opp (opp w x) y) z = opp (opp w (opp x y)) z.
Show proof.
cancellativity
Definition isrcancellative {X : UU} (opp : binop X) : UU :=
∏ x:X, isrcancelable opp x.
Definition islcancellative {X : UU} (opp : binop X) : UU :=
∏ x:X, islcancelable opp x.
Definition islunit {X : UU} (opp : binop X) (un0 : X) : UU := ∏ x : X, (opp un0 x) = x.
Lemma isapropislunit {X : hSet} (opp : binop X) (un0 : X) : isaprop (islunit opp un0).
Show proof.
Definition isrunit {X : UU} (opp : binop X) (un0 : X) : UU := ∏ x : X, (opp x un0) = x.
Lemma isapropisrunit {X : hSet} (opp : binop X) (un0 : X) : isaprop (isrunit opp un0).
Show proof.
Definition isunit {X : UU} (opp : binop X) (un0 : X) : UU :=
(islunit opp un0) × (isrunit opp un0).
Definition make_isunit {X : UU} {opp : binop X} {un0 : X} (H1 : islunit opp un0)
(H2 : isrunit opp un0) : isunit opp un0 := make_dirprod H1 H2.
Definition isunital {X : UU} (opp : binop X) : UU := total2 (λ un0 : X, isunit opp un0).
Definition make_isunital {X : UU} {opp : binop X} (un0 : X) (is : isunit opp un0) :
isunital opp := tpair _ un0 is.
Lemma isapropisunital {X : hSet} (opp : binop X) : isaprop (isunital opp).
Show proof.
apply (@isapropsubtype X (λ un0 : _, hconj (make_hProp _ (isapropislunit opp un0))
(make_hProp _ (isapropisrunit opp un0)))).
intros u1 u2. intros ua1 ua2.
apply (pathscomp0 (pathsinv0 (pr2 ua2 u1)) (pr1 ua1 u2)).
(make_hProp _ (isapropisrunit opp un0)))).
intros u1 u2. intros ua1 ua2.
apply (pathscomp0 (pathsinv0 (pr2 ua2 u1)) (pr1 ua1 u2)).
Definition ismonoidop {X : UU} (opp : binop X) : UU := (isassoc opp) × (isunital opp).
Definition make_ismonoidop {X : UU} {opp : binop X} (H1 : isassoc opp) (H2 : isunital opp) :
ismonoidop opp := make_dirprod H1 H2.
Definition assocax_is {X : UU} {opp : binop X} : ismonoidop opp -> isassoc opp := @pr1 _ _.
Definition unel_is {X : UU} {opp : binop X} (is : ismonoidop opp) : X := pr1 (pr2 is).
Definition lunax_is {X : UU} {opp : binop X} (is : ismonoidop opp) :
islunit opp (pr1 (pr2 is)) := pr1 (pr2 (pr2 is)).
Definition runax_is {X : UU} {opp : binop X} (is : ismonoidop opp) :
isrunit opp (pr1 (pr2 is)) := pr2 (pr2 (pr2 is)).
Definition unax_is {X : UU} {opp : binop X} (is : ismonoidop opp) :
isunit opp (pr1 (pr2 is)) := make_dirprod (lunax_is is) (runax_is is).
Lemma isapropismonoidop {X : hSet} (opp : binop X) : isaprop (ismonoidop opp).
Show proof.
***** Elements with inverses
Section ElementsWithInverses.
Context {X : UU} (opp : binop X) (is : ismonoidop opp).
Local Notation "x * y" := (opp x y).
Local Notation u := (unel_is is).
Is this element x0 the left/right inverse of x?
Definition islinvel (x : X) : X -> UU := fun x0 => paths (x0 * x) u.
Definition isrinvel (x : X) : X -> UU := fun x0 => paths (x * x0) u.
Definition isinvel (x : X) : X -> UU := fun x0 => (islinvel x x0) × (isrinvel x x0).
Is there some element x0 that is the left/right inverse of x?
Definition haslinv (x : X) : UU := ∑ x0 : X, islinvel x x0.
Definition hasrinv (x : X) : UU := ∑ x0 : X, isrinvel x x0.
Definition hasinv (x : X) : UU := ∑ x0 : X, isinvel x x0.
Accessor functions
Definition haslinv_to_linvel {x : X} : haslinv x → X := pr1.
Definition hasrinv_to_rinvel {x : X} : hasrinv x → X := pr1.
Definition hasinv_to_invel {x : X} : hasinv x → X := pr1.
Definition merely_haslinv (x : X) : hProp := ∥ haslinv x ∥.
Definition merely_hasrinv (x : X) : hProp := ∥ hasrinv x ∥.
Definition merely_hasinv (x : X) : hProp := ∥ hasinv x ∥.
Definition hasrinv_to_rinvel {x : X} : hasrinv x → X := pr1.
Definition hasinv_to_invel {x : X} : hasinv x → X := pr1.
Definition merely_haslinv (x : X) : hProp := ∥ haslinv x ∥.
Definition merely_hasrinv (x : X) : hProp := ∥ hasrinv x ∥.
Definition merely_hasinv (x : X) : hProp := ∥ hasinv x ∥.
Lemmas for elements with inverses
The inverse of an element's two-sided inverse is just that element
Definition is_inv_inv : ∏ (x x0 : X), (isinvel x x0 -> isinvel x0 x) :=
fun x x0 isinv => (make_dirprod (pr2 isinv) (pr1 isinv)).
fun x x0 isinv => (make_dirprod (pr2 isinv) (pr1 isinv)).
If two elements have left inverses, so does their product.
Lemma invop_l :
∏ (x y x' y' : X),
(islinvel x x' -> islinvel y y' -> islinvel (x * y) (y' * x')).
Show proof.
∏ (x y x' y' : X),
(islinvel x x' -> islinvel y y' -> islinvel (x * y) (y' * x')).
Show proof.
intros x y x' y' xinv yinv.
unfold islinvel.
pose (assoc := pr1 is).
cbn; unfold islinvel.
rewrite <- assoc.
rewrite (assoc4 opp assoc), xinv.
rewrite (runax_is is).
exact yinv.
unfold islinvel.
pose (assoc := pr1 is).
cbn; unfold islinvel.
rewrite <- assoc.
rewrite (assoc4 opp assoc), xinv.
rewrite (runax_is is).
exact yinv.
If two elements have right inverses, so does their product.
Lemma invop_r :
∏ (x y x' y' : X),
(isrinvel x x' -> isrinvel y y' -> isrinvel (x * y) (y' * x')).
Show proof.
∏ (x y x' y' : X),
(isrinvel x x' -> isrinvel y y' -> isrinvel (x * y) (y' * x')).
Show proof.
intros x y x' y' xinv yinv.
pose (assoc := pr1 is).
cbn; unfold isrinvel.
rewrite <- assoc.
rewrite (assoc4 opp assoc), yinv.
rewrite (runax_is is).
exact xinv.
pose (assoc := pr1 is).
cbn; unfold isrinvel.
rewrite <- assoc.
rewrite (assoc4 opp assoc), yinv.
rewrite (runax_is is).
exact xinv.
This is a similar statement to grinvop
Lemma invop :
∏ (x y x' y' : X),
(isinvel x x' -> isinvel y y' -> isinvel (x * y) (y' * x')).
Show proof.
Lemma mere_invop :
∏ (x y : X), (merely_hasinv x -> merely_hasinv y -> merely_hasinv (x * y)).
Show proof.
∏ (x y x' y' : X),
(isinvel x x' -> isinvel y y' -> isinvel (x * y) (y' * x')).
Show proof.
intros x y x' y' xinv yinv.
use make_dirprod.
- apply invop_l.
+ exact (dirprod_pr1 xinv).
+ exact (dirprod_pr1 yinv).
- apply invop_r.
+ exact (dirprod_pr2 xinv).
+ exact (dirprod_pr2 yinv).
use make_dirprod.
- apply invop_l.
+ exact (dirprod_pr1 xinv).
+ exact (dirprod_pr1 yinv).
- apply invop_r.
+ exact (dirprod_pr2 xinv).
+ exact (dirprod_pr2 yinv).
Lemma mere_invop :
∏ (x y : X), (merely_hasinv x -> merely_hasinv y -> merely_hasinv (x * y)).
Show proof.
intros x y.
apply hinhfun2.
intros xinv yinv.
exists ((hasinv_to_invel yinv) * (hasinv_to_invel xinv)).
apply invop.
- exact (pr2 xinv).
- exact (pr2 yinv).
apply hinhfun2.
intros xinv yinv.
exists ((hasinv_to_invel yinv) * (hasinv_to_invel xinv)).
apply invop.
- exact (pr2 xinv).
- exact (pr2 yinv).
If an element has both left and right inverses, they're equal.
Lemma linv_eq_rinv (x lx rx : X) (lxlinv : islinvel x lx) (rxrinv : isrinvel x rx) :
lx = rx.
Show proof.
End ElementsWithInverses.
Section InverseOperations.
Context {X : UU} (opp : binop X) (u : X) (inv : X -> X).
Local Notation "x * y" := (opp x y).
Definition islinv : UU := ∏ x : X, ((inv x) * x) = u.
Definition isrinv : UU := ∏ x : X, (x * (inv x)) = u.
Definition isinv : UU := islinv × isrinv.
End InverseOperations.
Section ElementsWithInversesSet.
lx = rx.
Show proof.
intros.
refine (!runax_is is _ @ _).
refine (!maponpaths (λ z, lx * z) rxrinv @ _).
refine (!assocax_is is _ _ _ @ _).
refine (maponpaths (λ z, z * rx) lxlinv @ _).
apply lunax_is.
refine (!runax_is is _ @ _).
refine (!maponpaths (λ z, lx * z) rxrinv @ _).
refine (!assocax_is is _ _ _ @ _).
refine (maponpaths (λ z, z * rx) lxlinv @ _).
apply lunax_is.
End ElementsWithInverses.
Section InverseOperations.
Context {X : UU} (opp : binop X) (u : X) (inv : X -> X).
Local Notation "x * y" := (opp x y).
Definition islinv : UU := ∏ x : X, ((inv x) * x) = u.
Definition isrinv : UU := ∏ x : X, (x * (inv x)) = u.
Definition isinv : UU := islinv × isrinv.
End InverseOperations.
Section ElementsWithInversesSet.
When working with an hSet instead of a general type, many of the above
statements become propositions
Context {X : hSet} (opp : binop X) (is : ismonoidop opp).
Local Notation "x * y" := (opp x y).
Definition isapropislinvel (x x0 : X) : isaprop (islinvel opp is x x0) := setproperty X _ _.
Definition isapropisrinvel (x x0 : X) : isaprop (isrinvel opp is x x0) := setproperty X _ _.
Definition isapropisinvel (x x0 : X) : isaprop (isinvel opp is x x0) := isapropdirprod _ _ (isapropislinvel _ _) (isapropisrinvel _ _).
If the operation is left cancellable, right inverses are unique.
Definition isaprop_haslinv (x : X) (can : islcancelable opp x) :
isaprop (hasrinv opp is x).
Show proof.
isaprop (hasrinv opp is x).
Show proof.
apply isaproptotal2.
- intro; apply isapropislinvel.
- intros x' x'' islinvx' islinvx''.
apply (Injectivity (λ x0 : X, x * x0)).
+ apply incl_injectivity; assumption.
+ exact (islinvx' @ !islinvx'').
- intro; apply isapropislinvel.
- intros x' x'' islinvx' islinvx''.
apply (Injectivity (λ x0 : X, x * x0)).
+ apply incl_injectivity; assumption.
+ exact (islinvx' @ !islinvx'').
If the operation is right cancellable, left inverses are unique.
Definition isaprop_hasrinv (x : X) (can : isrcancelable opp x) :
isaprop (haslinv opp is x).
Show proof.
isaprop (haslinv opp is x).
Show proof.
apply isaproptotal2.
- intro; apply isapropisrinvel.
- intros x' x'' isrinvx' isrinvx''.
apply (Injectivity (λ x0 : X, x0 * x)).
+ apply incl_injectivity; assumption.
+ exact (isrinvx' @ !isrinvx'').
- intro; apply isapropisrinvel.
- intros x' x'' isrinvx' isrinvx''.
apply (Injectivity (λ x0 : X, x0 * x)).
+ apply incl_injectivity; assumption.
+ exact (isrinvx' @ !isrinvx'').
For the two-sided case, we can just reuse the argument from the
left-cancellable case.
Definition isaprop_hasinv (x : X) (can : iscancelable opp x) :
isaprop (hasinv opp is x).
Show proof.
isaprop (hasinv opp is x).
Show proof.
apply isaproptotal2.
- intro; apply isapropdirprod.
+ apply isapropislinvel.
+ apply isapropisrinvel.
- intros x' x'' isinvx' isinvx''.
apply (Injectivity (λ x0 : X, x * x0)).
+ apply incl_injectivity; apply (pr1 can).
+ exact (pr2 isinvx' @ !pr2 isinvx'').
- intro; apply isapropdirprod.
+ apply isapropislinvel.
+ apply isapropisrinvel.
- intros x' x'' isinvx' isinvx''.
apply (Injectivity (λ x0 : X, x * x0)).
+ apply incl_injectivity; apply (pr1 can).
+ exact (pr2 isinvx' @ !pr2 isinvx'').
The subset of elements that have inverses
Definition merely_invertible_elements : hsubtype X := merely_hasinv opp is.
Definition invertible_elements (can : ∏ x, iscancelable opp x) : hsubtype X.
Show proof.
If an element has an inverse, then it is cancellable
Definition lcanfromlinv (a b c : X) (c' : haslinv opp is c) :
(c * a) = (c * b) → a = b.
Show proof.
intros e.
refine (!lunax_is is a @ _ @ lunax_is is b).
refine (!maponpaths (λ z, z * _) (pr2 c') @ _ @
maponpaths (λ z, z * _) (pr2 c')).
refine (assocax_is is _ _ _ @ _ @ !assocax_is is _ _ _).
apply maponpaths.
assumption.
refine (!lunax_is is a @ _ @ lunax_is is b).
refine (!maponpaths (λ z, z * _) (pr2 c') @ _ @
maponpaths (λ z, z * _) (pr2 c')).
refine (assocax_is is _ _ _ @ _ @ !assocax_is is _ _ _).
apply maponpaths.
assumption.
Definition rcanfromrinv (a b c : X) (c' : hasrinv opp is c) :
(a * c) = (b * c) → a = b.
Show proof.
intros e.
refine (!runax_is is a @ _ @ runax_is is b).
refine (!maponpaths (λ z, _ * z) (pr2 c') @ _ @
maponpaths (λ z, _ * z) (pr2 c')).
refine (!assocax_is is _ _ _ @ _ @ assocax_is is _ _ _).
apply (maponpaths (λ z, z * _)).
assumption.
End ElementsWithInversesSet.refine (!runax_is is a @ _ @ runax_is is b).
refine (!maponpaths (λ z, _ * z) (pr2 c') @ _ @
maponpaths (λ z, _ * z) (pr2 c')).
refine (!assocax_is is _ _ _ @ _ @ assocax_is is _ _ _).
apply (maponpaths (λ z, z * _)).
assumption.
Section InversesSet.
Similarly, these are propositions for hSets
Context {X : hSet} (opp : binop X) (u : X) (inv : X -> X).
Lemma isapropislinv : isaprop (islinv opp u inv).
Show proof.
Lemma isapropisrinv : isaprop (isrinv opp u inv).
Show proof.
Lemma isapropisinv : isaprop (isinv opp u inv).
Show proof.
End InversesSet.
Definition make_isinv {X : UU} {opp : binop X} {un0 : X} {inv0 : X -> X} (H1 : islinv opp un0 inv0)
(H2 : isrinv opp un0 inv0) : isinv opp un0 inv0 := make_dirprod H1 H2.
Definition invstruct {X : UU} (opp : binop X) (is : ismonoidop opp) : UU :=
total2 (fun inv0 : X -> X => isinv opp (unel_is is) inv0).
Definition make_invstruct {X : UU} {opp : binop X} {is : ismonoidop opp} (inv0 : X -> X)
(H : isinv opp (unel_is is) inv0) : invstruct opp is := tpair _ inv0 H.
Lemma isapropislinv : isaprop (islinv opp u inv).
Show proof.
Lemma isapropisrinv : isaprop (isrinv opp u inv).
Show proof.
Lemma isapropisinv : isaprop (isinv opp u inv).
Show proof.
End InversesSet.
Definition make_isinv {X : UU} {opp : binop X} {un0 : X} {inv0 : X -> X} (H1 : islinv opp un0 inv0)
(H2 : isrinv opp un0 inv0) : isinv opp un0 inv0 := make_dirprod H1 H2.
Definition invstruct {X : UU} (opp : binop X) (is : ismonoidop opp) : UU :=
total2 (fun inv0 : X -> X => isinv opp (unel_is is) inv0).
Definition make_invstruct {X : UU} {opp : binop X} {is : ismonoidop opp} (inv0 : X -> X)
(H : isinv opp (unel_is is) inv0) : invstruct opp is := tpair _ inv0 H.
***** Group operations
Definition isgrop {X : UU} (opp : binop X) : UU :=
total2 (λ is : ismonoidop opp, invstruct opp is).
Definition make_isgrop {X : UU} {opp : binop X} (is1 : ismonoidop opp) (is2 : invstruct opp is1) :
isgrop opp := tpair (λ is : ismonoidop opp, invstruct opp is) is1 is2.
Definition pr1isgrop (X : UU) (opp : binop X) : isgrop opp -> ismonoidop opp := @pr1 _ _.
Coercion pr1isgrop : isgrop >-> ismonoidop.
Definition grinv_is {X : UU} {opp : binop X} (is : isgrop opp) : X -> X := pr1 (pr2 is).
Definition grlinvax_is {X : UU} {opp : binop X} (is : isgrop opp) :
islinv opp (unel_is is) (pr1 (pr2 is)) := pr1 (pr2 (pr2 is)).
Definition grrinvax_is {X : UU} {opp : binop X} (is : isgrop opp) :
isrinv opp (unel_is is) (pr1 (pr2 is)) := pr2 (pr2 (pr2 is)).
Lemma isweqrmultingr_is {X : UU} {opp : binop X} (is : isgrop opp) (x0 : X) :
isrinvertible opp x0.
Show proof.
destruct is as [ is istr ].
set (f := λ x : X, opp x x0).
set (g := λ x : X, opp x ((pr1 istr) x0)).
destruct is as [ assoc isun0 ].
destruct istr as [ inv0 axs ].
destruct isun0 as [ un0 unaxs ].
simpl in * |-.
assert (egf : ∏ x : _, paths (g (f x)) x).
{
intro x. unfold f. unfold g.
destruct (pathsinv0 (assoc x x0 (inv0 x0))).
set (e := pr2 axs x0). simpl in e. rewrite e.
apply (pr2 unaxs x).
}
assert (efg : ∏ x : _, paths (f (g x)) x).
{
intro x. unfold f. unfold g.
destruct (pathsinv0 (assoc x (inv0 x0) x0)).
set (e := pr1 axs x0). simpl in e. rewrite e.
apply (pr2 unaxs x).
}
apply (isweq_iso _ _ egf efg).
set (f := λ x : X, opp x x0).
set (g := λ x : X, opp x ((pr1 istr) x0)).
destruct is as [ assoc isun0 ].
destruct istr as [ inv0 axs ].
destruct isun0 as [ un0 unaxs ].
simpl in * |-.
assert (egf : ∏ x : _, paths (g (f x)) x).
{
intro x. unfold f. unfold g.
destruct (pathsinv0 (assoc x x0 (inv0 x0))).
set (e := pr2 axs x0). simpl in e. rewrite e.
apply (pr2 unaxs x).
}
assert (efg : ∏ x : _, paths (f (g x)) x).
{
intro x. unfold f. unfold g.
destruct (pathsinv0 (assoc x (inv0 x0) x0)).
set (e := pr1 axs x0). simpl in e. rewrite e.
apply (pr2 unaxs x).
}
apply (isweq_iso _ _ egf efg).
Lemma isweqlmultingr_is {X : UU} {opp : binop X} (is : isgrop opp) (x0 : X) :
islinvertible opp x0.
Show proof.
destruct is as [ is istr ].
set (f := λ x : X, opp x0 x).
set (g := λ x : X, opp ((pr1 istr) x0) x).
destruct is as [ assoc isun0 ].
destruct istr as [ inv0 axs ].
destruct isun0 as [ un0 unaxs ].
simpl in * |-.
assert (egf : ∏ x : _, paths (g (f x)) x).
{
intro x. unfold f. unfold g.
destruct (assoc (inv0 x0) x0 x).
set (e := pr1 axs x0). simpl in e. rewrite e.
apply (pr1 unaxs x).
}
assert (efg : ∏ x : _, paths (f (g x)) x).
{
intro x. unfold f. unfold g.
destruct (assoc x0 (inv0 x0) x).
set (e := pr2 axs x0). simpl in e. rewrite e.
apply (pr1 unaxs x).
}
apply (isweq_iso _ _ egf efg).
set (f := λ x : X, opp x0 x).
set (g := λ x : X, opp ((pr1 istr) x0) x).
destruct is as [ assoc isun0 ].
destruct istr as [ inv0 axs ].
destruct isun0 as [ un0 unaxs ].
simpl in * |-.
assert (egf : ∏ x : _, paths (g (f x)) x).
{
intro x. unfold f. unfold g.
destruct (assoc (inv0 x0) x0 x).
set (e := pr1 axs x0). simpl in e. rewrite e.
apply (pr1 unaxs x).
}
assert (efg : ∏ x : _, paths (f (g x)) x).
{
intro x. unfold f. unfold g.
destruct (assoc x0 (inv0 x0) x).
set (e := pr2 axs x0). simpl in e. rewrite e.
apply (pr1 unaxs x).
}
apply (isweq_iso _ _ egf efg).
Lemma isapropinvstruct {X : hSet} {opp : binop X} (is : ismonoidop opp) :
isaprop (invstruct opp is).
Show proof.
apply isofhlevelsn. intro is0.
set (un0 := pr1 (pr2 is)).
assert (int : ∏ (i : X -> X),
isaprop (dirprod (∏ x : X, paths (opp (i x) x) un0)
(∏ x : X, paths (opp x (i x)) un0))).
{
intro i. apply (isofhleveldirprod 1).
- apply impred. intro x. simpl. apply (setproperty X).
- apply impred. intro x. simpl. apply (setproperty X).
}
apply (isapropsubtype (λ i : _, make_hProp _ (int i))).
intros inv1 inv2. simpl. intro ax1. intro ax2. apply funextfun. intro x0.
apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is (tpair _ is is0) x0))).
simpl. rewrite (pr1 ax1 x0). rewrite (pr1 ax2 x0). apply idpath.
set (un0 := pr1 (pr2 is)).
assert (int : ∏ (i : X -> X),
isaprop (dirprod (∏ x : X, paths (opp (i x) x) un0)
(∏ x : X, paths (opp x (i x)) un0))).
{
intro i. apply (isofhleveldirprod 1).
- apply impred. intro x. simpl. apply (setproperty X).
- apply impred. intro x. simpl. apply (setproperty X).
}
apply (isapropsubtype (λ i : _, make_hProp _ (int i))).
intros inv1 inv2. simpl. intro ax1. intro ax2. apply funextfun. intro x0.
apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is (tpair _ is is0) x0))).
simpl. rewrite (pr1 ax1 x0). rewrite (pr1 ax2 x0). apply idpath.
Lemma isapropisgrop {X : hSet} (opp : binop X) : isaprop (isgrop opp).
Show proof.
Lemma isgropif {X : hSet} {opp : binop X} (is0 : ismonoidop opp)
(is : ∏ x : X, merely_hasrinv opp is0 x) : isgrop opp.
Show proof.
split with is0.
destruct is0 as [ assoc isun0 ].
destruct isun0 as [ un0 unaxs0 ].
simpl in is.
simpl in unaxs0. simpl in un0.
simpl in assoc. simpl in unaxs0.
assert (l1 : ∏ x' : X, isincl (λ x0 : X, opp x0 x')).
{
intro x'.
apply (@hinhuniv (total2 (λ x0 : X, (opp x' x0) = un0))
(make_hProp _ (isapropisincl (λ x0 : X, opp x0 x')))).
- intro int1. simpl. apply isinclbetweensets.
+ apply (pr2 X).
+ apply (pr2 X).
+ intros a b. intro e.
rewrite (pathsinv0 (pr2 unaxs0 a)). rewrite (pathsinv0 (pr2 unaxs0 b)).
destruct int1 as [ invx' eq ].
rewrite (pathsinv0 eq).
destruct (assoc a x' invx').
destruct (assoc b x' invx').
rewrite e. apply idpath.
- apply (is x').
}
assert (is' : ∏ x : X, hexists (λ x0 : X, (opp x0 x) = un0)).
{
intro x. apply (λ f : _ , hinhuniv f (is x)). intro s1.
destruct s1 as [ x' eq ]. apply hinhpr. split with x'. simpl.
apply (invmaponpathsincl _ (l1 x')).
rewrite (assoc x' x x'). rewrite eq. rewrite (pr1 unaxs0 x').
unfold unel_is. simpl. rewrite (pr2 unaxs0 x'). apply idpath.
}
assert (l1' : ∏ x' : X, isincl (λ x0 : X, opp x' x0)).
{
intro x'.
apply (@hinhuniv (total2 (λ x0 : X, (opp x0 x') = un0))
(make_hProp _ (isapropisincl (λ x0 : X, opp x' x0)))).
- intro int1. simpl. apply isinclbetweensets.
+ apply (pr2 X).
+ apply (pr2 X).
+ intros a b. intro e.
rewrite (pathsinv0 (pr1 unaxs0 a)). rewrite (pathsinv0 (pr1 unaxs0 b)).
destruct int1 as [ invx' eq ]. rewrite (pathsinv0 eq).
destruct (pathsinv0 (assoc invx' x' a)).
destruct (pathsinv0 (assoc invx' x' b)).
rewrite e. apply idpath.
- apply (is' x').
}
assert (int : ∏ x : X, isaprop (total2 (λ x0 : X, (opp x0 x) = un0))).
{
intro x. apply isapropsubtype. intros x1 x2. intros eq1 eq2.
apply (invmaponpathsincl _ (l1 x)).
rewrite eq1. rewrite eq2. apply idpath.
}
simpl.
set (linv0 := λ x : X, hinhunivcor1 (make_hProp _ (int x)) (is' x)).
simpl in linv0.
set (inv0 := λ x : X, pr1 (linv0 x)). split with inv0. simpl.
split with (λ x : _, pr2 (linv0 x)). intro x.
apply (invmaponpathsincl _ (l1 x)).
rewrite (assoc x (inv0 x) x). change (inv0 x) with (pr1 (linv0 x)).
rewrite (pr2 (linv0 x)). unfold unel_is. simpl.
rewrite (pr1 unaxs0 x). rewrite (pr2 unaxs0 x). apply idpath.
destruct is0 as [ assoc isun0 ].
destruct isun0 as [ un0 unaxs0 ].
simpl in is.
simpl in unaxs0. simpl in un0.
simpl in assoc. simpl in unaxs0.
assert (l1 : ∏ x' : X, isincl (λ x0 : X, opp x0 x')).
{
intro x'.
apply (@hinhuniv (total2 (λ x0 : X, (opp x' x0) = un0))
(make_hProp _ (isapropisincl (λ x0 : X, opp x0 x')))).
- intro int1. simpl. apply isinclbetweensets.
+ apply (pr2 X).
+ apply (pr2 X).
+ intros a b. intro e.
rewrite (pathsinv0 (pr2 unaxs0 a)). rewrite (pathsinv0 (pr2 unaxs0 b)).
destruct int1 as [ invx' eq ].
rewrite (pathsinv0 eq).
destruct (assoc a x' invx').
destruct (assoc b x' invx').
rewrite e. apply idpath.
- apply (is x').
}
assert (is' : ∏ x : X, hexists (λ x0 : X, (opp x0 x) = un0)).
{
intro x. apply (λ f : _ , hinhuniv f (is x)). intro s1.
destruct s1 as [ x' eq ]. apply hinhpr. split with x'. simpl.
apply (invmaponpathsincl _ (l1 x')).
rewrite (assoc x' x x'). rewrite eq. rewrite (pr1 unaxs0 x').
unfold unel_is. simpl. rewrite (pr2 unaxs0 x'). apply idpath.
}
assert (l1' : ∏ x' : X, isincl (λ x0 : X, opp x' x0)).
{
intro x'.
apply (@hinhuniv (total2 (λ x0 : X, (opp x0 x') = un0))
(make_hProp _ (isapropisincl (λ x0 : X, opp x' x0)))).
- intro int1. simpl. apply isinclbetweensets.
+ apply (pr2 X).
+ apply (pr2 X).
+ intros a b. intro e.
rewrite (pathsinv0 (pr1 unaxs0 a)). rewrite (pathsinv0 (pr1 unaxs0 b)).
destruct int1 as [ invx' eq ]. rewrite (pathsinv0 eq).
destruct (pathsinv0 (assoc invx' x' a)).
destruct (pathsinv0 (assoc invx' x' b)).
rewrite e. apply idpath.
- apply (is' x').
}
assert (int : ∏ x : X, isaprop (total2 (λ x0 : X, (opp x0 x) = un0))).
{
intro x. apply isapropsubtype. intros x1 x2. intros eq1 eq2.
apply (invmaponpathsincl _ (l1 x)).
rewrite eq1. rewrite eq2. apply idpath.
}
simpl.
set (linv0 := λ x : X, hinhunivcor1 (make_hProp _ (int x)) (is' x)).
simpl in linv0.
set (inv0 := λ x : X, pr1 (linv0 x)). split with inv0. simpl.
split with (λ x : _, pr2 (linv0 x)). intro x.
apply (invmaponpathsincl _ (l1 x)).
rewrite (assoc x (inv0 x) x). change (inv0 x) with (pr1 (linv0 x)).
rewrite (pr2 (linv0 x)). unfold unel_is. simpl.
rewrite (pr1 unaxs0 x). rewrite (pr2 unaxs0 x). apply idpath.
Definition iscomm {X : UU} (opp : binop X) : UU := ∏ x x' : X, paths (opp x x') (opp x' x).
Lemma isapropiscomm {X : hSet} (opp : binop X) : isaprop (iscomm opp).
Show proof.
Definition isabmonoidop {X : UU} (opp : binop X) : UU := (ismonoidop opp) × (iscomm opp).
Definition make_isabmonoidop {X : UU} {opp : binop X} (H1 : ismonoidop opp) (H2 : iscomm opp) :
isabmonoidop opp := make_dirprod H1 H2.
Definition pr1isabmonoidop (X : UU) (opp : binop X) : isabmonoidop opp -> ismonoidop opp :=
@pr1 _ _.
Coercion pr1isabmonoidop : isabmonoidop >-> ismonoidop.
Definition commax_is {X : UU} {opp : binop X} (is : isabmonoidop opp) : iscomm opp := pr2 is.
Lemma isapropisabmonoidop {X : hSet} (opp : binop X) :
isaprop (isabmonoidop opp).
Show proof.
Lemma abmonoidoprer {X : UU} {opp : binop X} (is : isabmonoidop opp) (a b c d : X) :
paths (opp (opp a b) (opp c d)) (opp (opp a c) (opp b d)).
Show proof.
destruct is as [ is comm ]. destruct is as [ assoc unital0 ].
simpl in *.
destruct (assoc (opp a b) c d). destruct (assoc (opp a c) b d).
destruct (pathsinv0 (assoc a b c)). destruct (pathsinv0 (assoc a c b)).
destruct (comm b c). apply idpath.
simpl in *.
destruct (assoc (opp a b) c d). destruct (assoc (opp a c) b d).
destruct (pathsinv0 (assoc a b c)). destruct (pathsinv0 (assoc a c b)).
destruct (comm b c). apply idpath.
Lemma weqlcancelablercancelable {X : UU} (opp : binop X) (is : iscomm opp) (x : X) :
(islcancelable opp x) ≃ (isrcancelable opp x).
Show proof.
assert (f : (islcancelable opp x) -> (isrcancelable opp x)).
{
unfold islcancelable. unfold isrcancelable.
intro isl. apply (λ h : _, isinclhomot _ _ h isl).
intro x0. apply is.
}
assert (g : (isrcancelable opp x) -> (islcancelable opp x)).
{
unfold islcancelable. unfold isrcancelable. intro isr.
apply (λ h : _, isinclhomot _ _ h isr). intro x0. apply is.
}
split with f.
apply (isweqimplimpl f g (isapropisincl (λ x0 : X, opp x x0))
(isapropisincl (λ x0 : X, opp x0 x))).
{
unfold islcancelable. unfold isrcancelable.
intro isl. apply (λ h : _, isinclhomot _ _ h isl).
intro x0. apply is.
}
assert (g : (isrcancelable opp x) -> (islcancelable opp x)).
{
unfold islcancelable. unfold isrcancelable. intro isr.
apply (λ h : _, isinclhomot _ _ h isr). intro x0. apply is.
}
split with f.
apply (isweqimplimpl f g (isapropisincl (λ x0 : X, opp x x0))
(isapropisincl (λ x0 : X, opp x0 x))).
Lemma weqlinvertiblerinvertible {X : UU} (opp : binop X) (is : iscomm opp) (x : X) :
(islinvertible opp x) ≃ (isrinvertible opp x).
Show proof.
assert (f : (islinvertible opp x) -> (isrinvertible opp x)).
{
unfold islinvertible. unfold isrinvertible. intro isl.
apply (isweqhomot (λ y, opp x y)).
- intro z. apply is.
- apply isl.
}
assert (g : (isrinvertible opp x) -> (islinvertible opp x)).
{
unfold islinvertible. unfold isrinvertible. intro isr.
apply (λ h : _, isweqhomot _ _ h isr).
intro x0. apply is.
}
split with f.
apply (isweqimplimpl f g (isapropisweq (λ x0 : X, opp x x0))
(isapropisweq (λ x0 : X, opp x0 x))).
{
unfold islinvertible. unfold isrinvertible. intro isl.
apply (isweqhomot (λ y, opp x y)).
- intro z. apply is.
- apply isl.
}
assert (g : (isrinvertible opp x) -> (islinvertible opp x)).
{
unfold islinvertible. unfold isrinvertible. intro isr.
apply (λ h : _, isweqhomot _ _ h isr).
intro x0. apply is.
}
split with f.
apply (isweqimplimpl f g (isapropisweq (λ x0 : X, opp x x0))
(isapropisweq (λ x0 : X, opp x0 x))).
Lemma weqlunitrunit {X : hSet} (opp : binop X) (is : iscomm opp) (un0 : X) :
(islunit opp un0) ≃ (isrunit opp un0).
Show proof.
assert (f : (islunit opp un0) -> (isrunit opp un0)).
{
unfold islunit. unfold isrunit. intro isl. intro x.
destruct (is un0 x). apply (isl x).
}
assert (g : (isrunit opp un0) -> (islunit opp un0)).
{
unfold islunit. unfold isrunit. intro isr. intro x.
destruct (is x un0). apply (isr x).
}
split with f.
apply (isweqimplimpl f g (isapropislunit opp un0) (isapropisrunit opp un0)).
{
unfold islunit. unfold isrunit. intro isl. intro x.
destruct (is un0 x). apply (isl x).
}
assert (g : (isrunit opp un0) -> (islunit opp un0)).
{
unfold islunit. unfold isrunit. intro isr. intro x.
destruct (is x un0). apply (isr x).
}
split with f.
apply (isweqimplimpl f g (isapropislunit opp un0) (isapropisrunit opp un0)).
Lemma weqlinvrinv {X : hSet} (opp : binop X) (is : iscomm opp) (un0 : X) (inv0 : X -> X) :
(islinv opp un0 inv0) ≃ (isrinv opp un0 inv0).
Show proof.
assert (f : (islinv opp un0 inv0) -> (isrinv opp un0 inv0)).
{
unfold islinv. unfold isrinv. intro isl. intro x.
destruct (is (inv0 x) x). apply (isl x).
}
assert (g : (isrinv opp un0 inv0) -> (islinv opp un0 inv0)).
{
unfold islinv. unfold isrinv. intro isr. intro x.
destruct (is x (inv0 x)). apply (isr x).
}
split with f.
apply (isweqimplimpl f g (isapropislinv opp un0 inv0) (isapropisrinv opp un0 inv0)).
Opaque abmonoidoprer.{
unfold islinv. unfold isrinv. intro isl. intro x.
destruct (is (inv0 x) x). apply (isl x).
}
assert (g : (isrinv opp un0 inv0) -> (islinv opp un0 inv0)).
{
unfold islinv. unfold isrinv. intro isr. intro x.
destruct (is x (inv0 x)). apply (isr x).
}
split with f.
apply (isweqimplimpl f g (isapropislinv opp un0 inv0) (isapropisrinv opp un0 inv0)).
Definition isabgrop {X : UU} (opp : binop X) : UU := (isgrop opp) × (iscomm opp).
Definition make_isabgrop {X : UU} {opp : binop X} (H1 : isgrop opp) (H2 : iscomm opp) :
isabgrop opp := make_dirprod H1 H2.
Definition pr1isabgrop (X : UU) (opp : binop X) : isabgrop opp -> isgrop opp := @pr1 _ _.
Coercion pr1isabgrop : isabgrop >-> isgrop.
Definition isabgroptoisabmonoidop (X : UU) (opp : binop X) : isabgrop opp -> isabmonoidop opp :=
λ is : _, make_dirprod (pr1 (pr1 is)) (pr2 is).
Coercion isabgroptoisabmonoidop : isabgrop >-> isabmonoidop.
Lemma isapropisabgrop {X : hSet} (opp : binop X) : isaprop (isabgrop opp).
Show proof.
Definition isldistr {X : UU} (opp1 opp2 : binop X) : UU :=
∏ x x' x'' : X, paths (opp2 x'' (opp1 x x')) (opp1 (opp2 x'' x) (opp2 x'' x')).
Lemma isapropisldistr {X : hSet} (opp1 opp2 : binop X) : isaprop (isldistr opp1 opp2).
Show proof.
apply impred. intro x.
apply impred. intro x'.
apply impred. intro x''.
simpl. apply (setproperty X).
apply impred. intro x'.
apply impred. intro x''.
simpl. apply (setproperty X).
Definition isrdistr {X : UU} (opp1 opp2 : binop X) : UU :=
∏ x x' x'' : X, paths (opp2 (opp1 x x') x'') (opp1 (opp2 x x'') (opp2 x' x'')).
Lemma isapropisrdistr {X : hSet} (opp1 opp2 : binop X) : isaprop (isrdistr opp1 opp2).
Show proof.
apply impred. intro x.
apply impred. intro x'.
apply impred. intro x''.
simpl. apply (setproperty X).
apply impred. intro x'.
apply impred. intro x''.
simpl. apply (setproperty X).
Definition isdistr {X : UU} (opp1 opp2 : binop X) : UU :=
(isldistr opp1 opp2) × (isrdistr opp1 opp2).
Lemma isapropisdistr {X : hSet} (opp1 opp2 : binop X) : isaprop (isdistr opp1 opp2).
Show proof.
Lemma weqldistrrdistr {X : hSet} (opp1 opp2 : binop X) (is : iscomm opp2) :
(isldistr opp1 opp2) ≃ (isrdistr opp1 opp2).
Show proof.
assert (f : (isldistr opp1 opp2) -> (isrdistr opp1 opp2)).
{
unfold isldistr. unfold isrdistr. intro isl. intros x x' x''.
destruct (is x'' (opp1 x x')). destruct (is x'' x). destruct (is x'' x').
apply (isl x x' x'').
}
assert (g : (isrdistr opp1 opp2) -> (isldistr opp1 opp2)).
{
unfold isldistr. unfold isrdistr. intro isr. intros x x' x''.
destruct (is (opp1 x x') x''). destruct (is x x''). destruct (is x' x'').
apply (isr x x' x'').
}
split with f.
apply (isweqimplimpl f g (isapropisldistr opp1 opp2) (isapropisrdistr opp1 opp2)).
{
unfold isldistr. unfold isrdistr. intro isl. intros x x' x''.
destruct (is x'' (opp1 x x')). destruct (is x'' x). destruct (is x'' x').
apply (isl x x' x'').
}
assert (g : (isrdistr opp1 opp2) -> (isldistr opp1 opp2)).
{
unfold isldistr. unfold isrdistr. intro isr. intros x x' x''.
destruct (is (opp1 x x') x''). destruct (is x x''). destruct (is x' x'').
apply (isr x x' x'').
}
split with f.
apply (isweqimplimpl f g (isapropisldistr opp1 opp2) (isapropisrdistr opp1 opp2)).
Definition isabsorb {X : UU} (opp1 opp2 : binop X) : UU :=
∏ x y : X, opp1 x (opp2 x y) = x.
Lemma isapropisabsorb {X : hSet} (opp1 opp2 : binop X) :
isaprop (isabsorb opp1 opp2).
Show proof.
Definition isrigops {X : UU} (opp1 opp2 : binop X) : UU :=
(∑ axs : (isabmonoidop opp1) × (ismonoidop opp2),
(∏ x : X, (opp2 (unel_is (pr1 axs)) x) = (unel_is (pr1 axs)))
× (∏ x : X, (opp2 x (unel_is (pr1 axs))) = (unel_is (pr1 axs))))
× (isdistr opp1 opp2).
Definition make_isrigops {X : UU} {opp1 opp2 : binop X} (H1 : isabmonoidop opp1)
(H2 : ismonoidop opp2) (H3 : ∏ x : X, (opp2 (unel_is H1) x) = (unel_is H1))
(H4 : ∏ x : X, (opp2 x (unel_is H1)) = (unel_is H1))
(H5 : isdistr opp1 opp2) : isrigops opp1 opp2 :=
tpair _ (tpair _ (make_dirprod H1 H2) (make_dirprod H3 H4)) H5.
Definition rigop1axs_is {X : UU} {opp1 opp2 : binop X} :
isrigops opp1 opp2 -> isabmonoidop opp1 := λ is : _, pr1 (pr1 (pr1 is)).
Definition rigop2axs_is {X : UU} {opp1 opp2 : binop X} : isrigops opp1 opp2 -> ismonoidop opp2 :=
λ is : _, pr2 (pr1 (pr1 is)).
Definition rigdistraxs_is {X : UU} {opp1 opp2 : binop X} :
isrigops opp1 opp2 -> isdistr opp1 opp2 := λ is : _, pr2 is.
Definition rigldistrax_is {X : UU} {opp1 opp2 : binop X} :
isrigops opp1 opp2 -> isldistr opp1 opp2 := λ is : _, pr1 (pr2 is).
Definition rigrdistrax_is {X : UU} {opp1 opp2 : binop X} :
isrigops opp1 opp2 -> isrdistr opp1 opp2 := λ is : _, pr2 (pr2 is).
Definition rigunel1_is {X : UU} {opp1 opp2 : binop X} (is : isrigops opp1 opp2) : X :=
pr1 (pr2 (pr1 (rigop1axs_is is))).
Definition rigunel2_is {X : UU} {opp1 opp2 : binop X} (is : isrigops opp1 opp2) : X :=
(pr1 (pr2 (rigop2axs_is is))).
Definition rigmult0x_is {X : UU} {opp1 opp2 : binop X} (is : isrigops opp1 opp2) (x : X) :
paths (opp2 (rigunel1_is is) x) (rigunel1_is is) := pr1 (pr2 (pr1 is)) x.
Definition rigmultx0_is {X : UU} {opp1 opp2 : binop X} (is : isrigops opp1 opp2) (x : X) :
paths (opp2 x (rigunel1_is is)) (rigunel1_is is) := pr2 (pr2 (pr1 is)) x.
Lemma isapropisrigops {X : hSet} (opp1 opp2 : binop X) : isaprop (isrigops opp1 opp2).
Show proof.
apply (isofhleveldirprod 1).
- apply (isofhleveltotal2 1).
+ apply (isofhleveldirprod 1).
* apply isapropisabmonoidop.
* apply isapropismonoidop.
+ intro x. apply (isofhleveldirprod 1).
* apply impred. intro x'.
apply (setproperty X).
* apply impred. intro x'.
apply (setproperty X).
- apply isapropisdistr.
- apply (isofhleveltotal2 1).
+ apply (isofhleveldirprod 1).
* apply isapropisabmonoidop.
* apply isapropismonoidop.
+ intro x. apply (isofhleveldirprod 1).
* apply impred. intro x'.
apply (setproperty X).
* apply impred. intro x'.
apply (setproperty X).
- apply isapropisdistr.
Definition isringops {X : UU} (opp1 opp2 : binop X) : UU :=
dirprod ((isabgrop opp1) × (ismonoidop opp2)) (isdistr opp1 opp2).
Definition make_isringops {X : UU} {opp1 opp2 : binop X} (H1 : isabgrop opp1) (H2 : ismonoidop opp2)
(H3 : isdistr opp1 opp2) : isringops opp1 opp2 :=
make_dirprod (make_dirprod H1 H2) H3.
Definition ringop1axs_is {X : UU} {opp1 opp2 : binop X} : isringops opp1 opp2 -> isabgrop opp1 :=
λ is : _, pr1 (pr1 is).
Definition ringop2axs_is {X : UU} {opp1 opp2 : binop X} : isringops opp1 opp2 -> ismonoidop opp2 :=
λ is : _, pr2 (pr1 is).
Definition ringdistraxs_is {X : UU} {opp1 opp2 : binop X} :
isringops opp1 opp2 -> isdistr opp1 opp2 := λ is : _, pr2 is.
Definition ringldistrax_is {X : UU} {opp1 opp2 : binop X} :
isringops opp1 opp2 -> isldistr opp1 opp2 := λ is : _, pr1 (pr2 is).
Definition ringrdistrax_is {X : UU} {opp1 opp2 : binop X} :
isringops opp1 opp2 -> isrdistr opp1 opp2 := λ is : _, pr2 (pr2 is).
Definition ringunel1_is {X : UU} {opp1 opp2 : binop X} (is : isringops opp1 opp2) : X :=
unel_is (pr1 (pr1 is)).
Definition ringunel2_is {X : UU} {opp1 opp2 : binop X} (is : isringops opp1 opp2) : X :=
unel_is (pr2 (pr1 is)).
Lemma isapropisringops {X : hSet} (opp1 opp2 : binop X) : isaprop (isringops opp1 opp2).
Show proof.
apply (isofhleveldirprod 1).
- apply (isofhleveldirprod 1).
+ apply isapropisabgrop.
+ apply isapropismonoidop.
- apply isapropisdistr.
- apply (isofhleveldirprod 1).
+ apply isapropisabgrop.
+ apply isapropismonoidop.
- apply isapropisdistr.
Lemma multx0_is_l {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1) (is2 : ismonoidop opp2)
(is12 : isdistr opp1 opp2) (x : X) : paths (opp2 x (unel_is (pr1 is1))) (unel_is (pr1 is1)).
Show proof.
destruct is12 as [ ldistr0 rdistr0 ].
destruct is2 as [ assoc2 [ un2 [ lun2 run2 ] ] ].
simpl in *.
apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is is1 (opp2 x un2)))).
simpl.
destruct is1 as [ [ assoc1 [ un1 [ lun1 run1 ] ] ] [ inv0 [ linv0 rinv0 ] ] ].
unfold unel_is. simpl in *.
rewrite (lun1 (opp2 x un2)). destruct (ldistr0 un1 un2 x).
rewrite (run2 x). rewrite (lun1 un2). rewrite (run2 x). apply idpath.
Opaque multx0_is_l.destruct is2 as [ assoc2 [ un2 [ lun2 run2 ] ] ].
simpl in *.
apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is is1 (opp2 x un2)))).
simpl.
destruct is1 as [ [ assoc1 [ un1 [ lun1 run1 ] ] ] [ inv0 [ linv0 rinv0 ] ] ].
unfold unel_is. simpl in *.
rewrite (lun1 (opp2 x un2)). destruct (ldistr0 un1 un2 x).
rewrite (run2 x). rewrite (lun1 un2). rewrite (run2 x). apply idpath.
Lemma mult0x_is_l {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1) (is2 : ismonoidop opp2)
(is12 : isdistr opp1 opp2) (x : X) : paths (opp2 (unel_is (pr1 is1)) x) (unel_is (pr1 is1)).
Show proof.
destruct is12 as [ ldistr0 rdistr0 ].
destruct is2 as [ assoc2 [ un2 [ lun2 run2 ] ] ]. simpl in *.
apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is is1 (opp2 un2 x)))).
simpl.
destruct is1 as [ [ assoc1 [ un1 [ lun1 run1 ] ] ] [ inv0 [ linv0 rinv0 ] ] ].
unfold unel_is. simpl in *.
rewrite (lun1 (opp2 un2 x)). destruct (rdistr0 un1 un2 x).
rewrite (lun2 x). rewrite (lun1 un2). rewrite (lun2 x). apply idpath.
Opaque mult0x_is_l.destruct is2 as [ assoc2 [ un2 [ lun2 run2 ] ] ]. simpl in *.
apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is is1 (opp2 un2 x)))).
simpl.
destruct is1 as [ [ assoc1 [ un1 [ lun1 run1 ] ] ] [ inv0 [ linv0 rinv0 ] ] ].
unfold unel_is. simpl in *.
rewrite (lun1 (opp2 un2 x)). destruct (rdistr0 un1 un2 x).
rewrite (lun2 x). rewrite (lun1 un2). rewrite (lun2 x). apply idpath.
Definition minus1_is_l {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1)
(is2 : ismonoidop opp2) := (grinv_is is1) (unel_is is2).
Lemma islinvmultwithminus1_is_l {X : UU} {opp1 opp2 : binop X}
(is1 : isgrop opp1) (is2 : ismonoidop opp2) (is12 : isdistr opp1 opp2)
(x : X) : paths (opp1 (opp2 (minus1_is_l is1 is2) x) x) (unel_is (pr1 is1)).
Show proof.
set (xinv := opp2 (minus1_is_l is1 is2) x).
rewrite (pathsinv0 (lunax_is is2 x)).
unfold xinv.
rewrite (pathsinv0 (pr2 is12 _ _ x)).
unfold minus1_is_l. unfold grinv_is.
rewrite (grlinvax_is is1 _). apply mult0x_is_l.
- apply is2.
- apply is12.
Opaque islinvmultwithminus1_is_l.rewrite (pathsinv0 (lunax_is is2 x)).
unfold xinv.
rewrite (pathsinv0 (pr2 is12 _ _ x)).
unfold minus1_is_l. unfold grinv_is.
rewrite (grlinvax_is is1 _). apply mult0x_is_l.
- apply is2.
- apply is12.
Lemma isrinvmultwithminus1_is_l {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1)
(is2 : ismonoidop opp2) (is12 : isdistr opp1 opp2) (x : X) :
paths (opp1 x (opp2 (minus1_is_l is1 is2) x)) (unel_is (pr1 is1)).
Show proof.
set (xinv := opp2 (minus1_is_l is1 is2) x).
rewrite (pathsinv0 (lunax_is is2 x)). unfold xinv.
rewrite (pathsinv0 (pr2 is12 _ _ x)). unfold minus1_is_l. unfold grinv_is.
rewrite (grrinvax_is is1 _).
apply mult0x_is_l. apply is2. apply is12.
Opaque isrinvmultwithminus1_is_l.rewrite (pathsinv0 (lunax_is is2 x)). unfold xinv.
rewrite (pathsinv0 (pr2 is12 _ _ x)). unfold minus1_is_l. unfold grinv_is.
rewrite (grrinvax_is is1 _).
apply mult0x_is_l. apply is2. apply is12.
Lemma isminusmultwithminus1_is_l {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1)
(is2 : ismonoidop opp2) (is12 : isdistr opp1 opp2) (x : X) :
paths (opp2 (minus1_is_l is1 is2) x) (grinv_is is1 x).
Show proof.
apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is is1 x))).
simpl. rewrite (islinvmultwithminus1_is_l is1 is2 is12 x).
unfold grinv_is. rewrite (grlinvax_is is1 x). apply idpath.
Opaque isminusmultwithminus1_is_l.simpl. rewrite (islinvmultwithminus1_is_l is1 is2 is12 x).
unfold grinv_is. rewrite (grlinvax_is is1 x). apply idpath.
Lemma isringopsif {X : UU} {opp1 opp2 : binop X} (is1 : isgrop opp1) (is2 : ismonoidop opp2)
(is12 : isdistr opp1 opp2) : isringops opp1 opp2.
Show proof.
set (assoc1 := pr1 (pr1 is1)).
split.
- split.
+ split with is1.
intros x y.
apply (invmaponpathsweq
(make_weq _ (isweqrmultingr_is is1 (opp2 (minus1_is_l is1 is2) (opp1 x y))))).
simpl. rewrite (isrinvmultwithminus1_is_l is1 is2 is12 (opp1 x y)).
rewrite (pr1 is12 x y _).
destruct (assoc1 (opp1 y x) (opp2 (minus1_is_l is1 is2) x) (opp2 (minus1_is_l is1 is2) y)).
rewrite (assoc1 y x _).
destruct (pathsinv0 (isrinvmultwithminus1_is_l is1 is2 is12 x)).
unfold unel_is. rewrite (runax_is (pr1 is1) y).
rewrite (isrinvmultwithminus1_is_l is1 is2 is12 y).
apply idpath.
+ apply is2.
- apply is12.
split.
- split.
+ split with is1.
intros x y.
apply (invmaponpathsweq
(make_weq _ (isweqrmultingr_is is1 (opp2 (minus1_is_l is1 is2) (opp1 x y))))).
simpl. rewrite (isrinvmultwithminus1_is_l is1 is2 is12 (opp1 x y)).
rewrite (pr1 is12 x y _).
destruct (assoc1 (opp1 y x) (opp2 (minus1_is_l is1 is2) x) (opp2 (minus1_is_l is1 is2) y)).
rewrite (assoc1 y x _).
destruct (pathsinv0 (isrinvmultwithminus1_is_l is1 is2 is12 x)).
unfold unel_is. rewrite (runax_is (pr1 is1) y).
rewrite (isrinvmultwithminus1_is_l is1 is2 is12 y).
apply idpath.
+ apply is2.
- apply is12.
Definition ringmultx0_is {X : UU} {opp1 opp2 : binop X} (is : isringops opp1 opp2) :
∏ (x : X), opp2 x (unel_is (pr1 (ringop1axs_is is))) = unel_is (pr1 (ringop1axs_is is)) :=
multx0_is_l (ringop1axs_is is) (ringop2axs_is is) (ringdistraxs_is is).
Definition ringmult0x_is {X : UU} {opp1 opp2 : binop X} (is : isringops opp1 opp2) :
∏ (x : X), opp2 (unel_is (pr1 (ringop1axs_is is))) x = unel_is (pr1 (ringop1axs_is is)) :=
mult0x_is_l (ringop1axs_is is) (ringop2axs_is is) (ringdistraxs_is is).
Definition ringminus1_is {X : UU} {opp1 opp2 : binop X} (is : isringops opp1 opp2) : X :=
minus1_is_l (ringop1axs_is is) (ringop2axs_is is).
Definition ringmultwithminus1_is {X : UU} {opp1 opp2 : binop X} (is : isringops opp1 opp2) :
∏ (x : X),
opp2 (minus1_is_l (ringop1axs_is is) (ringop2axs_is is)) x = grinv_is (ringop1axs_is is) x :=
isminusmultwithminus1_is_l (ringop1axs_is is) (ringop2axs_is is) (ringdistraxs_is is).
Definition isringopstoisrigops (X : UU) (opp1 opp2 : binop X) (is : isringops opp1 opp2) :
isrigops opp1 opp2.
Show proof.
split.
- split with (make_dirprod (isabgroptoisabmonoidop _ _ (ringop1axs_is is)) (ringop2axs_is is)).
split.
+ simpl. apply (ringmult0x_is).
+ simpl. apply (ringmultx0_is).
- apply (ringdistraxs_is is).
Coercion isringopstoisrigops : isringops >-> isrigops.- split with (make_dirprod (isabgroptoisabmonoidop _ _ (ringop1axs_is is)) (ringop2axs_is is)).
split.
+ simpl. apply (ringmult0x_is).
+ simpl. apply (ringmultx0_is).
- apply (ringdistraxs_is is).
Definition iscommrigops {X : UU} (opp1 opp2 : binop X) : UU :=
(isrigops opp1 opp2) × (iscomm opp2).
Definition pr1iscommrigops (X : UU) (opp1 opp2 : binop X) :
iscommrigops opp1 opp2 -> isrigops opp1 opp2 := @pr1 _ _.
Coercion pr1iscommrigops : iscommrigops >-> isrigops.
Definition rigiscommop2_is {X : UU} {opp1 opp2 : binop X} (is : iscommrigops opp1 opp2) :
iscomm opp2 := pr2 is.
Lemma isapropiscommrig {X : hSet} (opp1 opp2 : binop X) : isaprop (iscommrigops opp1 opp2).
Show proof.
Definition iscommringops {X : UU} (opp1 opp2 : binop X) : UU :=
(isringops opp1 opp2) × (iscomm opp2).
Definition pr1iscommringops (X : UU) (opp1 opp2 : binop X) :
iscommringops opp1 opp2 -> isringops opp1 opp2 := @pr1 _ _.
Coercion pr1iscommringops : iscommringops >-> isringops.
Definition ringiscommop2_is {X : UU} {opp1 opp2 : binop X} (is : iscommringops opp1 opp2) :
iscomm opp2 := pr2 is.
Lemma isapropiscommring {X : hSet} (opp1 opp2 : binop X) : isaprop (iscommringops opp1 opp2).
Show proof.
Definition iscommringopstoiscommrigops (X : UU) (opp1 opp2 : binop X)
(is : iscommringops opp1 opp2) : iscommrigops opp1 opp2 :=
make_dirprod (isringopstoisrigops _ _ _ (pr1 is)) (pr2 is).
Coercion iscommringopstoiscommrigops : iscommringops >-> iscommrigops.
Lemma isassoc_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) :
isassoc opp → isassoc (binop_weq_fwd H opp).
Show proof.
intros is x y z.
apply (maponpaths H).
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply (maponpaths (λ x, opp x _)).
apply homotinvweqweq.
- apply maponpaths.
apply homotinvweqweq0.
apply (maponpaths H).
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply (maponpaths (λ x, opp x _)).
apply homotinvweqweq.
- apply maponpaths.
apply homotinvweqweq0.
Lemma islunit_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (x0 : X) :
islunit opp x0 → islunit (binop_weq_fwd H opp) (H x0).
Show proof.
intros is y.
unfold binop_weq_fwd.
refine (pathscomp0 (maponpaths _ _) _).
- refine (pathscomp0 (maponpaths (λ x, opp x _) _) _).
+ apply homotinvweqweq.
+ apply is.
- apply homotweqinvweq.
unfold binop_weq_fwd.
refine (pathscomp0 (maponpaths _ _) _).
- refine (pathscomp0 (maponpaths (λ x, opp x _) _) _).
+ apply homotinvweqweq.
+ apply is.
- apply homotweqinvweq.
Lemma isrunit_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (x0 : X) :
isrunit opp x0 → isrunit (binop_weq_fwd H opp) (H x0).
Show proof.
intros is y.
unfold binop_weq_fwd.
refine (pathscomp0 (maponpaths _ _) _).
- refine (pathscomp0 (maponpaths (opp _) _) _).
+ apply homotinvweqweq.
+ apply is.
- apply homotweqinvweq.
unfold binop_weq_fwd.
refine (pathscomp0 (maponpaths _ _) _).
- refine (pathscomp0 (maponpaths (opp _) _) _).
+ apply homotinvweqweq.
+ apply is.
- apply homotweqinvweq.
Lemma isunit_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (x0 : X) :
isunit opp x0 → isunit (binop_weq_fwd H opp) (H x0).
Show proof.
Lemma isunital_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) :
isunital opp → isunital (binop_weq_fwd H opp).
Show proof.
Lemma ismonoidop_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) :
ismonoidop opp → ismonoidop (binop_weq_fwd H opp).
Show proof.
Lemma islinv_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (x0 : X) (inv : X → X) :
islinv opp x0 inv → islinv (binop_weq_fwd H opp) (H x0) (λ y : Y, H (inv (invmap H y))).
Show proof.
intros is y.
unfold binop_weq_fwd.
apply maponpaths.
refine (pathscomp0 _ (is _)).
apply (maponpaths (λ x, opp x _)).
apply homotinvweqweq.
Lemma isrinv_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (x0 : X) (inv : X → X) :unfold binop_weq_fwd.
apply maponpaths.
refine (pathscomp0 _ (is _)).
apply (maponpaths (λ x, opp x _)).
apply homotinvweqweq.
isrinv opp x0 inv → isrinv (binop_weq_fwd H opp) (H x0) (λ y : Y, H (inv (invmap H y))).
Show proof.
intros is y.
unfold binop_weq_fwd.
apply maponpaths.
refine (pathscomp0 _ (is _)).
apply (maponpaths (opp _)).
apply homotinvweqweq.
Lemma isinv_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (x0 : X) (inv : X → X) :unfold binop_weq_fwd.
apply maponpaths.
refine (pathscomp0 _ (is _)).
apply (maponpaths (opp _)).
apply homotinvweqweq.
isinv opp x0 inv → isinv (binop_weq_fwd H opp) (H x0) (λ y : Y, H (inv (invmap H y))).
Show proof.
Lemma invstruct_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) (is : ismonoidop opp) :
invstruct opp is → invstruct (binop_weq_fwd H opp) (ismonoidop_weq_fwd H opp is).
Show proof.
Lemma isgrop_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) :
isgrop opp → isgrop (binop_weq_fwd H opp).
Show proof.
Lemma iscomm_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) :
iscomm opp → iscomm (binop_weq_fwd H opp).
Show proof.
Lemma isabmonoidop_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) :
isabmonoidop opp → isabmonoidop (binop_weq_fwd H opp).
Show proof.
Lemma isabgrop_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) :
isabgrop opp → isabgrop (binop_weq_fwd H opp).
Show proof.
Lemma isldistr_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) :
isldistr op1 op2 → isldistr (binop_weq_fwd H op1) (binop_weq_fwd H op2).
Show proof.
intros is x y z.
unfold binop_weq_fwd.
apply maponpaths.
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply maponpaths.
apply homotinvweqweq.
- apply map_on_two_paths ; apply homotinvweqweq0.
Lemma isrdistr_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) :unfold binop_weq_fwd.
apply maponpaths.
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply maponpaths.
apply homotinvweqweq.
- apply map_on_two_paths ; apply homotinvweqweq0.
isrdistr op1 op2 → isrdistr (binop_weq_fwd H op1) (binop_weq_fwd H op2).
Show proof.
intros is x y z.
unfold binop_weq_fwd.
apply maponpaths.
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply (maponpaths (λ x, op2 x _)).
apply homotinvweqweq.
- apply map_on_two_paths ; apply homotinvweqweq0.
unfold binop_weq_fwd.
apply maponpaths.
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply (maponpaths (λ x, op2 x _)).
apply homotinvweqweq.
- apply map_on_two_paths ; apply homotinvweqweq0.
Lemma isdistr_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) :
isdistr op1 op2 → isdistr (binop_weq_fwd H op1) (binop_weq_fwd H op2).
Show proof.
Lemma isabsorb_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) :
isabsorb op1 op2 → isabsorb (binop_weq_fwd H op1) (binop_weq_fwd H op2).
Show proof.
intros is x y.
unfold binop_weq_fwd.
refine (pathscomp0 _ (homotweqinvweq H _)).
apply maponpaths.
refine (pathscomp0 _ (is _ _)).
apply maponpaths.
apply (homotinvweqweq H).
unfold binop_weq_fwd.
refine (pathscomp0 _ (homotweqinvweq H _)).
apply maponpaths.
refine (pathscomp0 _ (is _ _)).
apply maponpaths.
apply (homotinvweqweq H).
Lemma isrigops_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) :
isrigops op1 op2 → isrigops (binop_weq_fwd H op1) (binop_weq_fwd H op2).
Show proof.
intro is.
split.
- use tpair.
+ split.
apply isabmonoidop_weq_fwd, (pr1 (pr1 (pr1 is))).
apply ismonoidop_weq_fwd, (pr2 (pr1 (pr1 is))).
+ split ; simpl.
* intros x.
apply (maponpaths H).
refine (pathscomp0 _ (pr1 (pr2 (pr1 is)) _)).
apply (maponpaths (λ x, op2 x _)).
apply homotinvweqweq.
* intros x.
apply (maponpaths H).
refine (pathscomp0 _ (pr2 (pr2 (pr1 is)) _)).
apply (maponpaths (op2 _)).
apply homotinvweqweq.
- apply isdistr_weq_fwd, (pr2 is).
split.
- use tpair.
+ split.
apply isabmonoidop_weq_fwd, (pr1 (pr1 (pr1 is))).
apply ismonoidop_weq_fwd, (pr2 (pr1 (pr1 is))).
+ split ; simpl.
* intros x.
apply (maponpaths H).
refine (pathscomp0 _ (pr1 (pr2 (pr1 is)) _)).
apply (maponpaths (λ x, op2 x _)).
apply homotinvweqweq.
* intros x.
apply (maponpaths H).
refine (pathscomp0 _ (pr2 (pr2 (pr1 is)) _)).
apply (maponpaths (op2 _)).
apply homotinvweqweq.
- apply isdistr_weq_fwd, (pr2 is).
Lemma isringops_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) :
isringops op1 op2 → isringops (binop_weq_fwd H op1) (binop_weq_fwd H op2).
Show proof.
intro is.
split.
- split.
+ apply isabgrop_weq_fwd, (pr1 (pr1 is)).
+ apply ismonoidop_weq_fwd, (pr2 (pr1 is)).
- apply isdistr_weq_fwd, (pr2 is).
split.
- split.
+ apply isabgrop_weq_fwd, (pr1 (pr1 is)).
+ apply ismonoidop_weq_fwd, (pr2 (pr1 is)).
- apply isdistr_weq_fwd, (pr2 is).
Lemma iscommrigops_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) :
iscommrigops op1 op2 → iscommrigops (binop_weq_fwd H op1) (binop_weq_fwd H op2).
Show proof.
Lemma iscommringops_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) :
iscommringops op1 op2 → iscommringops (binop_weq_fwd H op1) (binop_weq_fwd H op2).
Show proof.
binop_weq_bck
Lemma isassoc_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) :
isassoc opp → isassoc (binop_weq_bck H opp).
Show proof.
intros is x y z.
apply (maponpaths (invmap H)).
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply (maponpaths (λ x, opp x _)).
apply homotweqinvweq.
- apply maponpaths.
apply pathsinv0, homotweqinvweq.
Lemma islunit_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (x0 : Y) :apply (maponpaths (invmap H)).
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply (maponpaths (λ x, opp x _)).
apply homotweqinvweq.
- apply maponpaths.
apply pathsinv0, homotweqinvweq.
islunit opp x0 → islunit (binop_weq_bck H opp) (invmap H x0).
Show proof.
intros is y.
unfold binop_weq_bck.
refine (pathscomp0 (maponpaths _ _) _).
- refine (pathscomp0 (maponpaths (λ x, opp x _) _) _).
+ apply homotweqinvweq.
+ apply is.
- apply homotinvweqweq.
Lemma isrunit_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (x0 : Y) :unfold binop_weq_bck.
refine (pathscomp0 (maponpaths _ _) _).
- refine (pathscomp0 (maponpaths (λ x, opp x _) _) _).
+ apply homotweqinvweq.
+ apply is.
- apply homotinvweqweq.
isrunit opp x0 → isrunit (binop_weq_bck H opp) (invmap H x0).
Show proof.
intros is y.
unfold binop_weq_bck.
refine (pathscomp0 (maponpaths _ _) _).
- refine (pathscomp0 (maponpaths (opp _) _) _).
+ apply homotweqinvweq.
+ apply is.
- apply homotinvweqweq.
Lemma isunit_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (x0 : Y) :unfold binop_weq_bck.
refine (pathscomp0 (maponpaths _ _) _).
- refine (pathscomp0 (maponpaths (opp _) _) _).
+ apply homotweqinvweq.
+ apply is.
- apply homotinvweqweq.
isunit opp x0 → isunit (binop_weq_bck H opp) (invmap H x0).
Show proof.
Lemma isunital_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) :
isunital opp → isunital (binop_weq_bck H opp).
Show proof.
Lemma ismonoidop_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) :
ismonoidop opp → ismonoidop (binop_weq_bck H opp).
Show proof.
Lemma islinv_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (x0 : Y) (inv : Y → Y) :
islinv opp x0 inv → islinv (binop_weq_bck H opp) (invmap H x0) (λ y : X, invmap H (inv (H y))).
Show proof.
intros is y.
unfold binop_weq_bck.
apply maponpaths.
refine (pathscomp0 _ (is _)).
apply (maponpaths (λ x, opp x _)).
apply homotweqinvweq.
Lemma isrinv_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (x0 : Y) (inv : Y → Y) :unfold binop_weq_bck.
apply maponpaths.
refine (pathscomp0 _ (is _)).
apply (maponpaths (λ x, opp x _)).
apply homotweqinvweq.
isrinv opp x0 inv → isrinv (binop_weq_bck H opp) (invmap H x0) (λ y : X, invmap H (inv (H y))).
Show proof.
intros is y.
unfold binop_weq_bck.
apply maponpaths.
refine (pathscomp0 _ (is _)).
apply (maponpaths (opp _)).
apply homotweqinvweq.
Lemma isinv_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (x0 : Y) (inv : Y → Y) :unfold binop_weq_bck.
apply maponpaths.
refine (pathscomp0 _ (is _)).
apply (maponpaths (opp _)).
apply homotweqinvweq.
isinv opp x0 inv → isinv (binop_weq_bck H opp) (invmap H x0) (λ y : X, invmap H (inv (H y))).
Show proof.
Lemma invstruct_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) (is : ismonoidop opp) :
invstruct opp is → invstruct (binop_weq_bck H opp) (ismonoidop_weq_bck H opp is).
Show proof.
Lemma isgrop_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) :
isgrop opp → isgrop (binop_weq_bck H opp).
Show proof.
Lemma iscomm_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) :
iscomm opp → iscomm (binop_weq_bck H opp).
Show proof.
Lemma isabmonoidop_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) :
isabmonoidop opp → isabmonoidop (binop_weq_bck H opp).
Show proof.
Lemma isabgrop_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) :
isabgrop opp → isabgrop (binop_weq_bck H opp).
Show proof.
Lemma isldistr_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) :
isldistr op1 op2 → isldistr (binop_weq_bck H op1) (binop_weq_bck H op2).
Show proof.
intros is x y z.
unfold binop_weq_bck.
apply maponpaths.
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply maponpaths.
apply homotweqinvweq.
- apply map_on_two_paths ; apply pathsinv0, homotweqinvweq.
Lemma isrdistr_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) :unfold binop_weq_bck.
apply maponpaths.
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply maponpaths.
apply homotweqinvweq.
- apply map_on_two_paths ; apply pathsinv0, homotweqinvweq.
isrdistr op1 op2 → isrdistr (binop_weq_bck H op1) (binop_weq_bck H op2).
Show proof.
intros is x y z.
unfold binop_weq_bck.
apply maponpaths.
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply (maponpaths (λ x, op2 x _)).
apply homotweqinvweq.
- apply map_on_two_paths ; apply pathsinv0, homotweqinvweq.
unfold binop_weq_bck.
apply maponpaths.
refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)).
- apply (maponpaths (λ x, op2 x _)).
apply homotweqinvweq.
- apply map_on_two_paths ; apply pathsinv0, homotweqinvweq.
Lemma isdistr_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) :
isdistr op1 op2 → isdistr (binop_weq_bck H op1) (binop_weq_bck H op2).
Show proof.
Lemma isabsorb_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) :
isabsorb op1 op2 → isabsorb (binop_weq_bck H op1) (binop_weq_bck H op2).
Show proof.
intros is x y.
unfold binop_weq_bck.
refine (pathscomp0 _ (homotinvweqweq H _)).
apply maponpaths.
refine (pathscomp0 _ (is _ _)).
apply maponpaths.
apply (homotweqinvweq H).
unfold binop_weq_bck.
refine (pathscomp0 _ (homotinvweqweq H _)).
apply maponpaths.
refine (pathscomp0 _ (is _ _)).
apply maponpaths.
apply (homotweqinvweq H).
Lemma isrigops_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) :
isrigops op1 op2 → isrigops (binop_weq_bck H op1) (binop_weq_bck H op2).
Show proof.
intro is.
split.
- use tpair.
+ split.
apply isabmonoidop_weq_bck, (pr1 (pr1 (pr1 is))).
apply ismonoidop_weq_bck, (pr2 (pr1 (pr1 is))).
+ split ; simpl.
* intros x.
apply (maponpaths (invmap H)).
refine (pathscomp0 _ (pr1 (pr2 (pr1 is)) _)).
apply (maponpaths (λ x, op2 x _)).
apply homotweqinvweq.
* intros x.
apply (maponpaths (invmap H)).
refine (pathscomp0 _ (pr2 (pr2 (pr1 is)) _)).
apply (maponpaths (op2 _)).
apply homotweqinvweq.
- apply isdistr_weq_bck, (pr2 is).
split.
- use tpair.
+ split.
apply isabmonoidop_weq_bck, (pr1 (pr1 (pr1 is))).
apply ismonoidop_weq_bck, (pr2 (pr1 (pr1 is))).
+ split ; simpl.
* intros x.
apply (maponpaths (invmap H)).
refine (pathscomp0 _ (pr1 (pr2 (pr1 is)) _)).
apply (maponpaths (λ x, op2 x _)).
apply homotweqinvweq.
* intros x.
apply (maponpaths (invmap H)).
refine (pathscomp0 _ (pr2 (pr2 (pr1 is)) _)).
apply (maponpaths (op2 _)).
apply homotweqinvweq.
- apply isdistr_weq_bck, (pr2 is).
Lemma isringops_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) :
isringops op1 op2 → isringops (binop_weq_bck H op1) (binop_weq_bck H op2).
Show proof.
intro is.
split.
- split.
+ apply isabgrop_weq_bck, (pr1 (pr1 is)).
+ apply ismonoidop_weq_bck, (pr2 (pr1 is)).
- apply isdistr_weq_bck, (pr2 is).
split.
- split.
+ apply isabgrop_weq_bck, (pr1 (pr1 is)).
+ apply ismonoidop_weq_bck, (pr2 (pr1 is)).
- apply isdistr_weq_bck, (pr2 is).
Lemma iscommrigops_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) :
iscommrigops op1 op2 → iscommrigops (binop_weq_bck H op1) (binop_weq_bck H op2).
Show proof.
Lemma iscommringops_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) :
iscommringops op1 op2 → iscommringops (binop_weq_bck H op1) (binop_weq_bck H op2).
Show proof.
Definition setwithbinop : UU := total2 (λ X : hSet, binop X).
Definition make_setwithbinop (X : hSet) (opp : binop X) : setwithbinop :=
tpair (λ X : hSet, binop X) X opp.
Definition pr1setwithbinop : setwithbinop -> hSet := @pr1 _ (λ X : hSet, binop X).
Coercion pr1setwithbinop : setwithbinop >-> hSet.
Definition op {X : setwithbinop} : binop X := pr2 X.
Definition isasetbinoponhSet (X : hSet) : isaset (@binop X).
Show proof.
Opaque isasetbinoponhSet.
Declare Scope addoperation_scope.
Delimit Scope addoperation_scope with addoperation.
Notation "x + y" := (op x y) : addoperation_scope.
Declare Scope multoperation_scope.
Delimit Scope multoperation_scope with multoperation.
Notation "x * y" := (op x y) : multoperation_scope.
Definition setwithbinop_rev (X : setwithbinop) : setwithbinop :=
make_setwithbinop X (λ x y, op y x).
Definition isbinopfun {X Y : setwithbinop} (f : X -> Y) : UU :=
∏ x x' : X, paths (f (op x x')) (op (f x) (f x')).
Definition make_isbinopfun {X Y : setwithbinop} {f : X -> Y}
(H : ∏ x x' : X, f (op x x') = op (f x) (f x')) : isbinopfun f := H.
Lemma isapropisbinopfun {X Y : setwithbinop} (f : X -> Y) : isaprop (isbinopfun f).
Show proof.
Definition isbinopfun_twooutof3b {A B C : setwithbinop} (f : A -> B) (g : B -> C)
(H : issurjective f) : isbinopfun (g ∘ f)%functions -> isbinopfun f -> isbinopfun g.
Show proof.
intros H1 H2.
use make_isbinopfun.
intros b1 b2.
use (squash_to_prop (H b1) (@setproperty C _ _)). intros H1'.
use (squash_to_prop (H b2) (@setproperty C _ _)). intros H2'.
rewrite <- (hfiberpr2 _ _ H1'). rewrite <- (hfiberpr2 _ _ H2').
use (pathscomp0
(! (maponpaths (λ b : B, g b) (H2 (hfiberpr1 f b1 H1') (hfiberpr1 f b2 H2'))))).
exact (H1 (hfiberpr1 f b1 H1') (hfiberpr1 f b2 H2')).
use make_isbinopfun.
intros b1 b2.
use (squash_to_prop (H b1) (@setproperty C _ _)). intros H1'.
use (squash_to_prop (H b2) (@setproperty C _ _)). intros H2'.
rewrite <- (hfiberpr2 _ _ H1'). rewrite <- (hfiberpr2 _ _ H2').
use (pathscomp0
(! (maponpaths (λ b : B, g b) (H2 (hfiberpr1 f b1 H1') (hfiberpr1 f b2 H2'))))).
exact (H1 (hfiberpr1 f b1 H1') (hfiberpr1 f b2 H2')).
Definition binopfun (X Y : setwithbinop) : UU := total2 (fun f : X -> Y => isbinopfun f).
Definition make_binopfun {X Y : setwithbinop} (f : X -> Y) (is : isbinopfun f) : binopfun X Y :=
tpair _ f is.
Definition pr1binopfun (X Y : setwithbinop) : binopfun X Y -> (X -> Y) := @pr1 _ _.
Coercion pr1binopfun : binopfun >-> Funclass.
Definition binopfunisbinopfun {X Y : setwithbinop} (f : binopfun X Y) : isbinopfun f := pr2 f.
Lemma isasetbinopfun (X Y : setwithbinop) : isaset (binopfun X Y).
Show proof.
apply (isasetsubset (pr1binopfun X Y)).
- change (isofhlevel 2 (X -> Y)).
apply impred. intro.
apply (setproperty Y).
- refine (isinclpr1 _ _). intro.
apply isapropisbinopfun.
- change (isofhlevel 2 (X -> Y)).
apply impred. intro.
apply (setproperty Y).
- refine (isinclpr1 _ _). intro.
apply isapropisbinopfun.
Lemma isbinopfuncomp {X Y Z : setwithbinop} (f : binopfun X Y) (g : binopfun Y Z) :
isbinopfun (funcomp (pr1 f) (pr1 g)).
Show proof.
set (axf := pr2 f). set (axg := pr2 g).
intros a b. simpl.
rewrite (axf a b). rewrite (axg (pr1 f a) (pr1 f b)).
apply idpath.
Opaque isbinopfuncomp.intros a b. simpl.
rewrite (axf a b). rewrite (axg (pr1 f a) (pr1 f b)).
apply idpath.
Definition binopfuncomp {X Y Z : setwithbinop} (f : binopfun X Y) (g : binopfun Y Z) :
binopfun X Z := make_binopfun (funcomp (pr1 f) (pr1 g)) (isbinopfuncomp f g).
Definition binopmono (X Y : setwithbinop) : UU := total2 (λ f : incl X Y, isbinopfun (pr1 f)).
Definition make_binopmono {X Y : setwithbinop} (f : incl X Y) (is : isbinopfun f) :
binopmono X Y := tpair _ f is.
Definition pr1binopmono (X Y : setwithbinop) : binopmono X Y -> incl X Y := @pr1 _ _.
Coercion pr1binopmono : binopmono >-> incl.
Definition binopincltobinopfun (X Y : setwithbinop) :
binopmono X Y -> binopfun X Y := λ f, make_binopfun (pr1 (pr1 f)) (pr2 f).
Coercion binopincltobinopfun : binopmono >-> binopfun.
Definition binopmonocomp {X Y Z : setwithbinop} (f : binopmono X Y) (g : binopmono Y Z) :
binopmono X Z := make_binopmono (inclcomp (pr1 f) (pr1 g)) (isbinopfuncomp f g).
Definition binopiso (X Y : setwithbinop) : UU := total2 (λ f : X ≃ Y, isbinopfun f).
Definition make_binopiso {X Y : setwithbinop} (f : X ≃ Y) (is : isbinopfun f) :
binopiso X Y := tpair _ f is.
Definition pr1binopiso (X Y : setwithbinop) : binopiso X Y -> X ≃ Y := @pr1 _ _.
Coercion pr1binopiso : binopiso >-> weq.
Lemma isasetbinopiso (X Y : setwithbinop) : isaset (binopiso X Y).
Show proof.
use isaset_total2.
- use isaset_total2.
+ use impred_isaset. intros t. use setproperty.
+ intros x. use isasetaprop. use isapropisweq.
- intros w. use isasetaprop. use isapropisbinopfun.
Opaque isasetbinopiso.- use isaset_total2.
+ use impred_isaset. intros t. use setproperty.
+ intros x. use isasetaprop. use isapropisweq.
- intros w. use isasetaprop. use isapropisbinopfun.
Definition binopisotobinopmono (X Y : setwithbinop) :
binopiso X Y -> binopmono X Y := λ f, make_binopmono (weqtoincl (pr1 f)) (pr2 f).
Coercion binopisotobinopmono : binopiso >-> binopmono.
Definition binopisocomp {X Y Z : setwithbinop} (f : binopiso X Y) (g : binopiso Y Z) :
binopiso X Z := make_binopiso (weqcomp (pr1 f) (pr1 g)) (isbinopfuncomp f g).
Lemma isbinopfuninvmap {X Y : setwithbinop} (f : binopiso X Y) : isbinopfun (invmap (pr1 f)).
Show proof.
set (axf := pr2 f). intros a b.
apply (invmaponpathsweq (pr1 f)).
rewrite (homotweqinvweq (pr1 f) (op a b)).
rewrite (axf (invmap (pr1 f) a) (invmap (pr1 f) b)).
rewrite (homotweqinvweq (pr1 f) a).
rewrite (homotweqinvweq (pr1 f) b).
apply idpath.
Opaque isbinopfuninvmap.apply (invmaponpathsweq (pr1 f)).
rewrite (homotweqinvweq (pr1 f) (op a b)).
rewrite (axf (invmap (pr1 f) a) (invmap (pr1 f) b)).
rewrite (homotweqinvweq (pr1 f) a).
rewrite (homotweqinvweq (pr1 f) b).
apply idpath.
Definition invbinopiso {X Y : setwithbinop} (f : binopiso X Y) :
binopiso Y X := make_binopiso (invweq (pr1 f)) (isbinopfuninvmap f).
Definition idbinopiso (X : setwithbinop) : binopiso X X.
Show proof.
Definition setwithbinop_univalence_weq1 (X Y : setwithbinop) : (X = Y) ≃ (X ╝ Y) :=
total2_paths_equiv _ X Y.
Definition setwithbinop_univalence_weq2 (X Y : setwithbinop) : (X ╝ Y) ≃ (binopiso X Y).
Show proof.
use weqbandf.
- use hSet_univalence.
- intros e. use invweq. induction X as [X Xop]. induction Y as [Y Yop]. cbn in e.
induction e. use weqimplimpl.
+ intros i.
use funextfun. intros x1.
use funextfun. intros x2.
exact (i x1 x2).
+ intros e. cbn in e. intros x1 x2. induction e. use idpath.
+ use isapropisbinopfun.
+ use isasetbinoponhSet.
- use hSet_univalence.
- intros e. use invweq. induction X as [X Xop]. induction Y as [Y Yop]. cbn in e.
induction e. use weqimplimpl.
+ intros i.
use funextfun. intros x1.
use funextfun. intros x2.
exact (i x1 x2).
+ intros e. cbn in e. intros x1 x2. induction e. use idpath.
+ use isapropisbinopfun.
+ use isasetbinoponhSet.
Definition setwithbinop_univalence_map (X Y : setwithbinop) : X = Y -> binopiso X Y.
Show proof.
Lemma setwithbinop_univalence_isweq (X Y : setwithbinop) :
isweq (setwithbinop_univalence_map X Y).
Show proof.
use isweqhomot.
- exact (weqcomp (setwithbinop_univalence_weq1 X Y) (setwithbinop_univalence_weq2 X Y)).
- intros e. induction e. use weqcomp_to_funcomp_app.
- use weqproperty.
Opaque setwithbinop_univalence_isweq.- exact (weqcomp (setwithbinop_univalence_weq1 X Y) (setwithbinop_univalence_weq2 X Y)).
- intros e. induction e. use weqcomp_to_funcomp_app.
- use weqproperty.
Definition setwithbinop_univalence (X Y : setwithbinop) : (X = Y) ≃ (binopiso X Y).
Show proof.
use make_weq.
- exact (setwithbinop_univalence_map X Y).
- exact (setwithbinop_univalence_isweq X Y).
Opaque setwithbinop_univalence.- exact (setwithbinop_univalence_map X Y).
- exact (setwithbinop_univalence_isweq X Y).
Local Lemma hfiberbinop_path {A B : setwithbinop} (f : binopfun A B) (b1 b2 : B)
(hf1 : hfiber (pr1 f) b1) (hf2 : hfiber (pr1 f) b2) :
pr1 f (@op A (pr1 hf1) (pr1 hf2)) = (@op B b1 b2).
Show proof.
Definition hfiberbinop {A B : setwithbinop} (f : binopfun A B) (b1 b2 : B)
(hf1 : hfiber (pr1 f) b1) (hf2 : hfiber (pr1 f) b2) :
hfiber (pr1 f) (@op B b1 b2) :=
make_hfiber (pr1 f) (@op A (pr1 hf1) (pr1 hf2)) (hfiberbinop_path f b1 b2 hf1 hf2).
(hf1 : hfiber (pr1 f) b1) (hf2 : hfiber (pr1 f) b2) :
pr1 f (@op A (pr1 hf1) (pr1 hf2)) = (@op B b1 b2).
Show proof.
use (pathscomp0 (binopfunisbinopfun f _ _)).
rewrite <- (hfiberpr2 _ _ hf1). rewrite <- (hfiberpr2 _ _ hf2). use idpath.
rewrite <- (hfiberpr2 _ _ hf1). rewrite <- (hfiberpr2 _ _ hf2). use idpath.
Definition hfiberbinop {A B : setwithbinop} (f : binopfun A B) (b1 b2 : B)
(hf1 : hfiber (pr1 f) b1) (hf2 : hfiber (pr1 f) b2) :
hfiber (pr1 f) (@op B b1 b2) :=
make_hfiber (pr1 f) (@op A (pr1 hf1) (pr1 hf2)) (hfiberbinop_path f b1 b2 hf1 hf2).
Lemma islcancelablemonob {X Y : setwithbinop} (f : binopmono X Y) (x : X)
(is : islcancelable (@op Y) (f x)) : islcancelable (@op X) x.
Show proof.
unfold islcancelable.
apply (isincltwooutof3a (λ x0 : X, op x x0) f (pr2 (pr1 f))).
assert (h : homot (funcomp f (λ y0 : Y, op (f x) y0)) (funcomp (λ x0 : X, op x x0) f)).
{
intro x0; simpl. apply (pathsinv0 ((pr2 f) x x0)).
}
apply (isinclhomot _ _ h).
apply (isinclcomp f (make_incl _ is)).
apply (isincltwooutof3a (λ x0 : X, op x x0) f (pr2 (pr1 f))).
assert (h : homot (funcomp f (λ y0 : Y, op (f x) y0)) (funcomp (λ x0 : X, op x x0) f)).
{
intro x0; simpl. apply (pathsinv0 ((pr2 f) x x0)).
}
apply (isinclhomot _ _ h).
apply (isinclcomp f (make_incl _ is)).
Lemma isrcancelablemonob {X Y : setwithbinop} (f : binopmono X Y) (x : X)
(is : isrcancelable (@op Y) (f x)) : isrcancelable (@op X) x.
Show proof.
unfold islcancelable.
apply (isincltwooutof3a (λ x0 : X, op x0 x) f (pr2 (pr1 f))).
assert (h : homot (funcomp f (λ y0 : Y, op y0 (f x))) (funcomp (λ x0 : X, op x0 x) f)).
{
intro x0; simpl. apply (pathsinv0 ((pr2 f) x0 x)).
}
apply (isinclhomot _ _ h). apply (isinclcomp f (make_incl _ is)).
apply (isincltwooutof3a (λ x0 : X, op x0 x) f (pr2 (pr1 f))).
assert (h : homot (funcomp f (λ y0 : Y, op y0 (f x))) (funcomp (λ x0 : X, op x0 x) f)).
{
intro x0; simpl. apply (pathsinv0 ((pr2 f) x0 x)).
}
apply (isinclhomot _ _ h). apply (isinclcomp f (make_incl _ is)).
Lemma iscancelablemonob {X Y : setwithbinop} (f : binopmono X Y) (x : X)
(is : iscancelable (@op Y) (f x)) : iscancelable (@op X) x.
Show proof.
Notation islcancelableisob := islcancelablemonob.
Notation isrcancelableisob := isrcancelablemonob.
Notation iscancelableisob := iscancelablemonob.
Lemma islinvertibleisob {X Y : setwithbinop} (f : binopiso X Y) (x : X)
(is : islinvertible (@op Y) (f x)) : islinvertible (@op X) x.
Show proof.
unfold islinvertible. apply (twooutof3a (λ x0 : X, op x x0) f).
- assert (h : homot (funcomp f (λ y0 : Y, op (f x) y0)) (funcomp (λ x0 : X, op x x0) f)).
{
intro x0; simpl. apply (pathsinv0 ((pr2 f) x x0)).
}
apply (isweqhomot _ _ h). apply (pr2 (weqcomp f (make_weq _ is))).
- apply (pr2 (pr1 f)).
- assert (h : homot (funcomp f (λ y0 : Y, op (f x) y0)) (funcomp (λ x0 : X, op x x0) f)).
{
intro x0; simpl. apply (pathsinv0 ((pr2 f) x x0)).
}
apply (isweqhomot _ _ h). apply (pr2 (weqcomp f (make_weq _ is))).
- apply (pr2 (pr1 f)).
Lemma isrinvertibleisob {X Y : setwithbinop} (f : binopiso X Y) (x : X)
(is : isrinvertible (@op Y) (f x)) : isrinvertible (@op X) x.
Show proof.
unfold islinvertible. apply (twooutof3a (λ x0 : X, op x0 x) f).
- assert (h : homot (funcomp f (λ y0 : Y, op y0 (f x))) (funcomp (λ x0 : X, op x0 x) f)).
{
intro x0; simpl. apply (pathsinv0 ((pr2 f) x0 x)).
}
apply (isweqhomot _ _ h). apply (pr2 (weqcomp f (make_weq _ is))).
- apply (pr2 (pr1 f)).
- assert (h : homot (funcomp f (λ y0 : Y, op y0 (f x))) (funcomp (λ x0 : X, op x0 x) f)).
{
intro x0; simpl. apply (pathsinv0 ((pr2 f) x0 x)).
}
apply (isweqhomot _ _ h). apply (pr2 (weqcomp f (make_weq _ is))).
- apply (pr2 (pr1 f)).
Lemma isinvertiblemonob {X Y : setwithbinop} (f : binopiso X Y) (x : X)
(is : isinvertible (@op Y) (f x)) : isinvertible (@op X) x.
Show proof.
Definition islinvertibleisof {X Y : setwithbinop} (f : binopiso X Y) (x : X)
(is : islinvertible (@op X) x) : islinvertible (@op Y) (f x).
Show proof.
unfold islinvertible. apply (twooutof3b f).
- apply (pr2 (pr1 f)).
- assert (h : homot (funcomp (λ x0 : X, op x x0) f) (λ x0 : X, op (f x) (f x0))).
{
intro x0; simpl. apply (pr2 f x x0).
}
apply (isweqhomot _ _ h). apply (pr2 (weqcomp (make_weq _ is) f)).
- apply (pr2 (pr1 f)).
- assert (h : homot (funcomp (λ x0 : X, op x x0) f) (λ x0 : X, op (f x) (f x0))).
{
intro x0; simpl. apply (pr2 f x x0).
}
apply (isweqhomot _ _ h). apply (pr2 (weqcomp (make_weq _ is) f)).
Definition isrinvertibleisof {X Y : setwithbinop} (f : binopiso X Y) (x : X)
(is : isrinvertible (@op X) x) : isrinvertible (@op Y) (f x).
Show proof.
unfold isrinvertible. apply (twooutof3b f).
- apply (pr2 (pr1 f)).
- assert (h : homot (funcomp (λ x0 : X, op x0 x) f) (λ x0 : X, op (f x0) (f x))).
{
intro x0; simpl. apply (pr2 f x0 x).
}
apply (isweqhomot _ _ h). apply (pr2 (weqcomp (make_weq _ is) f)).
- apply (pr2 (pr1 f)).
- assert (h : homot (funcomp (λ x0 : X, op x0 x) f) (λ x0 : X, op (f x0) (f x))).
{
intro x0; simpl. apply (pr2 f x0 x).
}
apply (isweqhomot _ _ h). apply (pr2 (weqcomp (make_weq _ is) f)).
Lemma isinvertiblemonof {X Y : setwithbinop} (f : binopiso X Y) (x : X)
(is : isinvertible (@op X) x) : isinvertible (@op Y) (f x).
Show proof.
Lemma isassocmonob {X Y : setwithbinop} (f : binopmono X Y) (is : isassoc (@op Y)) :
isassoc (@op X).
Show proof.
set (axf := pr2 f). simpl in axf. intros a b c.
apply (invmaponpathsincl _ (pr2 (pr1 f))).
rewrite (axf (op a b) c). rewrite (axf a b).
rewrite (axf a (op b c)). rewrite (axf b c). apply is.
Opaque isassocmonob.apply (invmaponpathsincl _ (pr2 (pr1 f))).
rewrite (axf (op a b) c). rewrite (axf a b).
rewrite (axf a (op b c)). rewrite (axf b c). apply is.
Lemma iscommmonob {X Y : setwithbinop} (f : binopmono X Y) (is : iscomm (@op Y)) : iscomm (@op X).
Show proof.
set (axf := pr2 f). simpl in axf. intros a b.
apply (invmaponpathsincl _ (pr2 (pr1 f))).
rewrite (axf a b). rewrite (axf b a). apply is.
Opaque iscommmonob.apply (invmaponpathsincl _ (pr2 (pr1 f))).
rewrite (axf a b). rewrite (axf b a). apply is.
Notation isassocisob := isassocmonob.
Notation iscommisob := iscommmonob.
Lemma isassocisof {X Y : setwithbinop} (f : binopiso X Y) (is : isassoc (@op X)) : isassoc (@op Y).
Show proof.
Opaque isassocisof.
Lemma iscommisof {X Y : setwithbinop} (f : binopiso X Y) (is : iscomm (@op X)) : iscomm (@op Y).
Show proof.
Opaque iscommisof.
Lemma isunitisof {X Y : setwithbinop} (f : binopiso X Y) (unx : X) (is : isunit (@op X) unx) :
isunit (@op Y) (f unx).
Show proof.
set (axf := pr2 f). split.
- intro a. change (f unx) with (pr1 f unx).
apply (invmaponpathsweq (pr1 (invbinopiso f))).
rewrite (pr2 (invbinopiso f) (pr1 f unx) a). simpl.
rewrite (homotinvweqweq (pr1 f) unx). apply (pr1 is).
- intro a. change (f unx) with (pr1 f unx).
apply (invmaponpathsweq (pr1 (invbinopiso f))).
rewrite (pr2 (invbinopiso f) a (pr1 f unx)). simpl.
rewrite (homotinvweqweq (pr1 f) unx). apply (pr2 is).
Opaque isunitisof.- intro a. change (f unx) with (pr1 f unx).
apply (invmaponpathsweq (pr1 (invbinopiso f))).
rewrite (pr2 (invbinopiso f) (pr1 f unx) a). simpl.
rewrite (homotinvweqweq (pr1 f) unx). apply (pr1 is).
- intro a. change (f unx) with (pr1 f unx).
apply (invmaponpathsweq (pr1 (invbinopiso f))).
rewrite (pr2 (invbinopiso f) a (pr1 f unx)). simpl.
rewrite (homotinvweqweq (pr1 f) unx). apply (pr2 is).
Definition isunitalisof {X Y : setwithbinop} (f : binopiso X Y) (is : isunital (@op X)) :
isunital (@op Y) := make_isunital (f (pr1 is)) (isunitisof f (pr1 is) (pr2 is)).
Lemma isunitisob {X Y : setwithbinop} (f : binopiso X Y) (uny : Y) (is : isunit (@op Y) uny) :
isunit (@op X) ((invmap f) uny).
Show proof.
Opaque isunitisob.
Definition isunitalisob {X Y : setwithbinop} (f : binopiso X Y) (is : isunital (@op Y)) :
isunital (@op X) := make_isunital ((invmap f) (pr1 is)) (isunitisob f (pr1 is) (pr2 is)).
Definition ismonoidopisof {X Y : setwithbinop} (f : binopiso X Y) (is : ismonoidop (@op X)) :
ismonoidop (@op Y) := make_dirprod (isassocisof f (pr1 is)) (isunitalisof f (pr2 is)).
Definition ismonoidopisob {X Y : setwithbinop} (f : binopiso X Y) (is : ismonoidop (@op Y)) :
ismonoidop (@op X) := make_dirprod (isassocisob f (pr1 is)) (isunitalisob f (pr2 is)).
Lemma isinvisof {X Y : setwithbinop} (f : binopiso X Y) (unx : X) (invx : X -> X)
(is : isinv (@op X) unx invx) :
isinv (@op Y) (pr1 f unx) (funcomp (invmap (pr1 f)) (funcomp invx (pr1 f))).
Show proof.
set (axf := pr2 f). set (axinvf := pr2 (invbinopiso f)).
simpl in axf, axinvf. split.
- intro a. apply (invmaponpathsweq (pr1 (invbinopiso f))).
simpl. rewrite (axinvf ((pr1 f) (invx (invmap (pr1 f) a))) a).
rewrite (homotinvweqweq (pr1 f) unx).
rewrite (homotinvweqweq (pr1 f) (invx (invmap (pr1 f) a))).
apply (pr1 is).
- intro a. apply (invmaponpathsweq (pr1 (invbinopiso f))).
simpl. rewrite (axinvf a ((pr1 f) (invx (invmap (pr1 f) a)))).
rewrite (homotinvweqweq (pr1 f) unx).
rewrite (homotinvweqweq (pr1 f) (invx (invmap (pr1 f) a))).
apply (pr2 is).
Opaque isinvisof.simpl in axf, axinvf. split.
- intro a. apply (invmaponpathsweq (pr1 (invbinopiso f))).
simpl. rewrite (axinvf ((pr1 f) (invx (invmap (pr1 f) a))) a).
rewrite (homotinvweqweq (pr1 f) unx).
rewrite (homotinvweqweq (pr1 f) (invx (invmap (pr1 f) a))).
apply (pr1 is).
- intro a. apply (invmaponpathsweq (pr1 (invbinopiso f))).
simpl. rewrite (axinvf a ((pr1 f) (invx (invmap (pr1 f) a)))).
rewrite (homotinvweqweq (pr1 f) unx).
rewrite (homotinvweqweq (pr1 f) (invx (invmap (pr1 f) a))).
apply (pr2 is).
Definition isgropisof {X Y : setwithbinop} (f : binopiso X Y) (is : isgrop (@op X)) :
isgrop (@op Y) := tpair _ (ismonoidopisof f is)
(tpair _ (funcomp (invmap (pr1 f)) (funcomp (grinv_is is) (pr1 f)))
(isinvisof f (unel_is is) (grinv_is is) (pr2 (pr2 is)))).
Lemma isinvisob {X Y : setwithbinop} (f : binopiso X Y) (uny : Y) (invy : Y -> Y)
(is : isinv (@op Y) uny invy) : isinv (@op X) (invmap (pr1 f) uny)
(funcomp (pr1 f) (funcomp invy (invmap (pr1 f)))).
Show proof.
Opaque isinvisob.
Definition isgropisob {X Y : setwithbinop} (f : binopiso X Y) (is : isgrop (@op Y)) :
isgrop (@op X) := tpair _ (ismonoidopisob f is)
(tpair _ (funcomp (pr1 f) (funcomp (grinv_is is) (invmap (pr1 f))))
(isinvisob f (unel_is is) (grinv_is is) (pr2 (pr2 is)))).
Definition isabmonoidopisof {X Y : setwithbinop} (f : binopiso X Y) (is : isabmonoidop (@op X)) :
isabmonoidop (@op Y) := tpair _ (ismonoidopisof f is) (iscommisof f (commax_is is)).
Definition isabmonoidopisob {X Y : setwithbinop} (f : binopiso X Y) (is : isabmonoidop (@op Y)) :
isabmonoidop (@op X) := tpair _ (ismonoidopisob f is) (iscommisob f (commax_is is)).
Definition isabgropisof {X Y : setwithbinop} (f : binopiso X Y) (is : isabgrop (@op X)) :
isabgrop (@op Y) := tpair _ (isgropisof f is) (iscommisof f (commax_is is)).
Definition isabgropisob {X Y : setwithbinop} (f : binopiso X Y) (is : isabgrop (@op Y)) :
isabgrop (@op X) := tpair _ (isgropisob f is) (iscommisob f (commax_is is)).
Definition issubsetwithbinop {X : hSet} (opp : binop X) (A : hsubtype X) : UU :=
∏ a a' : A, A (opp (pr1 a) (pr1 a')).
Lemma isapropissubsetwithbinop {X : hSet} (opp : binop X) (A : hsubtype X) :
isaprop (issubsetwithbinop opp A).
Show proof.
Definition subsetswithbinop (X : setwithbinop) : UU :=
total2 (λ A : hsubtype X, issubsetwithbinop (@op X) A).
Definition make_subsetswithbinop {X : setwithbinop} :
∏ (t : hsubtype X), (λ A : hsubtype X, issubsetwithbinop op A) t →
∑ A : hsubtype X, issubsetwithbinop op A :=
tpair (λ A : hsubtype X, issubsetwithbinop (@op X) A).
Definition subsetswithbinopconstr {X : setwithbinop} :
∏ (t : hsubtype X), (λ A : hsubtype X, issubsetwithbinop op A) t →
∑ A : hsubtype X, issubsetwithbinop op A := @make_subsetswithbinop X.
Definition pr1subsetswithbinop (X : setwithbinop) : subsetswithbinop X -> hsubtype X :=
@pr1 _ (λ A : hsubtype X, issubsetwithbinop (@op X) A).
Coercion pr1subsetswithbinop : subsetswithbinop >-> hsubtype.
Definition pr2subsetswithbinop {X : setwithbinop} (Y : subsetswithbinop X) :
issubsetwithbinop (@op X) (pr1subsetswithbinop X Y) := pr2 Y.
Definition totalsubsetwithbinop (X : setwithbinop) : subsetswithbinop X.
Show proof.
Definition carrierofasubsetwithbinop {X : setwithbinop} (A : subsetswithbinop X) : setwithbinop.
Show proof.
set (aset := (make_hSet (carrier A) (isasetsubset (pr1carrier A) (setproperty X)
(isinclpr1carrier A))) : hSet).
split with aset.
set (subopp := (λ a a' : A, make_carrier A (op (pr1carrier _ a) (pr1carrier _ a')) (pr2 A a a')) :
(A -> A -> A)).
simpl. unfold binop. apply subopp.
Coercion carrierofasubsetwithbinop : subsetswithbinop >-> setwithbinop.(isinclpr1carrier A))) : hSet).
split with aset.
set (subopp := (λ a a' : A, make_carrier A (op (pr1carrier _ a) (pr1carrier _ a')) (pr2 A a a')) :
(A -> A -> A)).
simpl. unfold binop. apply subopp.
Definition isbinophrel {X : setwithbinop} (R : hrel X) : UU :=
dirprod (∏ a b c : X, R a b -> R (op c a) (op c b)) (∏ a b c : X, R a b -> R (op a c) (op b c)).
Definition make_isbinophrel {X : setwithbinop} {R : hrel X}
(H1 : ∏ a b c : X, R a b -> R (op c a) (op c b))
(H2 : ∏ a b c : X, R a b -> R (op a c) (op b c)) : isbinophrel R :=
tpair _ H1 H2.
Definition isbinophrellogeqf {X : setwithbinop} {L R : hrel X}
(lg : hrellogeq L R) (isl : isbinophrel L) : isbinophrel R.
Show proof.
split.
- intros a b c rab.
apply ((pr1 (lg _ _) ((pr1 isl) _ _ _ (pr2 (lg _ _) rab)))).
- intros a b c rab.
apply ((pr1 (lg _ _) ((pr2 isl) _ _ _ (pr2 (lg _ _) rab)))).
- intros a b c rab.
apply ((pr1 (lg _ _) ((pr1 isl) _ _ _ (pr2 (lg _ _) rab)))).
- intros a b c rab.
apply ((pr1 (lg _ _) ((pr2 isl) _ _ _ (pr2 (lg _ _) rab)))).
Lemma isapropisbinophrel {X : setwithbinop} (R : hrel X) : isaprop (isbinophrel R).
Show proof.
apply isapropdirprod.
- apply impred. intro a.
apply impred. intro b.
apply impred. intro c.
apply impred. intro r.
apply (pr2 (R _ _)).
- apply impred. intro a.
apply impred. intro b.
apply impred. intro c.
apply impred. intro r.
apply (pr2 (R _ _)).
- apply impred. intro a.
apply impred. intro b.
apply impred. intro c.
apply impred. intro r.
apply (pr2 (R _ _)).
- apply impred. intro a.
apply impred. intro b.
apply impred. intro c.
apply impred. intro r.
apply (pr2 (R _ _)).
Lemma isbinophrelif {X : setwithbinop} (R : hrel X) (is : iscomm (@op X))
(isl : ∏ a b c : X, R a b -> R (op c a) (op c b)) : isbinophrel R.
Show proof.
split with isl. intros a b c rab.
destruct (is c a). destruct (is c b). apply (isl _ _ _ rab).
destruct (is c a). destruct (is c b). apply (isl _ _ _ rab).
Lemma iscompbinoptransrel {X : setwithbinop} (R : hrel X) (ist : istrans R) (isb : isbinophrel R) :
iscomprelrelfun2 R R (@op X).
Show proof.
intros a b c d. intros rab rcd.
set (racbc := pr2 isb a b c rab). set (rbcbd := pr1 isb c d b rcd).
apply (ist _ _ _ racbc rbcbd).
set (racbc := pr2 isb a b c rab). set (rbcbd := pr1 isb c d b rcd).
apply (ist _ _ _ racbc rbcbd).
Lemma isbinopreflrel {X : setwithbinop} (R : hrel X) (isr : isrefl R)
(isb : iscomprelrelfun2 R R (@op X)) : isbinophrel R.
Show proof.
split.
- intros a b c rab. apply (isb c c a b (isr c) rab).
- intros a b c rab. apply (isb a b c c rab (isr c)).
- intros a b c rab. apply (isb c c a b (isr c) rab).
- intros a b c rab. apply (isb a b c c rab (isr c)).
Definition binophrel (X : setwithbinop) : UU := total2 (λ R : hrel X, isbinophrel R).
Definition make_binophrel {X : setwithbinop} :
∏ (t : hrel X), (λ R : hrel X, isbinophrel R) t → ∑ R : hrel X, isbinophrel R :=
tpair (λ R : hrel X, isbinophrel R).
Definition pr1binophrel (X : setwithbinop) : binophrel X -> hrel X :=
@pr1 _ (λ R : hrel X, isbinophrel R).
Coercion pr1binophrel : binophrel >-> hrel.
Definition binophrel_resp_left {X : setwithbinop} (R : binophrel X)
{a b : X} (c : X) (r : R a b) : R (op c a) (op c b) :=
pr1 (pr2 R) a b c r.
Definition binophrel_resp_right {X : setwithbinop} (R : binophrel X)
{a b : X} (c : X) (r : R a b) : R (op a c) (op b c) :=
pr2 (pr2 R) a b c r.
Definition binoppo (X : setwithbinop) : UU := total2 (λ R : po X, isbinophrel R).
Definition make_binoppo {X : setwithbinop} :
∏ (t : po X), (λ R : po X, isbinophrel R) t → ∑ R : po X, isbinophrel R :=
tpair (λ R : po X, isbinophrel R).
Definition pr1binoppo (X : setwithbinop) : binoppo X -> po X := @pr1 _ (λ R : po X, isbinophrel R).
Coercion pr1binoppo : binoppo >-> po.
Definition binopeqrel (X : setwithbinop) : UU := total2 (λ R : eqrel X, isbinophrel R).
Definition make_binopeqrel {X : setwithbinop} :
∏ (t : eqrel X), (λ R : eqrel X, isbinophrel R) t → ∑ R : eqrel X, isbinophrel R :=
tpair (λ R : eqrel X, isbinophrel R).
Definition pr1binopeqrel (X : setwithbinop) : binopeqrel X -> eqrel X :=
@pr1 _ (λ R : eqrel X, isbinophrel R).
Coercion pr1binopeqrel : binopeqrel >-> eqrel.
Definition binopeqrel_resp_left {X : setwithbinop} (R : binopeqrel X)
{a b : X} (c : X) (r : R a b) : R (op c a) (op c b) :=
pr1 (pr2 R) a b c r.
Definition binopeqrel_resp_right {X : setwithbinop} (R : binopeqrel X)
{a b : X} (c : X) (r : R a b) : R (op a c) (op b c) :=
pr2 (pr2 R) a b c r.
Definition setwithbinopquot {X : setwithbinop} (R : binopeqrel X) : setwithbinop.
Show proof.
split with (setquotinset R).
set (qt := setquot R). set (qtset := setquotinset R).
assert (iscomp : iscomprelrelfun2 R R op) by apply (iscompbinoptransrel R (eqreltrans R) (pr2 R)).
set (qtmlt := setquotfun2 R R op iscomp).
simpl. unfold binop. apply qtmlt.
set (qt := setquot R). set (qtset := setquotinset R).
assert (iscomp : iscomprelrelfun2 R R op) by apply (iscompbinoptransrel R (eqreltrans R) (pr2 R)).
set (qtmlt := setquotfun2 R R op iscomp).
simpl. unfold binop. apply qtmlt.
Definition ispartbinophrel {X : setwithbinop} (S : hsubtype X) (R : hrel X) : UU :=
dirprod (∏ a b c : X,