# Algebra I. Part C. Groups, abelian groups. Vladimir Voevodsky. Aug. 2011 - .

## Contents

• Groups
• Basic definitions
• Univalence for groups
• Computation lemmas for groups
• Relations on groups
• Subobjects
• Quotient objects
• Cosets
• Direct products
• Abelian groups
• Basic definitions
• Univalence for abelian groups
• Subobjects
• Kernels
• Quotient objects
• Direct products
• Abelian group of fractions of an abelian unitary monoid
• Abelian group of fractions and abelian monoid of fractions
• Canonical homomorphism to the abelian group of fractions
• Abelian group of fractions in the case when all elements are cancelable
• Relations on the abelian group of fractions
• Relations and the canonical homomorphism to abgrdiff

## Groups

### Basic definitions

Definition gr : UU := total2 (λ X : setwithbinop, isgrop (@op X)).

Definition make_gr :
(t : setwithbinop), (λ X : setwithbinop, isgrop op) t X : setwithbinop, isgrop op :=
tpair (λ X : setwithbinop, isgrop (@op X)).

Definition grtomonoid : gr monoid := λ X : _, make_monoid (pr1 X) (pr1 (pr2 X)).
Coercion grtomonoid : gr >-> monoid.

Definition grinv (X : gr) : X X := pr1 (pr2 (pr2 X)).

Definition grlinvax (X : gr) : islinv (@op X) (unel X) (grinv X) := pr1 (pr2 (pr2 (pr2 X))).

Definition grrinvax (X : gr) : isrinv (@op X) (unel X) (grinv X) := pr2 (pr2 (pr2 (pr2 X))).

Definition gr_of_monoid (X : monoid) (H : invstruct (@op X) (pr2 X)) : gr :=
make_gr X (make_isgrop (pr2 X) H).

Lemma monoidfuninvtoinv {X Y : gr} (f : monoidfun X Y) (x : X) :
f (grinv X x) = grinv Y (f x).
Proof.
intros.
apply (invmaponpathsweq (make_weq _ (isweqrmultingr_is (pr2 Y) (f x)))).
simpl.
change (paths (op (pr1 f (grinv X x)) (pr1 f x)) (op (grinv Y (pr1 f x)) (pr1 f x))).
rewrite (grlinvax Y (pr1 f x)).
destruct (pr1 (pr2 f) (grinv X x) x).
rewrite (grlinvax X x).
apply (pr2 (pr2 f)).
Defined.

Lemma grinv_path_from_op_path {X : gr} {x y : X} (p : (x × y)%multmonoid = unel X) :
grinv X x = y.
Proof.
now rewrite <- (lunax X y), <- (grlinvax X x), assocax, p, runax.
Defined.

### Construction of the trivial abmonoid consisting of one element given by unit.

Definition unitgr_isgrop : isgrop (@op unitmonoid).
Proof.
use make_isgrop.
- exact unitmonoid_ismonoid.
- use make_invstruct.
+ intros i. exact i.
+ use make_isinv.
× intros x. use isProofIrrelevantUnit.
× intros x. use isProofIrrelevantUnit.
Qed.

Definition unitgr : gr := make_gr unitmonoid unitgr_isgrop.

Lemma grfuntounit_ismonoidfun (X : gr) : ismonoidfun (λ x : X, (unel unitgr)).
Proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. use isProofIrrelevantUnit.
- use isProofIrrelevantUnit.
Qed.

Definition grfuntounit (X : gr) : monoidfun X unitgr := monoidfunconstr (grfuntounit_ismonoidfun X).

Lemma grfunfromunit_ismonoidfun (X : gr) : ismonoidfun (λ x : unitgr, (unel X)).
Proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. use pathsinv0. use (runax X).
- use idpath.
Qed.

Definition grfunfromunit (X : gr) : monoidfun unitmonoid X :=
monoidfunconstr (monoidfunfromunit_ismonoidfun X).

Lemma unelgrfun_ismonoidfun (X Y : gr) : ismonoidfun (λ x : X, (unel Y)).
Proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. use pathsinv0. use lunax.
- use idpath.
Qed.

Definition unelgrfun (X Y : gr) : monoidfun X Y :=
monoidfunconstr (unelgrfun_ismonoidfun X Y).

### (X = Y) ≃ (monoidiso X Y)

The idea is to use the composition
(X = Y) ≃ (make_gr' X = make_gr' Y) ≃ ((gr'_to_monoid (make_gr' X)) = (gr'_to_monoid (make_gr' Y))) ≃ (monoidiso X Y).
The reason why we use gr' is that then we can use univalence for monoids. See gr_univalence_weq3.

Local Definition gr' : UU :=
g : ( X : setwithbinop, ismonoidop (@op X)), invstruct (@op (pr1 g)) (pr2 g).

Local Definition make_gr' (X : gr) : gr' := tpair _ (tpair _ (pr1 X) (pr1 (pr2 X))) (pr2 (pr2 X)).

Local Definition gr'_to_monoid (X : gr') : monoid := pr1 X.

Definition gr_univalence_weq1 : gr gr' :=
weqtotal2asstol
(λ Z : setwithbinop, ismonoidop (@op Z))
(fun y : ( (x : setwithbinop), ismonoidop (@op x)) ⇒ invstruct (@op (pr1 y)) (pr2 y)).

Definition gr_univalence_weq1' (X Y : gr) : (X = Y) (make_gr' X = make_gr' Y) :=
make_weq _ (@isweqmaponpaths gr gr' gr_univalence_weq1 X Y).

Definition gr_univalence_weq2 (X Y : gr) :
((make_gr' X) = (make_gr' Y)) ((gr'_to_monoid (make_gr' X)) = (gr'_to_monoid (make_gr' Y))).
Proof.
use subtypeInjectivity.
intros w. use isapropinvstruct.
Defined.
Opaque gr_univalence_weq2.

Definition gr_univalence_weq3 (X Y : gr) :
((gr'_to_monoid (make_gr' X)) = (gr'_to_monoid (make_gr' Y))) (monoidiso X Y) :=
monoid_univalence (gr'_to_monoid (make_gr' X)) (gr'_to_monoid (make_gr' Y)).

Definition gr_univalence_map (X Y : gr) : (X = Y) (monoidiso X Y).
Proof.
intro e. induction e. exact (idmonoidiso X).
Defined.

