From HoTT Require Import Basics Types.From HoTT Require Import Basics Types.
Require Import WildCat.Core.
Require Import Truncations.Core.
Require Import Algebra.Groups.Group.
Require Import Colimits.Coeq.
Require Import Algebra.Groups.FreeProduct.
Require Import List.Core.

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

(** Coequalizers of group homomorphisms *)

Definition GroupCoeq {A B : Group} (f g : A $-> B) : Group.
A, B: Group
f, g: A $-> B
Group
Proof.
A, B: Group
f, g: A $-> B
Group
  napply (@AmalgamatedFreeProduct (FreeProduct A A) A B).
A, B: Group
f, g: A $-> B
GroupHomomorphism (FreeProduct A A) A
A, B: Group
f, g: A $-> B
GroupHomomorphism (FreeProduct A A) B
  -
A, B: Group
f, g: A $-> B
GroupHomomorphism (FreeProduct A A) A exact (FreeProduct_rec (Id _) (Id _)).
  -
A, B: Group
f, g: A $-> B
GroupHomomorphism (FreeProduct A A) B exact (FreeProduct_rec f g).
Defined.

Definition groupcoeq_in {A B : Group} {f g : A $-> B}
  : B $-> GroupCoeq f g
  := amal_inr.

Definition groupcoeq_glue {A B : Group} {f g : A $-> B}
  : groupcoeq_in (f:=f) (g:=g) $o f $== groupcoeq_in $o g.
A, B: Group
f, g: A $-> B
groupcoeq_in $o f $== groupcoeq_in $o g
Proof.
A, B: Group
f, g: A $-> B
groupcoeq_in $o f $== groupcoeq_in $o g
  intros x; simpl.
A, B: Group
f, g: A $-> B
x: A
amal_eta [inr (f x)]%list = amal_eta [inr (g x)]%list
  rewrite <- (right_identity (f x)).
A, B: Group
f, g: A $-> B
x: A
amal_eta [inr (f x * 1)]%list = amal_eta [inr (g x)]%list
  rewrite <- (right_identity (g x)).
A, B: Group
f, g: A $-> B
x: A
amal_eta [inr (f x * 1)]%list = amal_eta [inr (g x * 1)]%list
  rhs_V napply (amal_glue (freeproduct_inr x)).
A, B: Group
f, g: A $-> B
x: A
amal_eta [inr (f x * 1)]%list =
(amal_inl $o FreeProduct_rec grp_homo_id grp_homo_id) (freeproduct_inr x)
  symmetry.
A, B: Group
f, g: A $-> B
x: A
(amal_inl $o FreeProduct_rec grp_homo_id grp_homo_id) (freeproduct_inr x) =
amal_eta [inr (f x * 1)]%list
  napply (amal_glue (freeproduct_inl x)).
Defined.

Definition groupcoeq_rec {A B C : Group} (f g : A $-> B)
  (h : B $-> C) (p : h $o f $== h $o g)
  : GroupCoeq f g $-> C.
A, B, C: Group
f, g: A $-> B
h: B $-> C
p: h $o f $== h $o g
GroupCoeq f g $-> C
Proof.
A, B, C: Group
f, g: A $-> B
h: B $-> C
p: h $o f $== h $o g
GroupCoeq f g $-> C
  rapply (AmalgamatedFreeProduct_rec C (h $o f) h).
A, B, C: Group
f, g: A $-> B
h: B $-> C
p: h $o f $== h $o g
h $o f $o FreeProduct_rec (Id A) (Id A) $== h $o FreeProduct_rec f g
  snapply freeproduct_ind_homotopy.
A, B, C: Group
f, g: A $-> B
h: B $-> C
p: h $o f $== h $o g
h $o f $o FreeProduct_rec (Id A) (Id A) $o freeproduct_inl $==
h $o FreeProduct_rec f g $o freeproduct_inl
A, B, C: Group
f, g: A $-> B
h: B $-> C
p: h $o f $== h $o g
h $o f $o FreeProduct_rec (Id A) (Id A) $o freeproduct_inr $==
h $o FreeProduct_rec f g $o freeproduct_inr
  (** The goals generated are very simple, but we give explicit proofs with wild cat terms to stop Coq from unfolding terms when checking the proof. Note that the category of groups is definitionally associative. *)
  -
