From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
Require Import WildCat.Core WildCat.Square WildCat.Equiv Truncations.Core.
Require Import Groups.Group Groups.QuotientGroup AbelianGroup AbHom.

Local Open Scope mc_add_scope.

(** * Coequalizers of maps [f g : A $-> B] between abelian groups *)

(** Using the cokernel and addition and negation for the homs of abelian groups, we can define the coequalizer of two group homomorphisms as the cokernel of their difference. *)
Definition ab_coeq {A B : AbGroup} (f g : A $-> B)
  := ab_cokernel ((-f) + g).

Definition ab_coeq_in {A B : AbGroup} {f g : A $-> B} : B $-> ab_coeq f g.
A, B: AbGroup
f, g: A $-> B
B $-> ab_coeq f g
Proof.
A, B: AbGroup
f, g: A $-> B
B $-> ab_coeq f g
  exact grp_quotient_map.
Defined.

Definition ab_coeq_glue {A B : AbGroup} {f g : A $-> B}
  : ab_coeq_in (f:=f) (g:=g) $o f $== ab_coeq_in $o g.
A, B: AbGroup
f, g: A $-> B
ab_coeq_in $o f $== ab_coeq_in $o g
Proof.
A, B: AbGroup
f, g: A $-> B
ab_coeq_in $o f $== ab_coeq_in $o g
  intros x.
A, B: AbGroup
f, g: A $-> B
x: A
(ab_coeq_in $o f) x = (ab_coeq_in $o g) x
  napply qglue.
A, B: AbGroup
f, g: A $-> B
x: A
in_cosetL
  {|
    normalsubgroup_subgroup := grp_image (- f + g);
    normalsubgroup_isnormal := isnormal_ab_subgroup B (grp_image (- f + g))
  |} (f x) (g x)
  apply tr.
A, B: AbGroup
f, g: A $-> B
x: A
{x0 : A & (- f + g) x0 = - f x + g x}
  by exists x.
Defined.

Definition ab_coeq_rec {A B : AbGroup} {f g : A $-> B}
  {C : AbGroup} (i : B $-> C) (p : i $o f $== i $o g)
  : ab_coeq f g $-> C.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
ab_coeq f g $-> C
Proof.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
ab_coeq f g $-> C
  snapply (grp_quotient_rec _ _ i).
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
forall n : B,
{|
  normalsubgroup_subgroup := grp_image (- f + g);
  normalsubgroup_isnormal := isnormal_ab_subgroup B (grp_image (- f + g))
|} n -> i n = 0
  cbn.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
forall n : B, Trunc (-1) {x : A & - f x + g x = n} -> i n = 0
  intros b H.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
b: B
H: Trunc (-1) {x : A & - f x + g x = b}
i b = 0
  strip_truncations.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
b: B
H: {x : A & - f x + g x = b}
i b = 0
  destruct H as [a q].
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
b: B
a: A
q: - f a + g a = b
i b = 0
  destruct q; simpl.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
i (- f a + g a) = 0
  lhs napply grp_homo_op.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
i (- f a) + i (g a) = 0
  lhs napply (ap (+ _)).
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
i (- f a) = ?Goal
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
?Goal + i (g a) = 0
  1: apply grp_homo_inv.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
- i (f a) + i (g a) = 0
  apply grp_moveL_M1^-1.
A, B: AbGroup
f, g: A $-> B
C: AbGroup
i: B $-> C
p: i $o f $== i $o g
a: A
i (g a) = i (f a)
  exact (p a)^.
Defined.

Definition ab_coeq_rec_beta_in {A B : AbGroup} {f g : A $-> B}
  {C : AbGroup} (i : B $-> C) (p : i $o f $== i $o g)
  : ab_coeq_rec i p $o ab_coeq_in $== i
  := fun _ => idpath.