Lemma gr_univalence_isweq (X Y : gr) : isweq (gr_univalence_map X Y).
Proof.
use isweqhomot.
- exact (weqcomp (gr_univalence_weq1' X Y)
(weqcomp (gr_univalence_weq2 X Y) (gr_univalence_weq3 X Y))).
- intros e. induction e.
use (pathscomp0 weqcomp_to_funcomp_app).
use weqcomp_to_funcomp_app.
- use weqproperty.
Defined.
Opaque gr_univalence_isweq.

Definition gr_univalence (X Y : gr) : (X = Y) (monoidiso X Y).
Proof.
use make_weq.
- exact (gr_univalence_map X Y).
- exact (gr_univalence_isweq X Y).
Defined.
Opaque gr_univalence.

### Computation lemmas for groups

Definition weqlmultingr (X : gr) (x0 : X) : pr1 X pr1 X :=
make_weq _ (isweqlmultingr_is (pr2 X) x0).

Definition weqrmultingr (X : gr) (x0 : X) : pr1 X pr1 X :=
make_weq _ (isweqrmultingr_is (pr2 X) x0).

Lemma grlcan (X : gr) {a b : X} (c : X) (e : paths (op c a) (op c b)) : a = b.
Proof. apply (invmaponpathsweq (weqlmultingr X c) _ _ e). Defined.

Lemma grrcan (X : gr) {a b : X} (c : X) (e : paths (op a c) (op b c)) : a = b.
Proof. apply (invmaponpathsweq (weqrmultingr X c) _ _ e). Defined.

Lemma grinvunel (X : gr) : paths (grinv X (unel X)) (unel X).
Proof.
apply (grrcan X (unel X)).
rewrite (grlinvax X). rewrite (runax X).
apply idpath.
Defined.

Lemma grinvinv (X : gr) (a : X) : paths (grinv X (grinv X a)) a.
Proof.
apply (grlcan X (grinv X a)).
rewrite (grlinvax X a). rewrite (grrinvax X _).
apply idpath.
Defined.

Lemma grinvmaponpathsinv (X : gr) {a b : X} (e : paths (grinv X a) (grinv X b)) : a = b.
Proof.
assert (e' := maponpaths (λ x, grinv X x) e).
simpl in e'. rewrite (grinvinv X _) in e'.
rewrite (grinvinv X _) in e'. apply e'.
Defined.

Lemma grinvandmonoidfun (X Y : gr) {f : X Y} (is : ismonoidfun f) (x : X) :
paths (f (grinv X x)) (grinv Y (f x)).
Proof.
apply (grrcan Y (f x)).
rewrite (pathsinv0 (pr1 is _ _)). rewrite (grlinvax X).
rewrite (grlinvax Y).
apply (pr2 is).
Defined.

Lemma grinvop (Y : gr) :
y1 y2 : Y, grinv Y (@op Y y1 y2) = @op Y (grinv Y y2) (grinv Y y1).
Proof.
intros y1 y2.
apply (grrcan Y y1).
rewrite (assocax Y). rewrite (grlinvax Y). rewrite (runax Y).
apply (grrcan Y y2).
rewrite (grlinvax Y). rewrite (assocax Y). rewrite (grlinvax Y).
apply idpath.
Qed.

### Relations on groups

Lemma isinvbinophrelgr (X : gr) {R : hrel X} (is : isbinophrel R) : isinvbinophrel R.
Proof.
set (is1 := pr1 is). set (is2 := pr2 is). split.
- intros a b c r. set (r' := is1 _ _ (grinv X c) r).
clearbody r'. rewrite (pathsinv0 (assocax X _ _ a)) in r'.
rewrite (pathsinv0 (assocax X _ _ b)) in r'.
rewrite (grlinvax X c) in r'.
rewrite (lunax X a) in r'.
rewrite (lunax X b) in r'.
apply r'.
- intros a b c r. set (r' := is2 _ _ (grinv X c) r).
clearbody r'. rewrite ((assocax X a _ _)) in r'.
rewrite ((assocax X b _ _)) in r'.
rewrite (grrinvax X c) in r'.
rewrite (runax X a) in r'.
rewrite (runax X b) in r'.
apply r'.
Defined.
Opaque isinvbinophrelgr.

Lemma isbinophrelgr (X : gr) {R : hrel X} (is : isinvbinophrel R) : isbinophrel R.
Proof.
set (is1 := pr1 is). set (is2 := pr2 is). split.
- intros a b c r. rewrite (pathsinv0 (lunax X a)) in r.
rewrite (pathsinv0 (lunax X b)) in r.
rewrite (pathsinv0 (grlinvax X c)) in r.
rewrite (assocax X _ _ a) in r.
rewrite (assocax X _ _ b) in r.
apply (is1 _ _ (grinv X c) r).
- intros a b c r. rewrite (pathsinv0 (runax X a)) in r.
rewrite (pathsinv0 (runax X b)) in r.
rewrite (pathsinv0 (grrinvax X c)) in r.
rewrite (pathsinv0 (assocax X a _ _)) in r.
rewrite (pathsinv0 (assocax X b _ _)) in r.
apply (is2 _ _ (grinv X c) r).
Defined.
Opaque isbinophrelgr.

Lemma grfromgtunel (X : gr) {R : hrel X} (is : isbinophrel R) {x : X} (isg : R x (unel X)) :
R (unel X) (grinv X x).
Proof.
intros.
set (r := (pr2 is) _ _ (grinv X x) isg).
rewrite (grrinvax X x) in r.
rewrite (lunax X _) in r.
apply r.
Defined.

Lemma grtogtunel (X : gr) {R : hrel X} (is : isbinophrel R) {x : X} (isg : R (unel X) (grinv X x)) :
R x (unel X).
Proof.
assert (r := (pr2 is) _ _ x isg).
rewrite (grlinvax X x) in r.
rewrite (lunax X _) in r.
apply r.
Defined.

Lemma grfromltunel (X : gr) {R : hrel X} (is : isbinophrel R) {x : X} (isg : R (unel X) x) :
R (grinv X x) (unel X).
Proof.
assert (r := (pr1 is) _ _ (grinv X x) isg).
rewrite (grlinvax X x) in r.
rewrite (runax X _) in r.
apply r.
Defined.

Lemma grtoltunel (X : gr) {R : hrel X} (is : isbinophrel R) {x : X} (isg : R (grinv X x) (unel X)) :
R (unel X) x.
Proof.
assert (r := (pr1 is) _ _ x isg).
rewrite (grrinvax X x) in r. rewrite (runax X _) in r.
apply r.
Defined.

### Subobjects

Definition issubgr {X : gr} (A : hsubtype X) : UU :=
dirprod (issubmonoid A) ( x : X, A x A (grinv X x)).

Definition make_issubgr {X : gr} {A : hsubtype X} (H1 : issubmonoid A)
(H2 : x : X, A x A (grinv X x)) : issubgr A := make_dirprod H1 H2.

Lemma isapropissubgr {X : gr} (A : hsubtype X) : isaprop (issubgr A).
Proof.
apply (isofhleveldirprod 1).
- apply isapropissubmonoid.
- apply impred. intro x.
apply impred. intro a.
apply (pr2 (A (grinv X x))).
Defined.

Definition subgr (X : gr) : UU := total2 (λ A : hsubtype X, issubgr A).

Definition make_subgr {X : gr} :
(t : hsubtype X), (λ A : hsubtype X, issubgr A) t A : hsubtype X, issubgr A :=
tpair (λ A : hsubtype X, issubgr A).

Definition subgrconstr {X : gr} :
(t : hsubtype X), (λ A : hsubtype X, issubgr A) t A : hsubtype X, issubgr A :=
@make_subgr X.

Definition subgrtosubmonoid (X : gr) : subgr X submonoid X :=
λ A : _, make_submonoid (pr1 A) (pr1 (pr2 A)).
Coercion subgrtosubmonoid : subgr >-> submonoid.

Definition totalsubgr (X : gr) : subgr X.
Proof.
split with (@totalsubtype X).
split.
- exact (pr2 (totalsubmonoid X)).
- exact (fun _ _tt).
Defined.

Definition trivialsubgr (X : gr) : subgr X.
Proof.
(λ x, x = @unel X)%set.
split.
- exact (pr2 (@trivialsubmonoid X)).
- intro.
intro eq_1.
induction (!eq_1).
apply grinvunel.
Defined.

Lemma isinvoncarrier {X : gr} (A : subgr X) :
isinv (@op A) (unel A) (λ a : A, make_carrier _ (grinv X (pr1 a)) (pr2 (pr2 A) (pr1 a) (pr2 a))).
Proof.
split.
- intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)).
simpl. apply (grlinvax X (pr1 a)).
- intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)).
simpl. apply (grrinvax X (pr1 a)).
Defined.