A, B, C: Group
f, g: A $-> B
h: B $-> C
p: h $o f $== h $o g
h $o f $o FreeProduct_rec (Id A) (Id A) $o freeproduct_inl $==
h $o FreeProduct_rec f g $o freeproduct_inl refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
A, B, C: Group
f, g: A $-> B
h: B $-> C
p: h $o f $== h $o g
h $o f $o (FreeProduct_rec (Id A) (Id A) $o freeproduct_inl) $==
h $o (FreeProduct_rec f g $o freeproduct_inl)
    exact ((_ $@L freeproduct_rec_beta_inl _ _) $@ cat_idr _
      $@ (_ $@L freeproduct_rec_beta_inl _ _)^$).
  -
A, B, C: Group
f, g: A $-> B
h: B $-> C
p: h $o f $== h $o g
h $o f $o FreeProduct_rec (Id A) (Id A) $o freeproduct_inr $==
h $o FreeProduct_rec f g $o freeproduct_inr refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
A, B, C: Group
f, g: A $-> B
h: B $-> C
p: h $o f $== h $o g
h $o f $o (FreeProduct_rec (Id A) (Id A) $o freeproduct_inr) $==
h $o (FreeProduct_rec f g $o freeproduct_inr)
    exact ((_ $@L freeproduct_rec_beta_inr _ _) $@ (cat_idr _ $@ p)
      $@ (_ $@L freeproduct_rec_beta_inr _ _)^$).
Defined.

(** TODO: unify this with [groupcoeq_rec]. It will require doing the analogous thing for [AmalgamatedFreeProduct]. *)
Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : A $-> B)
  : {h : B $-> C & h $o f $== h $o g} <~> (GroupCoeq f g $-> C).
H: Funext
A, B, C: Group
f, g: A $-> B
{h : B $-> C & h $o f $== h $o g} <~> (GroupCoeq f g $-> C)
Proof.
H: Funext
A, B, C: Group
f, g: A $-> B
{h : B $-> C & h $o f $== h $o g} <~> (GroupCoeq f g $-> C)
  nrefine (equiv_amalgamatedfreeproduct_rec C oE _).
H: Funext
A, B, C: Group
f, g: A $-> B
{h : B $-> C & h $o f $== h $o g} <~>
{h : A $-> C &
{k : B $-> C &
h $o FreeProduct_rec (Id A) (Id A) $== k $o FreeProduct_rec f g}}
  nrefine (equiv_sigma_symm _ oE _).
H: Funext
A, B, C: Group
f, g: A $-> B
{h : B $-> C & h $o f $== h $o g} <~>
{a : B $-> C &
{b : A $-> C &
b $o FreeProduct_rec (Id A) (Id A) $== a $o FreeProduct_rec f g}}
  napply equiv_functor_sigma_id.