Definition ab_coeq_ind_hprop {A B f g} (P : @ab_coeq A B f g -> Type)
  `{forall x, IsHProp (P x)}
  (i : forall b, P (ab_coeq_in b))
  : forall x, P x.
A, B: AbGroup
f, g: A $-> B
P: ab_coeq f g -> Type
H: forall x : ab_coeq f g, IsHProp (P x)
i: forall b : B, P (ab_coeq_in b)
forall x : ab_coeq f g, P x
Proof.
A, B: AbGroup
f, g: A $-> B
P: ab_coeq f g -> Type
H: forall x : ab_coeq f g, IsHProp (P x)
i: forall b : B, P (ab_coeq_in b)
forall x : ab_coeq f g, P x
  rapply Quotient_ind_hprop.
A, B: AbGroup
f, g: A $-> B
P: ab_coeq f g -> Type
H: forall x : ab_coeq f g, IsHProp (P x)
i: forall b : B, P (ab_coeq_in b)
forall a : B,
P
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := grp_image (- f + g);
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup B (grp_image (- f + g))
        |})
     a)
  exact i.
Defined.

Definition ab_coeq_ind_homotopy {A B C f g}
  {l r : @ab_coeq A B f g $-> C}
  (p : l $o ab_coeq_in $== r $o ab_coeq_in)
  : l $== r.
A, B, C: AbGroup
f, g: A $-> B
l, r: ab_coeq f g $-> C
p: l $o ab_coeq_in $== r $o ab_coeq_in
l $== r
Proof.
A, B, C: AbGroup
f, g: A $-> B
l, r: ab_coeq f g $-> C
p: l $o ab_coeq_in $== r $o ab_coeq_in
l $== r
  srapply ab_coeq_ind_hprop.
A, B, C: AbGroup
f, g: A $-> B
l, r: ab_coeq f g $-> C
p: l $o ab_coeq_in $== r $o ab_coeq_in
forall b : B,
(fun x : ab_coeq f g =>
 (grp_homo_map : GroupHomomorphism (ab_coeq f g) C -> ab_coeq f g $-> C) l x =
 (grp_homo_map : GroupHomomorphism (ab_coeq f g) C -> ab_coeq f g $-> C) r x)
  (ab_coeq_in b)
  exact p.
Defined.

Definition functor_ab_coeq {A B : AbGroup} {f g : A $-> B} {A' B' : AbGroup} {f' g' : A' $-> B'}
  (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
  : ab_coeq f g $-> ab_coeq f' g'.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq f g $-> ab_coeq f' g'
Proof.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq f g $-> ab_coeq f' g'
  snapply ab_coeq_rec.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
B $-> ab_coeq f' g'
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
?i $o f $== ?i $o g
  1: exact (ab_coeq_in $o b).
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq_in $o b $o f $== ab_coeq_in $o b $o g
  refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq_in $o (b $o f) $== ab_coeq_in $o (b $o g)
  refine ((_ $@L p^$) $@ _ $@ (_ $@L q)).
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq_in $o (f' $o a) $== ab_coeq_in $o (g' $o a)
  refine (cat_assoc_opp _ _ _ $@ (_ $@R a) $@ cat_assoc _ _ _).
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq_in $o f' $== ab_coeq_in $o g'
  exact ab_coeq_glue.
Defined.

Definition functor2_ab_coeq {A B : AbGroup} {f g : A $-> B} {A' B' : AbGroup} {f' g' : A' $-> B'}
  {a a' : A $-> A'} {b b' : B $-> B'}
  (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
  (p' : f' $o a' $== b' $o f) (q' : g' $o a' $== b' $o g)
  (s : b $== b')
  : functor_ab_coeq a b p q $== functor_ab_coeq a' b' p' q'.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a, a': A $-> A'
b, b': B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
p': f' $o a' $== b' $o f
q': g' $o a' $== b' $o g
s: b $== b'
functor_ab_coeq a b p q $== functor_ab_coeq a' b' p' q'
Proof.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a, a': A $-> A'
b, b': B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
p': f' $o a' $== b' $o f
q': g' $o a' $== b' $o g
s: b $== b'
functor_ab_coeq a b p q $== functor_ab_coeq a' b' p' q'
  snapply ab_coeq_ind_homotopy.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a, a': A $-> A'
b, b': B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
p': f' $o a' $== b' $o f
q': g' $o a' $== b' $o g
s: b $== b'
functor_ab_coeq a b p q $o ab_coeq_in $==
functor_ab_coeq a' b' p' q' $o ab_coeq_in
  intros x.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a, a': A $-> A'
b, b': B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
p': f' $o a' $== b' $o f
q': g' $o a' $== b' $o g
s: b $== b'
x: B
(functor_ab_coeq a b p q $o ab_coeq_in) x =
(functor_ab_coeq a' b' p' q' $o ab_coeq_in) x
  exact (ap ab_coeq_in (s x)).
Defined.

Definition functor_ab_coeq_compose {A B : AbGroup} {f g : A $-> B}
  {A' B' : AbGroup} {f' g' : A' $-> B'}
  (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
  {A'' B'' : AbGroup} {f'' g'' : A'' $-> B''}
  (a' : A' $-> A'') (b' : B' $-> B'')
  (p' : f'' $o a' $== b' $o f') (q' : g'' $o a' $== b' $o g')
  : functor_ab_coeq a' b' p' q' $o functor_ab_coeq a b p q
  $== functor_ab_coeq (a' $o a) (b' $o b) (hconcat p p') (hconcat q q').
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
A'', B'': AbGroup
f'', g'': A'' $-> B''
a': A' $-> A''
b': B' $-> B''
p': f'' $o a' $== b' $o f'
q': g'' $o a' $== b' $o g'
functor_ab_coeq a' b' p' q' $o functor_ab_coeq a b p q $==
functor_ab_coeq (a' $o a) (b' $o b) (p $@h p') (q $@h q')
Proof.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
A'', B'': AbGroup
f'', g'': A'' $-> B''
a': A' $-> A''
b': B' $-> B''
p': f'' $o a' $== b' $o f'
q': g'' $o a' $== b' $o g'
functor_ab_coeq a' b' p' q' $o functor_ab_coeq a b p q $==
functor_ab_coeq (a' $o a) (b' $o b) (p $@h p') (q $@h q')
  snapply ab_coeq_ind_homotopy.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $-> A'
b: B $-> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
A'', B'': AbGroup
f'', g'': A'' $-> B''
a': A' $-> A''
b': B' $-> B''
p': f'' $o a' $== b' $o f'
q': g'' $o a' $== b' $o g'
functor_ab_coeq a' b' p' q' $o functor_ab_coeq a b p q $o ab_coeq_in $==
functor_ab_coeq (a' $o a) (b' $o b) (p $@h p') (q $@h q') $o ab_coeq_in
  simpl; reflexivity.
Defined.

Definition functor_ab_coeq_id {A B : AbGroup} (f g : A $-> B)
  : functor_ab_coeq (Id _) (Id _) (hrefl f) (hrefl g) $== Id _.
A, B: AbGroup
f, g: A $-> B
functor_ab_coeq (Id A) (Id B) (hrefl f) (hrefl g) $== Id (ab_coeq f g)
Proof.
A, B: AbGroup
f, g: A $-> B
functor_ab_coeq (Id A) (Id B) (hrefl f) (hrefl g) $== Id (ab_coeq f g)
  snapply ab_coeq_ind_homotopy.
A, B: AbGroup
f, g: A $-> B
functor_ab_coeq (Id A) (Id B) (hrefl f) (hrefl g) $o ab_coeq_in $==
Id (ab_coeq f g) $o ab_coeq_in
  reflexivity.
Defined.

Definition grp_iso_ab_coeq {A B : AbGroup} {f g : A $-> B}
  {A' B' : AbGroup} {f' g' : A' $-> B'}
  (a : A $<~> A') (b : B $<~> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
  : ab_coeq f g $<~> ab_coeq f' g'.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq f g $<~> ab_coeq f' g'
Proof.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq f g $<~> ab_coeq f' g'
  snapply cate_adjointify.
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq f g $-> ab_coeq f' g'
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq f' g' $-> ab_coeq f g
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
?f $o ?g $== Id (ab_coeq f' g')
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
?g $o ?f $== Id (ab_coeq f g)
  -
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq f g $-> ab_coeq f' g' exact (functor_ab_coeq a b p q).
  -
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
ab_coeq f' g' $-> ab_coeq f g exact (functor_ab_coeq a^-1$ b^-1$ (hinverse a _ p) (hinverse a _ q)).
  -
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
functor_ab_coeq a b p q $o functor_ab_coeq a^-1$ b^-1$ p ^h$ q ^h$ $==
Id (ab_coeq f' g') nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
      $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
b $o b^-1$ $== Id B'
    exact (cate_isretr b).
  -
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
functor_ab_coeq a^-1$ b^-1$ p ^h$ q ^h$ $o functor_ab_coeq a b p q $==
Id (ab_coeq f g) nrefine (functor_ab_coeq_compose _ _ _ _ _ _ _ _
      $@ functor2_ab_coeq _ _ _ _ _ $@ functor_ab_coeq_id _ _).
A, B: AbGroup
f, g: A $-> B
A', B': AbGroup
f', g': A' $-> B'
a: A $<~> A'
b: B $<~> B'
p: f' $o a $== b $o f
q: g' $o a $== b $o g
b^-1$ $o b $== Id B
    exact (cate_issect b).
Defined.