Definition isgrcarrier {X : gr} (A : subgr X) : isgrop (@op A) :=
tpair _ (ismonoidcarrier A)
(tpair _ (λ a : A, make_carrier _ (grinv X (pr1 a)) (pr2 (pr2 A) (pr1 a) (pr2 a)))
(isinvoncarrier A)).

Definition carrierofasubgr {X : gr} (A : subgr X) : gr.
Proof. split with A. apply (isgrcarrier A). Defined.
Coercion carrierofasubgr : subgr >-> gr.

Lemma intersection_subgr : {X : gr} {I : UU} (S : I hsubtype X)
(each_is_subgr : i : I, issubgr (S i)),
issubgr (subtype_intersection S).
Proof.
intros.
use make_issubgr.
- exact (intersection_submonoid S (λ i, (pr1 (each_is_subgr i)))).
- exact (λ x x_in_S i, pr2 (each_is_subgr i) x (x_in_S i)).
Qed.

Definition subgr_incl {X : gr} (A : subgr X) : monoidfun A X :=
submonoid_incl A.

### Quotient objects

Lemma grquotinvcomp {X : gr} (R : binopeqrel X) : iscomprelrelfun R R (grinv X).
Proof.
destruct R as [ R isb ].
set (isc := iscompbinoptransrel _ (eqreltrans _) isb).
unfold iscomprelrelfun. intros x x' r.
destruct R as [ R iseq ]. destruct iseq as [ ispo0 symm0 ].
destruct ispo0 as [ trans0 refl0 ]. unfold isbinophrel in isb.
set (r0 := isc _ _ _ _ (isc _ _ _ _ (refl0 (grinv X x')) r) (refl0 (grinv X x))).
rewrite (grlinvax X x') in r0.
rewrite (assocax X (grinv X x') x (grinv X x)) in r0.
rewrite (grrinvax X x) in r0. rewrite (lunax X _) in r0.
rewrite (runax X _) in r0.
apply (symm0 _ _ r0).
Defined.
Opaque grquotinvcomp.

Definition invongrquot {X : gr} (R : binopeqrel X) : setquot R setquot R :=
setquotfun R R (grinv X) (grquotinvcomp R).

Lemma isinvongrquot {X : gr} (R : binopeqrel X) :
isinv (@op (setwithbinopquot R)) (setquotpr R (unel X)) (invongrquot R).
Proof.
split.
- unfold islinv.
apply (setquotunivprop
R (λ x : setwithbinopquot R, eqset
(@op (setwithbinopquot R) (invongrquot R x) x)
(setquotpr R (unel X)))).
intro x.
apply (@maponpaths _ _ (setquotpr R) (@op X (grinv X x) x) (unel X)).
apply (grlinvax X).
- unfold isrinv.
apply (setquotunivprop
R (λ x : setwithbinopquot R, eqset
(@op (setwithbinopquot R) x (invongrquot R x))
(setquotpr R (unel X)))).
intro x.
apply (@maponpaths _ _ (setquotpr R) (@op X x (grinv X x)) (unel X)).
apply (grrinvax X).
Defined.
Opaque isinvongrquot.

Definition isgrquot {X : gr} (R : binopeqrel X) : isgrop (@op (setwithbinopquot R)) :=
tpair _ (ismonoidquot R) (tpair _ (invongrquot R) (isinvongrquot R)).

Definition grquot {X : gr} (R : binopeqrel X) : gr.
Proof. split with (setwithbinopquot R). apply isgrquot. Defined.

### Cosets

Section GrCosets.
Context {X : gr}.

Local Open Scope multmonoid.

Local Lemma isaprop_mult_eq_r (x y : X) : isaprop ( z : X, x × z = y).
Proof.
apply invproofirrelevance; intros z1 z2.
apply subtypePath.
{ intros x'. apply setproperty. }
refine (!lunax _ _ @ _ @ lunax _ _).
refine (maponpaths (λ z, z × _) (!grlinvax X x) @ _ @
maponpaths (λ z, z × _) (grlinvax X x)).
refine (assocax _ _ _ _ @ _ @ !assocax _ _ _ _).
refine (maponpaths _ (pr2 z1) @ _ @ !maponpaths _ (pr2 z2)).
reflexivity.
Defined.

Local Lemma isaprop_mult_eq_l (x y : X) : isaprop ( z : X, z × x = y).
Proof.
apply invproofirrelevance; intros z1 z2.
apply subtypePath.
{ intros x'. apply setproperty. }
refine (!runax _ _ @ _ @ runax _ _).
refine (maponpaths (λ z, _ × z) (!grrinvax X x) @ _ @
maponpaths (λ z, _ × z) (grrinvax X x)).
refine (!assocax _ _ _ _ @ _ @ assocax _ _ _ _).
refine (maponpaths (λ z, z × _) (pr2 z1) @ _ @ !maponpaths (λ z, z × _) (pr2 z2)).
reflexivity.
Defined.

Context (Y : subgr X).

Lemma isaprop_in_same_left_coset (x1 x2 : X) :
isaprop (in_same_left_coset Y x1 x2).
Proof.
unfold in_same_left_coset.
apply invproofirrelevance; intros p q.
apply subtypePath.
{ intros x'. apply setproperty. }
apply subtypePath.
{ intros x'. apply propproperty. }
pose (p' := (pr11 p,, pr2 p) : y : X, x1 × y = x2).
pose (q' := (pr11 q,, pr2 q) : y : X, x1 × y = x2).
apply (maponpaths pr1 (iscontrpr1 (isaprop_mult_eq_r _ _ p' q'))).
Defined.

Lemma isaprop_in_same_right_coset (x1 x2 : X) :
isaprop (in_same_right_coset Y x1 x2).
Proof.
apply invproofirrelevance.
intros p q.
apply subtypePath; [intros x; apply setproperty|].
apply subtypePath; [intros x; apply propproperty|].
pose (p' := (pr11 p,, pr2 p) : y : X, y × x1 = x2).
pose (q' := (pr11 q,, pr2 q) : y : X, y × x1 = x2).
apply (maponpaths pr1 (iscontrpr1 (isaprop_mult_eq_l _ _ p' q'))).
Defined.

The property of being in the same coset defines an equivalence relation.

Definition in_same_left_coset_eqrel : eqrel X.
use make_eqrel.
- intros x1 x2.
use make_hProp.
+ exact (in_same_left_coset Y x1 x2).
+ apply isaprop_in_same_left_coset.
- use iseqrelconstr.
+
Transitivity
intros ? ? ?; cbn; intros inxy inyz.
unfold in_same_left_coset in ×.
use tpair.
× (pr11 inxy × pr11 inyz).
apply (pr2 Y).
× cbn.
refine (_ @ pr2 inyz).
refine (_ @ maponpaths (λ z, z × _) (pr2 inxy)).
apply pathsinv0, assocax.
+
Reflexivity
intro; cbn.
use tpair.
× 1; apply (pr2 Y).
× apply runax.
+
Symmetry
intros x y inxy.
use tpair.
× (grinv X (pr1 (pr1 inxy))).
apply (pr2 Y).
exact (pr2 (pr1 inxy)).
× cbn in ×.
refine (!maponpaths (λ z, z × _) (pr2 inxy) @ _).
refine (assocax _ _ _ _ @ _).
refine (maponpaths _ (grrinvax _ _) @ _).
apply runax.
Defined.

x₁ and x₂ are in the same Y-coset if and only if x₁⁻¹ * x₂ is in Y. (Proposition 4 in Dummit and Foote)

Definition in_same_coset_test (x1 x2 : X) :
(Y ((grinv _ x1) × x2)) in_same_left_coset Y x1 x2.
Proof.
apply weqimplimpl; unfold in_same_left_coset in ×.
- intros yx1x2.
((grinv _ x1) × x2,, yx1x2); cbn.
refine (!assocax X _ _ _ @ _).
refine (maponpaths (λ z, z × _) (grrinvax X _) @ _).
apply lunax.
- intros y.
use (transportf (pr1 Y)).
+ exact (pr11 y).
+ refine (_ @ maponpaths _ (pr2 y)).
refine (_ @ assocax _ _ _ _).
refine (_ @ !maponpaths (λ z, z × _) (grlinvax X _)).
apply pathsinv0, lunax.
+ exact (pr2 (pr1 y)).
- apply propproperty.
- apply isaprop_in_same_left_coset.
Defined.
End GrCosets.

### Direct products

Lemma isgrdirprod (X Y : gr) : isgrop (@op (setwithbinopdirprod X Y)).
Proof.
split with (ismonoiddirprod X Y).
split with (λ xy : _, make_dirprod (grinv X (pr1 xy)) (grinv Y (pr2 xy))).
split.
- intro xy. destruct xy as [ x y ].
unfold unel_is. simpl. apply pathsdirprod.
apply (grlinvax X x). apply (grlinvax Y y).
- intro xy. destruct xy as [ x y ].
unfold unel_is. simpl. apply pathsdirprod.
apply (grrinvax X x). apply (grrinvax Y y).
Defined.

Definition grdirprod (X Y : gr) : gr.
Proof. split with (setwithbinopdirprod X Y). apply isgrdirprod. Defined.

## Abelian groups

### Basic definitions

Definition abgr : UU := total2 (λ X : setwithbinop, isabgrop (@op X)).

Definition make_abgr (X : setwithbinop) (is : isabgrop (@op X)) : abgr :=
tpair (λ X : setwithbinop, isabgrop (@op X)) X is.

Definition abgrconstr (X : abmonoid) (inv0 : X X) (is : isinv (@op X) (unel X) inv0) : abgr :=
make_abgr X (make_dirprod (make_isgrop (pr2 X) (tpair _ inv0 is)) (commax X)).

Definition abgrtogr : abgr gr := λ X : _, make_gr (pr1 X) (pr1 (pr2 X)).
Coercion abgrtogr : abgr >-> gr.

Definition abgrtoabmonoid : abgr abmonoid :=
λ X : _, make_abmonoid (pr1 X) (make_dirprod (pr1 (pr1 (pr2 X))) (pr2 (pr2 X))).
Coercion abgrtoabmonoid : abgr >-> abmonoid.

Definition abgr_of_gr (X : gr) (H : iscomm (@op X)) : abgr :=
make_abgr X (make_isabgrop (pr2 X) H).

Declare Scope abgr.
Delimit Scope abgr with abgr.
Notation "x - y" := (op x (grinv _ y)) : abgr.
Notation "- y" := (grinv _ y) : abgr.

### Construction of the trivial abgr consisting of one element given by unit.

Definition unitabgr_isabgrop : isabgrop (@op unitabmonoid).
Proof.
use make_isabgrop.
- exact unitgr_isgrop.
- exact (commax unitabmonoid).
Qed.

Definition unitabgr : abgr := make_abgr unitabmonoid unitabgr_isabgrop.

Lemma abgrfuntounit_ismonoidfun (X : abgr) : ismonoidfun (λ x : X, (unel unitabgr)).
Proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. use isProofIrrelevantUnit.
- use isProofIrrelevantUnit.
Qed.

Definition abgrfuntounit (X : abgr) : monoidfun X unitabgr :=
monoidfunconstr (abgrfuntounit_ismonoidfun X).

Lemma abgrfunfromunit_ismonoidfun (X : abgr) : ismonoidfun (λ x : unitabgr, (unel X)).
Proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. use pathsinv0. use (runax X).
- use idpath.
Qed.

Definition abgrfunfromunit (X : abgr) : monoidfun unitabgr X :=
monoidfunconstr (abgrfunfromunit_ismonoidfun X).

Lemma unelabgrfun_ismonoidfun (X Y : abgr) : ismonoidfun (λ x : X, (unel Y)).
Proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. use pathsinv0. use lunax.
- use idpath.
Qed.

Definition unelabgrfun (X Y : abgr) : monoidfun X Y :=
monoidfunconstr (unelgrfun_ismonoidfun X Y).

### Abelian group structure on morphism between abelian groups

Definition abgrshombinop_inv_ismonoidfun {X Y : abgr} (f : monoidfun X Y) :
ismonoidfun (λ x : X, grinv Y (pr1 f x)).
Proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. cbn.
rewrite (pr1 (pr2 f)). rewrite (pr2 (pr2 Y)). use (grinvop Y).
- use (pathscomp0 (maponpaths (λ y : Y, grinv Y y) (monoidfununel f))).
use grinvunel.
Qed.

Definition abgrshombinop_inv {X Y : abgr} (f : monoidfun X Y) : monoidfun X Y :=
monoidfunconstr (abgrshombinop_inv_ismonoidfun f).

Definition abgrshombinop_linvax {X Y : abgr} (f : monoidfun X Y) :
@abmonoidshombinop X Y (abgrshombinop_inv f) f = unelmonoidfun X Y.
Proof.
use monoidfun_paths. use funextfun. intros x. use (@grlinvax Y).
Qed.

Definition abgrshombinop_rinvax {X Y : abgr} (f : monoidfun X Y) :
@abmonoidshombinop X Y f (abgrshombinop_inv f) = unelmonoidfun X Y.
Proof.
use monoidfun_paths. use funextfun. intros x. use (grrinvax Y).
Qed.

Lemma abgrshomabgr_isabgrop (X Y : abgr) :
@isabgrop (abmonoidshomabmonoid X Y) (λ f g : monoidfun X Y, @abmonoidshombinop X Y f g).
Proof.
use make_isabgrop.
- use make_isgrop.
+ exact (abmonoidshomabmonoid_ismonoidop X Y).
+ use make_invstruct.
× intros f. exact (abgrshombinop_inv f).
× use make_isinv.
intros f. exact (abgrshombinop_linvax f).
intros f. exact (abgrshombinop_rinvax f).
- intros f g. exact (abmonoidshombinop_comm f g).
Defined.

Definition abgrshomabgr (X Y : abgr) : abgr.
Proof.
use make_abgr.
- exact (abmonoidshomabmonoid X Y).
- exact (abgrshomabgr_isabgrop X Y).
Defined.

### (X = Y) ≃ (monoidiso X Y)

The idea is to use the following composition
(X = Y) ≃ (make_abgr' X = make_abgr' Y) ≃ (pr1 (make_abgr' X) = pr1 (make_abgr' Y)) ≃ (monoidiso X Y)
We use abgr' so that we can use univalence for groups, gr_univalence. See abgr_univalence_weq3.

Local Definition abgr' : UU :=
g : ( X : setwithbinop, isgrop (@op X)), iscomm (pr2 (pr1 g)).

Local Definition make_abgr' (X : abgr) : abgr' :=
tpair _ (tpair _ (pr1 X) (dirprod_pr1 (pr2 X))) (dirprod_pr2 (pr2 X)).

Local Definition abgr_univalence_weq1 : abgr abgr' :=
weqtotal2asstol (λ Z : setwithbinop, isgrop (@op Z))
(fun y : ( x : setwithbinop, isgrop (@op x)) ⇒ iscomm (@op (pr1 y))).

Definition abgr_univalence_weq1' (X Y : abgr) : (X = Y) (make_abgr' X = make_abgr' Y) :=
make_weq _ (@isweqmaponpaths abgr abgr' abgr_univalence_weq1 X Y).

Definition abgr_univalence_weq2 (X Y : abgr) :
(make_abgr' X = make_abgr' Y) (pr1 (make_abgr' X) = pr1 (make_abgr' Y)).
Proof.
use subtypeInjectivity.
intros w. use isapropiscomm.
Defined.
Opaque abgr_univalence_weq2.

Definition abgr_univalence_weq3 (X Y : abgr) :
(pr1 (make_abgr' X) = pr1 (make_abgr' Y)) (monoidiso X Y) :=
gr_univalence (pr1 (make_abgr' X)) (pr1 (make_abgr' Y)).

Definition abgr_univalence_map (X Y : abgr) : (X = Y) (monoidiso X Y).
Proof.
intro e. induction e. exact (idmonoidiso X).
Defined.

Lemma abgr_univalence_isweq (X Y : abgr) : isweq (abgr_univalence_map X Y).
Proof.
use isweqhomot.
- exact (weqcomp (abgr_univalence_weq1' X Y)
(weqcomp (abgr_univalence_weq2 X Y) (abgr_univalence_weq3 X Y))).
- intros e. induction e.
use (pathscomp0 weqcomp_to_funcomp_app).
use weqcomp_to_funcomp_app.
- use weqproperty.
Defined.
Opaque abgr_univalence_isweq.

Definition abgr_univalence (X Y : abgr) : (X = Y) (monoidiso X Y).
Proof.
use make_weq.
- exact (abgr_univalence_map X Y).
- exact (abgr_univalence_isweq X Y).
Defined.
Opaque abgr_univalence.

### Subobjects

Definition subabgr (X : abgr) := subgr X.
Identity Coercion id_subabgr : subabgr >-> subgr.

Lemma isabgrcarrier {X : abgr} (A : subgr X) : isabgrop (@op A).
Proof.
split with (isgrcarrier A).
apply (pr2 (@isabmonoidcarrier X A)).
Defined.

Definition carrierofasubabgr {X : abgr} (A : subabgr X) : abgr.
Proof. split with A. apply isabgrcarrier. Defined.
Coercion carrierofasubabgr : subabgr >-> abgr.

Definition subabgr_incl {X : abgr} (A : subabgr X) : monoidfun A X :=
submonoid_incl A.

Definition abgr_kernel_hsubtype {A B : abgr} (f : monoidfun A B) : hsubtype A :=
monoid_kernel_hsubtype f.

Definition abgr_image_hsubtype {A B : abgr} (f : monoidfun A B) : hsubtype B :=
(λ y : B, x : A, (f x) = y).

# Kernels

Let f : X -> Y be a morphism of abelian groups. A kernel of f is given by the subgroup of X consisting of elements x such that f x = unel Y.

## Kernel as abelian group

Definition abgr_Kernel_subabgr_issubgr {A B : abgr} (f : monoidfun A B) :
issubgr (abgr_kernel_hsubtype f).
Proof.
use make_issubgr.
- apply kernel_issubmonoid.
- intros x a.
apply (grrcan B (f x)).
apply (pathscomp0 (! (binopfunisbinopfun f (grinv A x) x))).
apply (pathscomp0 (maponpaths (λ a : A, f a) (grlinvax A x))).
apply (pathscomp0 (monoidfununel f)).
apply pathsinv0.
apply (pathscomp0 (lunax B (f x))).
exact a.
Defined.

Definition abgr_Kernel_subabgr {A B : abgr} (f : monoidfun A B) : @subabgr A :=
subgrconstr (@abgr_kernel_hsubtype A B f) (abgr_Kernel_subabgr_issubgr f).

## The inclusion Kernel f --> X is a morphism of abelian groups

Definition abgr_Kernel_monoidfun_ismonoidfun {A B : abgr} (f : monoidfun A B) :
@ismonoidfun (abgr_Kernel_subabgr f) A
(make_incl (pr1carrier (abgr_kernel_hsubtype f))
(isinclpr1carrier (abgr_kernel_hsubtype f))).
Proof.
use make_ismonoidfun.
- use make_isbinopfun. intros x x'. use idpath.
- use idpath.
Qed.

## Image of f is a subgroup

Definition abgr_image_issubgr {A B : abgr} (f : monoidfun A B) : issubgr (abgr_image_hsubtype f).
Proof.
use make_issubgr.
- use make_issubmonoid.
+ intros a a'.
use (hinhuniv _ (pr2 a)). intros ae.
use (hinhuniv _ (pr2 a')). intros a'e.
use hinhpr.
use tpair.
× exact (@op A (pr1 ae) (pr1 a'e)).
× use (pathscomp0 (binopfunisbinopfun f (pr1 ae) (pr1 a'e))).
use two_arg_paths.
exact (pr2 ae).
exact (pr2 a'e).
+ use hinhpr. use tpair.
× exact (unel A).
× exact (monoidfununel f).
- intros b b'.
use (hinhuniv _ b'). intros eb.
use hinhpr.
use tpair.
+ exact (grinv A (pr1 eb)).
+ use (pathscomp0 _ (maponpaths (λ bb : B, (grinv B bb)) (pr2 eb))).
use monoidfuninvtoinv.
Qed.

Definition abgr_image {A B : abgr} (f : monoidfun A B) : @subabgr B :=
@subgrconstr B (@abgr_image_hsubtype A B f) (abgr_image_issubgr f).

### Quotient objects

Lemma isabgrquot {X : abgr} (R : binopeqrel X) : isabgrop (@op (setwithbinopquot R)).
Proof.
split with (isgrquot R).
apply (pr2 (@isabmonoidquot X R)).
Defined.

Definition abgrquot {X : abgr} (R : binopeqrel X) : abgr.
Proof. split with (setwithbinopquot R). apply isabgrquot. Defined.

### Direct products

Lemma isabgrdirprod (X Y : abgr) : isabgrop (@op (setwithbinopdirprod X Y)).
Proof.
split with (isgrdirprod X Y).
apply (pr2 (isabmonoiddirprod X Y)).
Defined.

Definition abgrdirprod (X Y : abgr) : abgr.
Proof.
split with (setwithbinopdirprod X Y).
apply isabgrdirprod.
Defined.

### Abelian group of fractions of an abelian unitary monoid

Section Fractions.

Definition hrelabgrdiff (X : abmonoid) : hrel (X × X) :=
λ xa1 xa2,
hexists (λ x0 : X, paths (((pr1 xa1) + (pr2 xa2)) + x0) (((pr1 xa2) + (pr2 xa1)) + x0)).

Definition abgrdiffphi (X : abmonoid) (xa : dirprod X X) :
dirprod X (totalsubtype X) := make_dirprod (pr1 xa) (make_carrier (λ x : X, htrue) (pr2 xa) tt).

Definition hrelabgrdiff' (X : abmonoid) : hrel (X × X) :=
λ xa1 xa2, eqrelabmonoidfrac X (totalsubmonoid X) (abgrdiffphi X xa1) (abgrdiffphi X xa2).

Lemma logeqhrelsabgrdiff (X : abmonoid) : hrellogeq (hrelabgrdiff' X) (hrelabgrdiff X).
Proof.
split. simpl. apply hinhfun. intro t2.
set (a0 := pr1 (pr1 t2)). split with a0. apply (pr2 t2). simpl.
apply hinhfun. intro t2. set (x0 := pr1 t2). split with (tpair _ x0 tt).
apply (pr2 t2).
Defined.

Lemma iseqrelabgrdiff (X : abmonoid) : iseqrel (hrelabgrdiff X).
Proof.
apply (iseqrellogeqf (logeqhrelsabgrdiff X)).
apply (iseqrelconstr).
intros xx' xx'' xx'''.
intros r1 r2.
apply (eqreltrans (eqrelabmonoidfrac X (totalsubmonoid X)) _ _ _ r1 r2).
intro xx. apply (eqrelrefl (eqrelabmonoidfrac X (totalsubmonoid X)) _).
intros xx xx'. intro r.
apply (eqrelsymm (eqrelabmonoidfrac X (totalsubmonoid X)) _ _ r).
Defined.
Opaque iseqrelabgrdiff.

Definition eqrelabgrdiff (X : abmonoid) : @eqrel (abmonoiddirprod X X) :=
make_eqrel _ (iseqrelabgrdiff X).

Lemma isbinophrelabgrdiff (X : abmonoid) : @isbinophrel (abmonoiddirprod X X) (hrelabgrdiff X).
Proof.
apply (@isbinophrellogeqf (abmonoiddirprod X X) _ _ (logeqhrelsabgrdiff X)).
split. intros a b c r.
apply (pr1 (isbinophrelabmonoidfrac X (totalsubmonoid X)) _ _
(make_dirprod (pr1 c) (make_carrier (λ x : X, htrue) (pr2 c) tt))
r).
intros a b c r.
apply (pr2 (isbinophrelabmonoidfrac X (totalsubmonoid X)) _ _
(make_dirprod (pr1 c) (make_carrier (λ x : X, htrue) (pr2 c) tt))
r).
Defined.
Opaque isbinophrelabgrdiff.

Definition binopeqrelabgrdiff (X : abmonoid) : binopeqrel (abmonoiddirprod X X) :=
make_binopeqrel (eqrelabgrdiff X) (isbinophrelabgrdiff X).

Definition abgrdiffcarrier (X : abmonoid) : abmonoid := @abmonoidquot (abmonoiddirprod X X)
(binopeqrelabgrdiff X).

Definition abgrdiffinvint (X : abmonoid) : dirprod X X dirprod X X :=
λ xs : _, make_dirprod (pr2 xs) (pr1 xs).

Lemma abgrdiffinvcomp (X : abmonoid) :
iscomprelrelfun (hrelabgrdiff X) (eqrelabgrdiff X) (abgrdiffinvint X).
Proof.
unfold iscomprelrelfun. unfold eqrelabgrdiff. unfold hrelabgrdiff.
unfold eqrelabmonoidfrac. unfold hrelabmonoidfrac. simpl. intros xs xs'.
apply (hinhfun). intro tt0.
set (x := pr1 xs). set (s := pr2 xs).
set (x' := pr1 xs'). set (s' := pr2 xs').
split with (pr1 tt0).
destruct tt0 as [ a eq ]. change (paths (s + x' + a) (s' + x + a)).
apply pathsinv0. simpl.
set(e := commax X s' x). simpl in e. rewrite e. clear e.
set (e := commax X s x'). simpl in e. rewrite e. clear e.
apply eq.
Defined.
Opaque abgrdiffinvcomp.

Definition abgrdiffinv (X : abmonoid) : abgrdiffcarrier X abgrdiffcarrier X :=
setquotfun (hrelabgrdiff X) (eqrelabgrdiff X) (abgrdiffinvint X) (abgrdiffinvcomp X).

Lemma abgrdiffisinv (X : abmonoid) :
isinv (@op (abgrdiffcarrier X)) (unel (abgrdiffcarrier X)) (abgrdiffinv X).
Proof.
set (R := eqrelabgrdiff X).
assert (isl : islinv (@op (abgrdiffcarrier X)) (unel (abgrdiffcarrier X)) (abgrdiffinv X)).
{
unfold islinv.
apply (setquotunivprop
R (λ x : abgrdiffcarrier X, eqset (abgrdiffinv X x + x) (unel (abgrdiffcarrier X)))).
intro xs.
set (x := pr1 xs). set (s := pr2 xs).
apply (iscompsetquotpr R (@op (abmonoiddirprod X X) (abgrdiffinvint X xs) xs) (unel _)).
simpl. apply hinhpr. split with (unel X).
change (paths (s + x + (unel X) + (unel X)) ((unel X) + (x + s) + (unel X))).
destruct (commax X x s). destruct (commax X (unel X) (x + s)).
apply idpath.
}
apply (make_dirprod isl (weqlinvrinv (@op (abgrdiffcarrier X)) (commax (abgrdiffcarrier X))
(unel (abgrdiffcarrier X)) (abgrdiffinv X) isl)).
Defined.
Opaque abgrdiffisinv.

Definition abgrdiff (X : abmonoid) : abgr := abgrconstr (abgrdiffcarrier X) (abgrdiffinv X)
(abgrdiffisinv X).

Definition prabgrdiff (X : abmonoid) : X X abgrdiff X :=
λ x x' : X, setquotpr (eqrelabgrdiff X) (make_dirprod x x').

### Abelian group of fractions and abelian monoid of fractions

Definition weqabgrdiffint (X : abmonoid) : weq (X × X) (dirprod X (totalsubtype X)) :=
weqdirprodf (idweq X) (invweq (weqtotalsubtype X)).

Definition weqabgrdiff (X : abmonoid) : weq (abgrdiff X) (abmonoidfrac X (totalsubmonoid X)).
Proof.
intros.
apply (weqsetquotweq (eqrelabgrdiff X)
(eqrelabmonoidfrac X (totalsubmonoid X)) (weqabgrdiffint X)).
- simpl. intros x x'. destruct x as [ x1 x2 ]. destruct x' as [ x1' x2' ].
simpl in ×. apply hinhfun. intro tt0. destruct tt0 as [ xx0 is0 ].
split with (make_carrier (λ x : X, htrue) xx0 tt). apply is0.
- simpl. intros x x'. destruct x as [ x1 x2 ]. destruct x' as [ x1' x2' ].
simpl in ×. apply hinhfun. intro tt0. destruct tt0 as [ xx0 is0 ].
split with (pr1 xx0). apply is0.
Defined.

### Canonical homomorphism to the abelian group of fractions

Definition toabgrdiff (X : abmonoid) (x : X) : abgrdiff X := setquotpr _ (make_dirprod x (unel X)).

Lemma isbinopfuntoabgrdiff (X : abmonoid) : isbinopfun (toabgrdiff X).
Proof.
unfold isbinopfun. intros x1 x2.
change (paths (setquotpr _ (make_dirprod (x1 + x2) (unel X)))
(setquotpr (eqrelabgrdiff X) (make_dirprod (x1 + x2) ((unel X) + (unel X))))).
apply (maponpaths (setquotpr _)).
apply (@pathsdirprod X X).
apply idpath.
apply (pathsinv0 (lunax X 0)).
Defined.

Lemma isunitalfuntoabgrdiff (X : abmonoid) : paths (toabgrdiff X (unel X)) (unel (abgrdiff X)).
Proof. apply idpath. Defined.

Definition ismonoidfuntoabgrdiff (X : abmonoid) : ismonoidfun (toabgrdiff X) :=
make_dirprod (isbinopfuntoabgrdiff X) (isunitalfuntoabgrdiff X).

### Abelian group of fractions in the case when all elements are cancelable

Lemma isinclprabgrdiff (X : abmonoid) (iscanc : x : X, isrcancelable (@op X) x) :
x' : X, isincl (λ x, prabgrdiff X x x').
Proof.
intros.
set (int := isinclprabmonoidfrac X (totalsubmonoid X) (λ a : totalsubmonoid X, iscanc (pr1 a))
(make_carrier (λ x : X, htrue) x' tt)).
set (int1 := isinclcomp (make_incl _ int) (weqtoincl (invweq (weqabgrdiff X)))).
apply int1.
Defined.

Definition isincltoabgrdiff (X : abmonoid) (iscanc : x : X, isrcancelable (@op X) x) :
isincl (toabgrdiff X) := isinclprabgrdiff X iscanc (unel X).

Lemma isdeceqabgrdiff (X : abmonoid) (iscanc : x : X, isrcancelable (@op X) x) (is : isdeceq X) :
isdeceq (abgrdiff X).
Proof.
intros.
apply (isdeceqweqf (invweq (weqabgrdiff X))).
apply (isdeceqabmonoidfrac X (totalsubmonoid X) (λ a : totalsubmonoid X, iscanc (pr1 a)) is).
Defined.

### Relations on the abelian group of fractions

Definition abgrdiffrelint (X : abmonoid) (L : hrel X) : hrel (setwithbinopdirprod X X) :=
λ xa yb, hexists (λ c0 : X, L (((pr1 xa) + (pr2 yb)) + c0) (((pr1 yb) + (pr2 xa)) + c0)).

Definition abgrdiffrelint' (X : abmonoid) (L : hrel X) : hrel (setwithbinopdirprod X X) :=
λ xa1 xa2, abmonoidfracrelint _ (totalsubmonoid X) L (abgrdiffphi X xa1) (abgrdiffphi X xa2).

Lemma logeqabgrdiffrelints (X : abmonoid) (L : hrel X) :
hrellogeq (abgrdiffrelint' X L) (abgrdiffrelint X L).
Proof.
split. unfold abgrdiffrelint. unfold abgrdiffrelint'.
simpl. apply hinhfun. intro t2. set (a0 := pr1 (pr1 t2)).
split with a0. apply (pr2 t2). simpl. apply hinhfun.
intro t2. set (x0 := pr1 t2). split with (tpair _ x0 tt). apply (pr2 t2).
Defined.

Lemma iscomprelabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) :
iscomprelrel (eqrelabgrdiff X) (abgrdiffrelint X L).
Proof.
apply (iscomprelrellogeqf1 _ (logeqhrelsabgrdiff X)).
apply (iscomprelrellogeqf2 _ (logeqabgrdiffrelints X L)).
intros x x' x0 x0' r r0.
apply (iscomprelabmonoidfracrelint
_ (totalsubmonoid X) (isbinoptoispartbinop _ _ is) _ _ _ _ r r0).
Defined.
Opaque iscomprelabgrdiffrelint.

Definition abgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) :=
quotrel (iscomprelabgrdiffrelint X is).

Definition abgrdiffrel' (X : abmonoid) {L : hrel X} (is : isbinophrel L) : hrel (abgrdiff X) :=
λ x x', abmonoidfracrel X (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
(weqabgrdiff X x) (weqabgrdiff X x').

Definition logeqabgrdiffrels (X : abmonoid) {L : hrel X} (is : isbinophrel L) :
hrellogeq (abgrdiffrel' X is) (abgrdiffrel X is).
Proof.
intros x1 x2. split.
- assert (int : x x', isaprop (abgrdiffrel' X is x x' abgrdiffrel X is x x')).
{
intros x x'.
apply impred. intro.
apply (pr2 _).
}
generalize x1 x2. clear x1 x2.
apply (setquotuniv2prop _ (λ x x', make_hProp _ (int x x'))).
intros x x'.
change ((abgrdiffrelint' X L x x') (abgrdiffrelint _ L x x')).
apply (pr1 (logeqabgrdiffrelints X L x x')).
- assert (int : x x', isaprop (abgrdiffrel X is x x' abgrdiffrel' X is x x')).
intros x x'.
apply impred. intro.
apply (pr2 _).
generalize x1 x2. clear x1 x2.
apply (setquotuniv2prop _ (λ x x', make_hProp _ (int x x'))).
intros x x'.
change ((abgrdiffrelint X L x x') (abgrdiffrelint' _ L x x')).
apply (pr2 (logeqabgrdiffrelints X L x x')).
Defined.

Lemma istransabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : istrans L) :
istrans (abgrdiffrelint X L).
Proof.
apply (istranslogeqf (logeqabgrdiffrelints X L)).
intros a b c rab rbc.
apply (istransabmonoidfracrelint
_ (totalsubmonoid X) (isbinoptoispartbinop _ _ is) isl _ _ _ rab rbc).
Defined.
Opaque istransabgrdiffrelint.

Lemma istransabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : istrans L) :
istrans (abgrdiffrel X is).
Proof.
refine (istransquotrel _ _). apply istransabgrdiffrelint.
- apply is.
- apply isl.
Defined.

Lemma issymmabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : issymm L) :
issymm (abgrdiffrelint X L).
Proof.
apply (issymmlogeqf (logeqabgrdiffrelints X L)).
intros a b rab.
apply (issymmabmonoidfracrelint _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is) isl _ _ rab).
Defined.
Opaque issymmabgrdiffrelint.

Lemma issymmabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : issymm L) :
issymm (abgrdiffrel X is).
Proof.
refine (issymmquotrel _ _). apply issymmabgrdiffrelint.
- apply is.
- apply isl.
Defined.

Lemma isreflabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : isrefl L) :
isrefl (abgrdiffrelint X L).
Proof.
intro xa. unfold abgrdiffrelint. simpl.
apply hinhpr. split with (unel X). apply (isl _).
Defined.

Lemma isreflabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : isrefl L) :
isrefl (abgrdiffrel X is).
Proof.
refine (isreflquotrel _ _). apply isreflabgrdiffrelint.
- apply is.
- apply isl.
Defined.

Lemma ispoabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : ispreorder L) :
ispreorder (abgrdiffrelint X L).
Proof.
split with (istransabgrdiffrelint X is (pr1 isl)).
apply (isreflabgrdiffrelint X is (pr2 isl)).
Defined.

Lemma ispoabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : ispreorder L) :
ispreorder (abgrdiffrel X is).
Proof.
refine (ispoquotrel _ _). apply ispoabgrdiffrelint.
- apply is.
- apply isl.
Defined.

Lemma iseqrelabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : iseqrel L) :
iseqrel (abgrdiffrelint X L).
Proof.
split with (ispoabgrdiffrelint X is (pr1 isl)).
apply (issymmabgrdiffrelint X is (pr2 isl)).
Defined.

Lemma iseqrelabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : iseqrel L) :
iseqrel (abgrdiffrel X is).
Proof.
refine (iseqrelquotrel _ _). apply iseqrelabgrdiffrelint.
- apply is.
- apply isl.
Defined.

Lemma isantisymmnegabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L)
(isl : isantisymmneg L) : isantisymmneg (abgrdiffrel X is).
Proof.
apply (isantisymmneglogeqf (logeqabgrdiffrels X is)).
intros a b rab rba.
set (int := isantisymmnegabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
isl (weqabgrdiff X a) (weqabgrdiff X b) rab rba).
apply (invmaponpathsweq _ _ _ int).
Defined.

Lemma isantisymmabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : isantisymm L) :
isantisymm (abgrdiffrel X is).
Proof.
apply (isantisymmlogeqf (logeqabgrdiffrels X is)).
intros a b rab rba.
set (int := isantisymmabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
isl (weqabgrdiff X a) (weqabgrdiff X b) rab rba).
apply (invmaponpathsweq _ _ _ int).
Defined.
Opaque isantisymmabgrdiffrel.

Lemma isirreflabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : isirrefl L) :
isirrefl (abgrdiffrel X is).
Proof.
apply (isirrefllogeqf (logeqabgrdiffrels X is)).
intros a raa.
apply (isirreflabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
isl (weqabgrdiff X a) raa).
Defined.
Opaque isirreflabgrdiffrel.

Lemma isasymmabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : isasymm L) :
isasymm (abgrdiffrel X is).
Proof.
apply (isasymmlogeqf (logeqabgrdiffrels X is)).
intros a b rab rba.
apply (isasymmabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
isl (weqabgrdiff X a) (weqabgrdiff X b) rab rba).
Defined.
Opaque isasymmabgrdiffrel.

Lemma iscoasymmabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : iscoasymm L) :
iscoasymm (abgrdiffrel X is).
Proof.
apply (iscoasymmlogeqf (logeqabgrdiffrels X is)).
intros a b rab.
apply (iscoasymmabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
isl (weqabgrdiff X a) (weqabgrdiff X b) rab).
Defined.
Opaque iscoasymmabgrdiffrel.

Lemma istotalabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : istotal L) :
istotal (abgrdiffrel X is).
Proof.
apply (istotallogeqf (logeqabgrdiffrels X is)).
intros a b.
apply (istotalabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
isl (weqabgrdiff X a) (weqabgrdiff X b)).
Defined.
Opaque istotalabgrdiffrel.

Lemma iscotransabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) (isl : iscotrans L) :
iscotrans (abgrdiffrel X is).
Proof.
apply (iscotranslogeqf (logeqabgrdiffrels X is)).
intros a b c.
apply (iscotransabmonoidfracrel _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is)
isl (weqabgrdiff X a) (weqabgrdiff X b) (weqabgrdiff X c)).
Defined.
Opaque iscotransabgrdiffrel.

Lemma abgrdiffrelimpl (X : abmonoid) {L L' : hrel X} (is : isbinophrel L) (is' : isbinophrel L')
(impl : x x', L x x' L' x x') (x x' : abgrdiff X) (ql : abgrdiffrel X is x x') :
abgrdiffrel X is' x x'.
Proof.
generalize ql. refine (quotrelimpl _ _ _ _ _).
intros x0 x0'. simpl. apply hinhfun. intro t2. split with (pr1 t2).
apply (impl _ _ (pr2 t2)).
Defined.
Opaque abgrdiffrelimpl.

Lemma abgrdiffrellogeq (X : abmonoid) {L L' : hrel X} (is : isbinophrel L) (is' : isbinophrel L')
(lg : x x', L x x' L' x x') (x x' : abgrdiff X) :
(abgrdiffrel X is x x') (abgrdiffrel X is' x x').
Proof.
refine (quotrellogeq _ _ _ _ _). intros x0 x0'. split.
- simpl. apply hinhfun. intro t2. split with (pr1 t2).
apply (pr1 (lg _ _) (pr2 t2)).
- simpl. apply hinhfun. intro t2. split with (pr1 t2).
apply (pr2 (lg _ _) (pr2 t2)).
Defined.
Opaque abgrdiffrellogeq.

Lemma isbinopabgrdiffrelint (X : abmonoid) {L : hrel X} (is : isbinophrel L) :
@isbinophrel (setwithbinopdirprod X X) (abgrdiffrelint X L).
Proof.
apply (isbinophrellogeqf (logeqabgrdiffrelints X L)). split.
- intros a b c lab.
apply (pr1 (ispartbinopabmonoidfracrelint _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is))
(abgrdiffphi X a) (abgrdiffphi X b) (abgrdiffphi X c) tt lab).
- intros a b c lab.
apply (pr2 (ispartbinopabmonoidfracrelint _ (totalsubmonoid X) (isbinoptoispartbinop _ _ is))
(abgrdiffphi X a) (abgrdiffphi X b) (abgrdiffphi X c) tt lab).
Defined.
Opaque isbinopabgrdiffrelint.

Lemma isbinopabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L) :
@isbinophrel (abgrdiff X) (abgrdiffrel X is).
Proof.
intros.
apply (isbinopquotrel (binopeqrelabgrdiff X) (iscomprelabgrdiffrelint X is)).
apply (isbinopabgrdiffrelint X is).
Defined.

Definition isdecabgrdiffrelint (X : abmonoid) {L : hrel X}
(is : isinvbinophrel L) (isl : isdecrel L) : isdecrel (abgrdiffrelint X L).
Proof.
intros xa1 xa2.
set (x1 := pr1 xa1). set (a1 := pr2 xa1).
set (x2 := pr1 xa2). set (a2 := pr2 xa2).
assert (int : coprod (L (x1 + a2) (x2 + a1)) (neg (L (x1 + a2) (x2 + a1)))) by apply (isl _ _).
destruct int as [ l | nl ].
- apply ii1. unfold abgrdiffrelint. apply hinhpr. split with (unel X).
rewrite (runax X _). rewrite (runax X _). apply l.
- apply ii2. generalize nl. clear nl. apply negf. unfold abgrdiffrelint.
simpl. apply (@hinhuniv _ (make_hProp _ (pr2 (L _ _)))).
intro t2l. destruct t2l as [ c0a l ]. simpl. apply ((pr2 is) _ _ c0a l).
Defined.

Definition isdecabgrdiffrel (X : abmonoid) {L : hrel X} (is : isbinophrel L)
(isi : isinvbinophrel L) (isl : isdecrel L) : isdecrel (abgrdiffrel X is).
Proof.
refine (isdecquotrel _ _). apply isdecabgrdiffrelint.
- apply isi.
- apply isl.
Defined.

### Relations and the canonical homomorphism to abgrdiff

Lemma iscomptoabgrdiff (X : abmonoid) {L : hrel X} (is : isbinophrel L) :
iscomprelrelfun L (abgrdiffrel X is) (toabgrdiff X).
Proof.
unfold iscomprelrelfun.
intros x x' l.
change (abgrdiffrelint X L (make_dirprod x (unel X)) (make_dirprod x' (unel X))).
simpl. apply (hinhpr). split with (unel X).
apply ((pr2 is) _ _ 0). apply ((pr2 is) _ _ 0).
apply l.
Defined.
Opaque iscomptoabgrdiff.