H: Funext
A, B, C: Group
f, g: A $-> B
forall a : B $-> C,
a $o f $== a $o g <~>
{b : A $-> C &
b $o FreeProduct_rec (Id A) (Id A) $== a $o FreeProduct_rec f g}
  intros h.
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h $o f $== h $o g <~>
{b : A $-> C &
b $o FreeProduct_rec (Id A) (Id A) $== h $o FreeProduct_rec f g}
  transitivity {b : A $-> C & (b $== h $o f) * (b $== h $o g)}%type.
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h $o f $== h $o g <~> {b : A $-> C & ((b $== h $o f) * (b $== h $o g))%type}
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
{b : A $-> C & ((b $== h $o f) * (b $== h $o g))%type} <~>
{b : A $-> C &
b $o FreeProduct_rec (Id A) (Id A) $== h $o FreeProduct_rec f g}
  {
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h $o f $== h $o g <~> {b : A $-> C & ((b $== h $o f) * (b $== h $o g))%type} nrefine (equiv_functor_sigma_id (fun b => equiv_sigma_prod0 _ _) oE _).
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h $o f $== h $o g <~> {b : A $-> C & {_ : b $== h $o f & b $== h $o g}}
    symmetry.
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
{b : A $-> C & {_ : b $== h $o f & b $== h $o g}} <~> h $o f $== h $o g
    nrefine (_ oE (equiv_sigma_assoc' _ _)).
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
{ap : {a : A $-> C & a $== h $o f} & ap.1 $== h $o g} <~> h $o f $== h $o g
    transitivity {fp' : {f' : A $-> C & f' = h $o f} & fp'.1 $== h $o g}.
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
{ap : {a : A $-> C & a $== h $o f} & ap.1 $== h $o g} <~>
{fp' : {f' : A $-> C & f' = h $o f} & fp'.1 $== h $o g}
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
{fp' : {f' : A $-> C & f' = h $o f} & fp'.1 $== h $o g} <~> h $o f $== h $o g
    -
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
{ap : {a : A $-> C & a $== h $o f} & ap.1 $== h $o g} <~>
{fp' : {f' : A $-> C & f' = h $o f} & fp'.1 $== h $o g} exact (equiv_functor_sigma_pb
        (equiv_functor_sigma_id (fun _ => equiv_path_grouphomomorphism))).
    -
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
{fp' : {f' : A $-> C & f' = h $o f} & fp'.1 $== h $o g} <~> h $o f $== h $o g exact (@equiv_contr_sigma _ _ (contr_basedpaths' (h $o f))). }
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
{b : A $-> C & ((b $== h $o f) * (b $== h $o g))%type} <~>
{b : A $-> C &
b $o FreeProduct_rec (Id A) (Id A) $== h $o FreeProduct_rec f g}
  snapply equiv_functor_sigma_id.
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
forall a : A $-> C,
(fun b : A $-> C => ((b $== h $o f) * (b $== h $o g))%type) a <~>
(fun b : A $-> C =>
 b $o FreeProduct_rec (Id A) (Id A) $== h $o FreeProduct_rec f g) a
  intros h'; cbn beta.
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h': A $-> C
(h' $== h $o f) * (h' $== h $o g) <~>
h' $o FreeProduct_rec (Id A) (Id A) $== h $o FreeProduct_rec f g
  nrefine (equiv_freeproduct_ind_homotopy _ _ oE _).
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h': A $-> C
(h' $== h $o f) * (h' $== h $o g) <~>
(h' $o FreeProduct_rec (Id A) (Id A) $o freeproduct_inl $==
 h $o FreeProduct_rec f g $o freeproduct_inl) *
(h' $o FreeProduct_rec (Id A) (Id A) $o freeproduct_inr $==
 h $o FreeProduct_rec f g $o freeproduct_inr)
  snapply equiv_functor_prod'.
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h': A $-> C
h' $== h $o f <~>
h' $o FreeProduct_rec (Id A) (Id A) $o freeproduct_inl $==
h $o FreeProduct_rec f g $o freeproduct_inl
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h': A $-> C
h' $== h $o g <~>
h' $o FreeProduct_rec (Id A) (Id A) $o freeproduct_inr $==
h $o FreeProduct_rec f g $o freeproduct_inr
  -
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h': A $-> C
h' $== h $o f <~>
h' $o FreeProduct_rec (Id A) (Id A) $o freeproduct_inl $==
h $o FreeProduct_rec f g $o freeproduct_inl snapply equiv_functor_forall_id; simpl; intros a.
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h': A $-> C
a: A
h' a = h (f a) <~> h' (a * 1) = h (f a * 1)
    by rewrite 2 grp_unit_r.
  -
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h': A $-> C
h' $== h $o g <~>
h' $o FreeProduct_rec (Id A) (Id A) $o freeproduct_inr $==
h $o FreeProduct_rec f g $o freeproduct_inr snapply equiv_functor_forall_id; simpl; intros a.
H: Funext
A, B, C: Group
f, g: A $-> B
h: B $-> C
h': A $-> C
a: A
h' a = h (g a) <~> h' (a * 1) = h (g a * 1)
    by rewrite 2 grp_unit_r.
Defined.

Definition groupcoeq_ind_hprop {G H : Group} {f g : G $-> H}
  (P : GroupCoeq f g -> Type) `{forall x, IsHProp (P x)}
  (c : forall h, P (groupcoeq_in h))
  (Hop : forall x y, P x -> P y -> P (x * y))
  : forall x, P x.
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x : GroupCoeq f g, IsHProp (P x)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x y : GroupCoeq f g, P x -> P y -> P (x * y)
forall x : GroupCoeq f g, P x
Proof.
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x : GroupCoeq f g, IsHProp (P x)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x y : GroupCoeq f g, P x -> P y -> P (x * y)
forall x : GroupCoeq f g, P x
  snapply amalgamatedfreeproduct_ind_hprop.
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x : GroupCoeq f g, IsHProp (P x)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x y : GroupCoeq f g, P x -> P y -> P (x * y)
forall
x : AmalgamatedFreeProduct (FreeProduct_rec (Id G) (Id G))
      (FreeProduct_rec f g),
IsHProp (P x)
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x : GroupCoeq f g, IsHProp (P x)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x y : GroupCoeq f g, P x -> P y -> P (x * y)
forall a : G, P (amal_inl a)
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x : GroupCoeq f g, IsHProp (P x)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x y : GroupCoeq f g, P x -> P y -> P (x * y)
forall b : H, P (amal_inr b)
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x : GroupCoeq f g, IsHProp (P x)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x y : GroupCoeq f g, P x -> P y -> P (x * y)
forall
x
 y : AmalgamatedFreeProduct (FreeProduct_rec (Id G) (Id G))
       (FreeProduct_rec f g),
P x -> P y -> P (x * y)
  -
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x : GroupCoeq f g, IsHProp (P x)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x y : GroupCoeq f g, P x -> P y -> P (x * y)
forall
x : AmalgamatedFreeProduct (FreeProduct_rec (Id G) (Id G))
      (FreeProduct_rec f g),
IsHProp (P x) exact _.
  -
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x : GroupCoeq f g, IsHProp (P x)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x y : GroupCoeq f g, P x -> P y -> P (x * y)
forall a : G, P (amal_inl a) intros x.
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x0 : GroupCoeq f g, IsHProp (P x0)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x0 y : GroupCoeq f g, P x0 -> P y -> P (x0 * y)
x: G
P (amal_inl x)
    rewrite <- (right_identity x).
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x0 : GroupCoeq f g, IsHProp (P x0)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x0 y : GroupCoeq f g, P x0 -> P y -> P (x0 * y)
x: G
P (amal_inl (x * 1))
    refine ((amal_glue (freeproduct_inl x))^ #_).
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x0 : GroupCoeq f g, IsHProp (P x0)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x0 y : GroupCoeq f g, P x0 -> P y -> P (x0 * y)
x: G
P ((amal_inr $o FreeProduct_rec f g) (freeproduct_inl x))
    simpl.
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x0 : GroupCoeq f g, IsHProp (P x0)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x0 y : GroupCoeq f g, P x0 -> P y -> P (x0 * y)
x: G
P (amal_eta [inr (f x * 1)]%list)
    rewrite (right_identity (f x)).
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x0 : GroupCoeq f g, IsHProp (P x0)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x0 y : GroupCoeq f g, P x0 -> P y -> P (x0 * y)
x: G
P (amal_eta [inr (f x)]%list)
    exact (c (f x)).
  -
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x : GroupCoeq f g, IsHProp (P x)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x y : GroupCoeq f g, P x -> P y -> P (x * y)
forall b : H, P (amal_inr b) exact c.
  -
G, H: Group
f, g: G $-> H
P: GroupCoeq f g -> Type
H0: forall x : GroupCoeq f g, IsHProp (P x)
c: forall h : H, P (groupcoeq_in h)
Hop: forall x y : GroupCoeq f g, P x -> P y -> P (x * y)
forall
x
 y : AmalgamatedFreeProduct (FreeProduct_rec (Id G) (Id G))
       (FreeProduct_rec f g),
P x -> P y -> P (x * y) exact Hop. (* Slow, ~0.09s *)
Defined. (* Slow, ~0.09s *)

Definition groupcoeq_ind_homotopy {G H K : Group} {f g : G $-> H}
  {h h' : GroupCoeq f g $-> K}
  (r : h $o groupcoeq_in $== h' $o groupcoeq_in)
  : h $== h'.
G, H, K: Group
f, g: G $-> H
h, h': GroupCoeq f g $-> K
r: h $o groupcoeq_in $== h' $o groupcoeq_in
h $== h'
Proof.
G, H, K: Group
f, g: G $-> H
h, h': GroupCoeq f g $-> K
r: h $o groupcoeq_in $== h' $o groupcoeq_in
h $== h'
  rapply (groupcoeq_ind_hprop _ r).
G, H, K: Group
f, g: G $-> H
h, h': GroupCoeq f g $-> K
r: h $o groupcoeq_in $== h' $o groupcoeq_in
forall x y : GroupCoeq f g,
h x = h' x -> h y = h' y -> h (x * y) = h' (x * y)
  intros x y p q; by napply grp_homo_op_agree.
Defined.

Definition functor_groupcoeq
  {G H : Group} {f g : G $-> H} {G' H' : Group} {f' g' : G' $-> H'}
  (h : G $-> G') (k : H $-> H')
  (p : k $o f $== f' $o h) (q : k $o g $== g' $o h)
  : GroupCoeq f g $-> GroupCoeq f' g'.
G, H: Group
f, g: G $-> H
G', H': Group
f', g': G' $-> H'
h: G $-> G'
k: H $-> H'
p: k $o f $== f' $o h
q: k $o g $== g' $o h
GroupCoeq f g $-> GroupCoeq f' g'
Proof.
G, H: Group
f, g: G $-> H
G', H': Group
f', g': G' $-> H'
h: G $-> G'
k: H $-> H'
p: k $o f $== f' $o h
q: k $o g $== g' $o h
GroupCoeq f g $-> GroupCoeq f' g'
  refine (groupcoeq_rec f g (groupcoeq_in $o k) _).
G, H: Group
f, g: G $-> H
G', H': Group
f', g': G' $-> H'
h: G $-> G'
k: H $-> H'
p: k $o f $== f' $o h
q: k $o g $== g' $o h
groupcoeq_in $o k $o f $== groupcoeq_in $o k $o g
  refine (cat_assoc _ _ _ $@ _ $@ cat_assoc_opp _ _ _).
G, H: Group
f, g: G $-> H
G', H': Group
f', g': G' $-> H'
h: G $-> G'
k: H $-> H'
p: k $o f $== f' $o h
q: k $o g $== g' $o h
groupcoeq_in $o (k $o f) $== groupcoeq_in $o (k $o g) 
  refine ((_ $@L p) $@ _ $@ (_ $@L q^$)).
G, H: Group
f, g: G $-> H
G', H': Group
f', g': G' $-> H'
h: G $-> G'
k: H $-> H'
p: k $o f $== f' $o h
q: k $o g $== g' $o h
groupcoeq_in $o (f' $o h) $== groupcoeq_in $o (g' $o h)
  refine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_assoc _ _ _).
G, H: Group
f, g: G $-> H
G', H': Group
f', g': G' $-> H'
h: G $-> G'
k: H $-> H'
p: k $o f $== f' $o h
q: k $o g $== g' $o h
groupcoeq_in $o f' $== groupcoeq_in $o g' 
  apply groupcoeq_glue.
Defined.