Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core.
Require Import Truncations.Core.
Require Import Algebra.Groups.Group.
Require Import Colimits.Coeq.
Require Import Algebra.Groups.FreeProduct.

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
  rapply (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
  1,2: apply FreeProduct_rec.
A, B: Group
f, g: A $-> B
GroupHomomorphism A A
A, B: Group
f, g: A $-> B
GroupHomomorphism A A
A, B: Group
f, g: A $-> B
GroupHomomorphism A B
A, B: Group
f, g: A $-> B
GroupHomomorphism A B
  +
A, B: Group
f, g: A $-> B
GroupHomomorphism A A exact grp_homo_id.
  +
A, B: Group
f, g: A $-> B
GroupHomomorphism A A exact grp_homo_id.
  +
A, B: Group
f, g: A $-> B
GroupHomomorphism A B exact f.
  +
A, B: Group
f, g: A $-> B
GroupHomomorphism A B exact g.
Defined.

Definition equiv_groupcoeq_rec `{Funext} {A B C : Group} (f g : GroupHomomorphism A B)
  : {h : B $-> C & h o f == h o g} <~> (GroupCoeq f g $-> C).
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
{h : B $-> C & h o f == h o g} <~>
(GroupCoeq f g $-> C)
Proof.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
{h : B $-> C & h o f == h o g} <~>
(GroupCoeq f g $-> C)
  refine (equiv_amalgamatedfreeproduct_rec _ _ _ _ _ _ oE _).
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
{h : B $-> C &
(fun x : A => h (f x)) == (fun x : A => h (g x))} <~>
{h : GroupHomomorphism A C &
{k : GroupHomomorphism B C &
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 k (FreeProduct_rec A A B f g x))}}
  refine (equiv_sigma_symm _ oE _).
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
{h : B $-> C &
(fun x : A => h (f x)) == (fun x : A => h (g x))} <~>
{a : GroupHomomorphism B C &
{b : GroupHomomorphism A C &
(fun x : FreeProduct A A =>
 b (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 a (FreeProduct_rec A A B f g x))}}
  apply equiv_functor_sigma_id.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
forall a : B $-> C,
(fun x : A => a (f x)) == (fun x : A => a (g x)) <~>
{b : GroupHomomorphism A C &
(fun x : FreeProduct A A =>
 b (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 a (FreeProduct_rec A A B f g x))}
  intros h.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
(fun x : A => h (f x)) == (fun x : A => h (g x)) <~>
{b : GroupHomomorphism A C &
(fun x : FreeProduct A A =>
 b (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))}
  snrapply equiv_adjointify.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
(fun x : A => h (f x)) == (fun x : A => h (g x)) ->
{b : GroupHomomorphism A C &
(fun x : FreeProduct A A =>
 b (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))}
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
{b : GroupHomomorphism A C &
(fun x : FreeProduct A A =>
 b (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))} ->
(fun x : A => h (f x)) == (fun x : A => h (g x))
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
?f o ?g == idmap
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
?g o ?f == idmap
  {
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
(fun x : A => h (f x)) == (fun x : A => h (g x)) ->
{b : GroupHomomorphism A C &
(fun x : FreeProduct A A =>
 b (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))} intros p.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
{b : GroupHomomorphism A C &
(fun x : FreeProduct A A =>
 b (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))}
    exists (grp_homo_compose h f).
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
(fun x : FreeProduct A A =>
 grp_homo_compose h f
   (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
    hnf; intro x.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
x: FreeProduct A A
grp_homo_compose h f
  (FreeProduct_rec A A A grp_homo_id grp_homo_id x) =
h (FreeProduct_rec A A B f g x)
    refine (p _ @ _).
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
x: FreeProduct A A
h
  (g (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) =
h (FreeProduct_rec A A B f g x)
    revert x.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
forall x : FreeProduct A A,
h
  (g (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) =
h (FreeProduct_rec A A B f g x)
    rapply Trunc_ind.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
forall
a : Coeq
      (FreeProduct.map1 grp_trivial A A
         (grp_trivial_rec A))
      (FreeProduct.map2 grp_trivial A A
         (grp_trivial_rec A)),
h
  (g
     (FreeProduct_rec A A A grp_homo_id grp_homo_id
        (tr a))) =
h (FreeProduct_rec A A B f g (tr a))
    srapply Coeq_ind.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
forall a : FreeProduct.Words A A,
(fun
   w : Coeq
         (FreeProduct.map1 grp_trivial A A
            (grp_trivial_rec A))
         (FreeProduct.map2 grp_trivial A A
            (grp_trivial_rec A)) =>
 h
   (g
      (FreeProduct_rec A A A grp_homo_id grp_homo_id
         (tr w))) =
 h (FreeProduct_rec A A B f g (tr w))) (coeq a)
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
forall
b : FreeProduct.pc1 A A + FreeProduct.pc2 A A +
    FreeProduct.pc3 grp_trivial A A +
    FreeProduct.pc4 A A + FreeProduct.pc5 A A,
transport
  (fun
     w : Coeq
           (FreeProduct.map1 grp_trivial A A
              (grp_trivial_rec A))
           (FreeProduct.map2 grp_trivial A A
              (grp_trivial_rec A)) =>
   h
     (g
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           (tr w))) =
   h (FreeProduct_rec A A B f g (tr w))) (cglue b)
  (?coeq'
     (FreeProduct.map1 grp_trivial A A
        (grp_trivial_rec A) b)) =
?coeq'
  (FreeProduct.map2 grp_trivial A A
     (grp_trivial_rec A) b)
    2: intros; apply path_ishprop.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
forall a : FreeProduct.Words A A,
(fun
   w : Coeq
         (FreeProduct.map1 grp_trivial A A
            (grp_trivial_rec A))
         (FreeProduct.map2 grp_trivial A A
            (grp_trivial_rec A)) =>
 h
   (g
      (FreeProduct_rec A A A grp_homo_id grp_homo_id
         (tr w))) =
 h (FreeProduct_rec A A B f g (tr w))) (coeq a)
    intros w.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
w: FreeProduct.Words A A
(fun
   w : Coeq
         (FreeProduct.map1 grp_trivial A A
            (grp_trivial_rec A))
         (FreeProduct.map2 grp_trivial A A
            (grp_trivial_rec A)) =>
 h
   (g
      (FreeProduct_rec A A A grp_homo_id grp_homo_id
         (tr w))) =
 h (FreeProduct_rec A A B f g (tr w))) (coeq w) hnf.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
w: FreeProduct.Words A A
h
  (g
     (FreeProduct_rec A A A grp_homo_id grp_homo_id
        (tr (coeq w)))) =
h (FreeProduct_rec A A B f g (tr (coeq w)))
    induction w.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
h
  (g
     (FreeProduct_rec A A A grp_homo_id grp_homo_id
        (tr (coeq Core.nil)))) =
h (FreeProduct_rec A A B f g (tr (coeq Core.nil)))
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
a: (A + A)%type
w: Core.list (A + A)
IHw: h (g (FreeProduct_rec A A A grp_homo_id grp_homo_id (tr (coeq w)))) =
h (FreeProduct_rec A A B f g (tr (coeq w)))
h
  (g
     (FreeProduct_rec A A A grp_homo_id grp_homo_id
        (tr (coeq (Core.cons a w))))) =
h
  (FreeProduct_rec A A B f g
     (tr (coeq (Core.cons a w))))
    1: apply ap, grp_homo_unit.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
a: (A + A)%type
w: Core.list (A + A)
IHw: h (g (FreeProduct_rec A A A grp_homo_id grp_homo_id (tr (coeq w)))) =
h (FreeProduct_rec A A B f g (tr (coeq w)))
h
  (g
     (FreeProduct_rec A A A grp_homo_id grp_homo_id
        (tr (coeq (Core.cons a w))))) =
h
  (FreeProduct_rec A A B f g
     (tr (coeq (Core.cons a w))))
    simpl.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
a: (A + A)%type
w: Core.list (A + A)
IHw: h (g (FreeProduct_rec A A A grp_homo_id grp_homo_id (tr (coeq w)))) =
h (FreeProduct_rec A A B f g (tr (coeq w)))
h
  (g
     (match a with
      | inl g | inr g => fun x : A => g * x
      end
        (Core.fold_right
           (fun X0 : A + A =>
            match X0 with
            | inl g | inr g => fun x : A => g * x
            end) mon_unit w))) =
h
  (match a with
   | inl g => fun x : B => f g * x
   | inr g0 => fun x : B => g g0 * x
   end
     (Core.fold_right
        (fun X0 : A + A =>
         match X0 with
         | inl g => fun x : B => f g * x
         | inr g0 => fun x : B => g g0 * x
         end) mon_unit w))
    destruct a as [a|a].
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
a: A
w: Core.list (A + A)
IHw: h (g (FreeProduct_rec A A A grp_homo_id grp_homo_id (tr (coeq w)))) =
h (FreeProduct_rec A A B f g (tr (coeq w)))
h
  (g
     (a *
      Core.fold_right
        (fun X0 : A + A =>
         match X0 with
         | inl g | inr g => fun x : A => g * x
         end) mon_unit w)) =
h
  (f a *
   Core.fold_right
     (fun X0 : A + A =>
      match X0 with
      | inl g => fun x : B => f g * x
      | inr g0 => fun x : B => g g0 * x
      end) mon_unit w)
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
a: A
w: Core.list (A + A)
IHw: h (g (FreeProduct_rec A A A grp_homo_id grp_homo_id (tr (coeq w)))) =
h (FreeProduct_rec A A B f g (tr (coeq w)))
h
  (g
     (a *
      Core.fold_right
        (fun X0 : A + A =>
         match X0 with
         | inl g | inr g => fun x : A => g * x
         end) mon_unit w)) =
h
  (g a *
   Core.fold_right
     (fun X0 : A + A =>
      match X0 with
      | inl g => fun x : B => f g * x
      | inr g0 => fun x : B => g g0 * x
      end) mon_unit w)
    1,2: refine (ap _ (grp_homo_op _ _ _) @ _).
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
a: A
w: Core.list (A + A)
IHw: h (g (FreeProduct_rec A A A grp_homo_id grp_homo_id (tr (coeq w)))) =
h (FreeProduct_rec A A B f g (tr (coeq w)))
h
  (g a *
   g
     (Core.fold_right
        (fun X0 : A + A =>
         match X0 with
         | inl g | inr g => fun x : A => g * x
         end) mon_unit w)) =
h
  (f a *
   Core.fold_right
     (fun X0 : A + A =>
      match X0 with
      | inl g => fun x : B => f g * x
      | inr g0 => fun x : B => g g0 * x
      end) mon_unit w)
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
a: A
w: Core.list (A + A)
IHw: h (g (FreeProduct_rec A A A grp_homo_id grp_homo_id (tr (coeq w)))) =
h (FreeProduct_rec A A B f g (tr (coeq w)))
h
  (g a *
   g
     (Core.fold_right
        (fun X0 : A + A =>
         match X0 with
         | inl g | inr g => fun x : A => g * x
         end) mon_unit w)) =
h
  (g a *
   Core.fold_right
     (fun X0 : A + A =>
      match X0 with
      | inl g => fun x : B => f g * x
      | inr g0 => fun x : B => g g0 * x
      end) mon_unit w)
    1,2: refine (grp_homo_op _ _ _ @ _ @ (grp_homo_op _ _ _)^); f_ap.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
a: A
w: Core.list (A + A)
IHw: h (g (FreeProduct_rec A A A grp_homo_id grp_homo_id (tr (coeq w)))) =
h (FreeProduct_rec A A B f g (tr (coeq w)))
h (g a) = h (f a)
    symmetry.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
p: (fun x : A => h (f x)) == (fun x : A => h (g x))
a: A
w: Core.list (A + A)
IHw: h (g (FreeProduct_rec A A A grp_homo_id grp_homo_id (tr (coeq w)))) =
h (FreeProduct_rec A A B f g (tr (coeq w)))
h (f a) = h (g a)
    apply p. }
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
{b : GroupHomomorphism A C &
(fun x : FreeProduct A A =>
 b (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))} ->
(fun x : A => h (f x)) == (fun x : A => h (g x))
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
(fun
   p : (fun x : A => h (f x)) ==
       (fun x : A => h (g x)) =>
 (grp_homo_compose h f;
 (fun x : FreeProduct A A =>
  p (FreeProduct_rec A A A grp_homo_id grp_homo_id x) @
  Trunc_ind
    (fun
       aa : Trunc 0
              (Coeq
                 (FreeProduct.map1 grp_trivial A A
                    (grp_trivial_rec A))
                 (FreeProduct.map2 grp_trivial A A
                    (grp_trivial_rec A))) =>
     h
       (g
          (FreeProduct_rec A A A grp_homo_id
             grp_homo_id aa)) =
     h (FreeProduct_rec A A B f g aa))
    (Coeq_ind
       (fun
          w : Coeq
                (FreeProduct.map1 grp_trivial A A
                   (grp_trivial_rec A))
                (FreeProduct.map2 grp_trivial A A
                   (grp_trivial_rec A)) =>
        h
          (g
             (FreeProduct_rec A A A grp_homo_id
                grp_homo_id (tr w))) =
        h (FreeProduct_rec A A B f g (tr w)))
       (fun w : FreeProduct.Words A A =>
        Core.list_rect (A + A)
          (fun w0 : Core.list (A + A) =>
           h
             (g
                (FreeProduct_rec A A A grp_homo_id
                   grp_homo_id (tr (...)))) =
           h
             (FreeProduct_rec A A B f g (tr (coeq w0))))
          (ap h (grp_homo_unit g))
          (fun (a : A + A) (w0 : Core.list (A + A))
             (IHw : h
                      (g
                         (FreeProduct_rec A A A
                            grp_homo_id grp_homo_id
                            (...))) =
                    h
                      (FreeProduct_rec A A B f g
                         (tr (...)))) =>
           match
             a as s return (h (...) = h (...))
           with
           | inl g0 =>
               (fun a0 : A =>
                ap h (...) @ (... @ ...^)) g0
           | inr g0 =>
               (fun a0 : A =>
                ap h (...) @ (... @ ...^)) g0
           end
           :
           h
             (g
                (FreeProduct_rec A A A grp_homo_id
                   grp_homo_id (tr ...))) =
           h
             (FreeProduct_rec A A B f g
                (tr (coeq ...)))) w
        :
        (fun
           w0 : Coeq
                  (FreeProduct.map1 grp_trivial A A
                     (grp_trivial_rec A))
                  (FreeProduct.map2 grp_trivial A A
                     (grp_trivial_rec A)) =>
         h
           (g
              (FreeProduct_rec A A A grp_homo_id
                 grp_homo_id (tr w0))) =
         h (FreeProduct_rec A A B f g (tr w0)))
          (coeq w))
       (fun
          b : FreeProduct.pc1 A A +
              FreeProduct.pc2 A A +
              FreeProduct.pc3 grp_trivial A A +
              FreeProduct.pc4 A A +
              FreeProduct.pc5 A A =>
        path_ishprop
          (transport
             (fun
                w : Coeq
                      (FreeProduct.map1 grp_trivial A
                         A (grp_trivial_rec A))
                      (FreeProduct.map2 grp_trivial A
                         A (grp_trivial_rec A)) =>
              h
                (g
                   (FreeProduct_rec A A A grp_homo_id
                      grp_homo_id (tr w))) =
              h (FreeProduct_rec A A B f g (tr w)))
             (cglue b)
             ((fun w : FreeProduct.Words A A =>
               Core.list_rect (A + A)
                 (fun w0 : ... => h ... = h ...)
                 (ap h (grp_homo_unit g))
                 (fun (a : ...) (w0 : ...) (IHw : ...)
                  => ...
                     ...
                     ...
                     end : ... = ...) w
               :
               (fun w0 : ... => h ... = h ...)
                 (coeq w))
                (FreeProduct.map1 grp_trivial A A
                   (grp_trivial_rec A) b)))
          ((fun w : FreeProduct.Words A A =>
            Core.list_rect (A + A)
              (fun w0 : Core.list (...) =>
               h (g ...) =
               h (FreeProduct_rec A A B f g ...))
              (ap h (grp_homo_unit g))
              (fun (a : A + A) (w0 : Core.list (...))
                 (IHw : h ... = h ...) =>
               match ... ... with
               | ... => ... g0
               | ... => ... g0
               end
               :
               h (...) = h (...)) w
            :
            (fun w0 : Coeq (...) (...) =>
             h (g ...) =
             h (FreeProduct_rec A A B f g ...))
              (coeq w))
             (FreeProduct.map2 grp_trivial A A
                (grp_trivial_rec A) b)))) x)
 :
 (fun x : FreeProduct A A =>
  grp_homo_compose h f
    (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
 (fun x : FreeProduct A A =>
  h (FreeProduct_rec A A B f g x)))) o ?g == idmap
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
?g
o (fun
     p : (fun x : A => h (f x)) ==
         (fun x : A => h (g x)) =>
   (grp_homo_compose h f;
   (fun x : FreeProduct A A =>
    p
      (FreeProduct_rec A A A grp_homo_id grp_homo_id x) @
    Trunc_ind
      (fun
         aa : Trunc 0
                (Coeq
                   (FreeProduct.map1 grp_trivial A A
                      (grp_trivial_rec A))
                   (FreeProduct.map2 grp_trivial A A
                      (grp_trivial_rec A))) =>
       h
         (g
            (FreeProduct_rec A A A grp_homo_id
               grp_homo_id aa)) =
       h (FreeProduct_rec A A B f g aa))
      (Coeq_ind
         (fun
            w : Coeq
                  (FreeProduct.map1 grp_trivial A A
                     (grp_trivial_rec A))
                  (FreeProduct.map2 grp_trivial A A
                     (grp_trivial_rec A)) =>
          h
            (g
               (FreeProduct_rec A A A grp_homo_id
                  grp_homo_id (tr w))) =
          h (FreeProduct_rec A A B f g (tr w)))
         (fun w : FreeProduct.Words A A =>
          Core.list_rect (A + A)
            (fun w0 : Core.list (A + A) =>
             h
               (g
                  (FreeProduct_rec A A A grp_homo_id
                     grp_homo_id (tr (...)))) =
             h
               (FreeProduct_rec A A B f g
                  (tr (coeq w0))))
            (ap h (grp_homo_unit g))
            (fun (a : A + A) (w0 : Core.list (A + A))
               (IHw : h
                        (g
                           (FreeProduct_rec A A A
                              grp_homo_id grp_homo_id
                              (...))) =
                      h
                        (FreeProduct_rec A A B f g
                           (tr (...)))) =>
             match
               a as s return (h (...) = h (...))
             with
             | inl g0 =>
                 (fun a0 : A =>
                  ap h (...) @ (... @ ...^)) g0
             | inr g0 =>
                 (fun a0 : A =>
                  ap h (...) @ (... @ ...^)) g0
             end
             :
             h
               (g
                  (FreeProduct_rec A A A grp_homo_id
                     grp_homo_id (tr ...))) =
             h
               (FreeProduct_rec A A B f g
                  (tr (coeq ...)))) w
          :
          (fun
             w0 : Coeq
                    (FreeProduct.map1 grp_trivial A A
                       (grp_trivial_rec A))
                    (FreeProduct.map2 grp_trivial A A
                       (grp_trivial_rec A)) =>
           h
             (g
                (FreeProduct_rec A A A grp_homo_id
                   grp_homo_id (tr w0))) =
           h (FreeProduct_rec A A B f g (tr w0)))
            (coeq w))
         (fun
            b : FreeProduct.pc1 A A +
                FreeProduct.pc2 A A +
                FreeProduct.pc3 grp_trivial A A +
                FreeProduct.pc4 A A +
                FreeProduct.pc5 A A =>
          path_ishprop
            (transport
               (fun
                  w : Coeq
                        (FreeProduct.map1 grp_trivial
                           A A (grp_trivial_rec A))
                        (FreeProduct.map2 grp_trivial
                           A A (grp_trivial_rec A)) =>
                h
                  (g
                     (FreeProduct_rec A A A
                        grp_homo_id grp_homo_id (tr w))) =
                h (FreeProduct_rec A A B f g (tr w)))
               (cglue b)
               ((fun w : FreeProduct.Words A A =>
                 Core.list_rect (A + A)
                   (fun w0 : ... => h ... = h ...)
                   (ap h (grp_homo_unit g))
                   (fun (a : ...) (w0 : ...)
                      (IHw : ...) =>
                    ...
                    ...
                    ...
                    end : ... = ...) w
                 :
                 (fun w0 : ... => h ... = h ...)
                   (coeq w))
                  (FreeProduct.map1 grp_trivial A A
                     (grp_trivial_rec A) b)))
            ((fun w : FreeProduct.Words A A =>
              Core.list_rect (A + A)
                (fun w0 : Core.list (...) =>
                 h (g ...) =
                 h (FreeProduct_rec A A B f g ...))
                (ap h (grp_homo_unit g))
                (fun (a : A + A)
                   (w0 : Core.list (...))
                   (IHw : h ... = h ...) =>
                 match ... ... with
                 | ... => ... g0
                 | ... => ... g0
                 end
                 :
                 h (...) = h (...)) w
              :
              (fun w0 : Coeq (...) (...) =>
               h (g ...) =
               h (FreeProduct_rec A A B f g ...))
                (coeq w))
               (FreeProduct.map2 grp_trivial A A
                  (grp_trivial_rec A) b)))) x)
   :
   (fun x : FreeProduct A A =>
    grp_homo_compose h f
      (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
   (fun x : FreeProduct A A =>
    h (FreeProduct_rec A A B f g x)))) == idmap
  {
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
{b : GroupHomomorphism A C &
(fun x : FreeProduct A A =>
 b (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))} ->
(fun x : A => h (f x)) == (fun x : A => h (g x)) intros [k p] x.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
x: A
h (f x) = h (g x)
    assert (q1 := p (freeproduct_inl x)).
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
x: A
q1: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) (freeproduct_inl x) =
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
  (freeproduct_inl x)
h (f x) = h (g x)
    assert (q2 := p (freeproduct_inr x)).
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
x: A
q1: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) (freeproduct_inl x) =
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
  (freeproduct_inl x)
q2: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) (freeproduct_inr x) =
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
  (freeproduct_inr x)
h (f x) = h (g x)
    simpl in q1, q2.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
x: A
q1: k (x * mon_unit) = h (f x * mon_unit)
q2: k (x * mon_unit) = h (g x * mon_unit)
h (f x) = h (g x)
    rewrite 2 right_identity in q1, q2.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
x: A
q1: k x = h (f x)
q2: k x = h (g x)
h (f x) = h (g x)
    refine (q1^ @ q2). }
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
(fun
   p : (fun x : A => h (f x)) ==
       (fun x : A => h (g x)) =>
 (grp_homo_compose h f;
 (fun x : FreeProduct A A =>
  p (FreeProduct_rec A A A grp_homo_id grp_homo_id x) @
  Trunc_ind
    (fun
       aa : Trunc 0
              (Coeq
                 (FreeProduct.map1 grp_trivial A A
                    (grp_trivial_rec A))
                 (FreeProduct.map2 grp_trivial A A
                    (grp_trivial_rec A))) =>
     h
       (g
          (FreeProduct_rec A A A grp_homo_id
             grp_homo_id aa)) =
     h (FreeProduct_rec A A B f g aa))
    (Coeq_ind
       (fun
          w : Coeq
                (FreeProduct.map1 grp_trivial A A
                   (grp_trivial_rec A))
                (FreeProduct.map2 grp_trivial A A
                   (grp_trivial_rec A)) =>
        h
          (g
             (FreeProduct_rec A A A grp_homo_id
                grp_homo_id (tr w))) =
        h (FreeProduct_rec A A B f g (tr w)))
       (fun w : FreeProduct.Words A A =>
        Core.list_rect (A + A)
          (fun w0 : Core.list (A + A) =>
           h
             (g
                (FreeProduct_rec A A A grp_homo_id
                   grp_homo_id (tr (...)))) =
           h
             (FreeProduct_rec A A B f g (tr (coeq w0))))
          (ap h (grp_homo_unit g))
          (fun (a : A + A) (w0 : Core.list (A + A))
             (IHw : h
                      (g
                         (FreeProduct_rec A A A
                            grp_homo_id grp_homo_id
                            (...))) =
                    h
                      (FreeProduct_rec A A B f g
                         (tr (...)))) =>
           match
             a as s return (h (...) = h (...))
           with
           | inl g0 =>
               (fun a0 : A =>
                ap h (...) @ (... @ ...^)) g0
           | inr g0 =>
               (fun a0 : A =>
                ap h (...) @ (... @ ...^)) g0
           end
           :
           h
             (g
                (FreeProduct_rec A A A grp_homo_id
                   grp_homo_id (tr ...))) =
           h
             (FreeProduct_rec A A B f g
                (tr (coeq ...)))) w
        :
        (fun
           w0 : Coeq
                  (FreeProduct.map1 grp_trivial A A
                     (grp_trivial_rec A))
                  (FreeProduct.map2 grp_trivial A A
                     (grp_trivial_rec A)) =>
         h
           (g
              (FreeProduct_rec A A A grp_homo_id
                 grp_homo_id (tr w0))) =
         h (FreeProduct_rec A A B f g (tr w0)))
          (coeq w))
       (fun
          b : FreeProduct.pc1 A A +
              FreeProduct.pc2 A A +
              FreeProduct.pc3 grp_trivial A A +
              FreeProduct.pc4 A A +
              FreeProduct.pc5 A A =>
        path_ishprop
          (transport
             (fun
                w : Coeq
                      (FreeProduct.map1 grp_trivial A
                         A (grp_trivial_rec A))
                      (FreeProduct.map2 grp_trivial A
                         A (grp_trivial_rec A)) =>
              h
                (g
                   (FreeProduct_rec A A A grp_homo_id
                      grp_homo_id (tr w))) =
              h (FreeProduct_rec A A B f g (tr w)))
             (cglue b)
             ((fun w : FreeProduct.Words A A =>
               Core.list_rect (A + A)
                 (fun w0 : ... => h ... = h ...)
                 (ap h (grp_homo_unit g))
                 (fun (a : ...) (w0 : ...) (IHw : ...)
                  => ...
                     ...
                     ...
                     end : ... = ...) w
               :
               (fun w0 : ... => h ... = h ...)
                 (coeq w))
                (FreeProduct.map1 grp_trivial A A
                   (grp_trivial_rec A) b)))
          ((fun w : FreeProduct.Words A A =>
            Core.list_rect (A + A)
              (fun w0 : Core.list (...) =>
               h (g ...) =
               h (FreeProduct_rec A A B f g ...))
              (ap h (grp_homo_unit g))
              (fun (a : A + A) (w0 : Core.list (...))
                 (IHw : h ... = h ...) =>
               match ... ... with
               | ... => ... g0
               | ... => ... g0
               end
               :
               h (...) = h (...)) w
            :
            (fun w0 : Coeq (...) (...) =>
             h (g ...) =
             h (FreeProduct_rec A A B f g ...))
              (coeq w))
             (FreeProduct.map2 grp_trivial A A
                (grp_trivial_rec A) b)))) x)
 :
 (fun x : FreeProduct A A =>
  grp_homo_compose h f
    (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
 (fun x : FreeProduct A A =>
  h (FreeProduct_rec A A B f g x))))
o (fun
     X : {b : GroupHomomorphism A C &
         (fun x : FreeProduct A A =>
          b
            (FreeProduct_rec A A A grp_homo_id
               grp_homo_id x)) ==
         (fun x : FreeProduct A A =>
          h (FreeProduct_rec A A B f g x))} =>
   (fun (k : GroupHomomorphism A C)
      (p : (fun x : FreeProduct A A =>
            k
              (FreeProduct_rec A A A grp_homo_id
                 grp_homo_id x)) ==
           (fun x : FreeProduct A A =>
            h (FreeProduct_rec A A B f g x))) =>
    (fun x : A =>
     let q1 := p (freeproduct_inl x) in
     let q2 := p (freeproduct_inr x) in
     let q3 :=
       internal_paths_rew
         (fun g : A => k g = h (f x * mon_unit)) q1
         (right_identity x) in
     let q4 :=
       internal_paths_rew
         (fun g0 : A => k g0 = h (g x * mon_unit)) q2
         (right_identity x) in
     let q5 :=
       internal_paths_rew (fun g : B => k x = h g) q3
         (right_identity (f x)) in
     let q6 :=
       internal_paths_rew (fun g : B => k x = h g) q4
         (right_identity (g x)) in
     q5^ @ q6)
    :
    (fun x : A => h (f x)) == (fun x : A => h (g x)))
     X.1 X.2) == idmap
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
(fun
   X : {b : GroupHomomorphism A C &
       (fun x : FreeProduct A A =>
        b
          (FreeProduct_rec A A A grp_homo_id
             grp_homo_id x)) ==
       (fun x : FreeProduct A A =>
        h (FreeProduct_rec A A B f g x))} =>
 (fun (k : GroupHomomorphism A C)
    (p : (fun x : FreeProduct A A =>
          k
            (FreeProduct_rec A A A grp_homo_id
               grp_homo_id x)) ==
         (fun x : FreeProduct A A =>
          h (FreeProduct_rec A A B f g x))) =>
  (fun x : A =>
   let q1 := p (freeproduct_inl x) in
   let q2 := p (freeproduct_inr x) in
   let q3 :=
     internal_paths_rew
       (fun g : A => k g = h (f x * mon_unit)) q1
       (right_identity x) in
   let q4 :=
     internal_paths_rew
       (fun g0 : A => k g0 = h (g x * mon_unit)) q2
       (right_identity x) in
   let q5 :=
     internal_paths_rew (fun g : B => k x = h g) q3
       (right_identity (f x)) in
   let q6 :=
     internal_paths_rew (fun g : B => k x = h g) q4
       (right_identity (g x)) in
   q5^ @ q6)
  :
  (fun x : A => h (f x)) == (fun x : A => h (g x)))
   X.1 X.2)
o (fun
     p : (fun x : A => h (f x)) ==
         (fun x : A => h (g x)) =>
   (grp_homo_compose h f;
   (fun x : FreeProduct A A =>
    p
      (FreeProduct_rec A A A grp_homo_id grp_homo_id x) @
    Trunc_ind
      (fun
         aa : Trunc 0
                (Coeq
                   (FreeProduct.map1 grp_trivial A A
                      (grp_trivial_rec A))
                   (FreeProduct.map2 grp_trivial A A
                      (grp_trivial_rec A))) =>
       h
         (g
            (FreeProduct_rec A A A grp_homo_id
               grp_homo_id aa)) =
       h (FreeProduct_rec A A B f g aa))
      (Coeq_ind
         (fun
            w : Coeq
                  (FreeProduct.map1 grp_trivial A A
                     (grp_trivial_rec A))
                  (FreeProduct.map2 grp_trivial A A
                     (grp_trivial_rec A)) =>
          h
            (g
               (FreeProduct_rec A A A grp_homo_id
                  grp_homo_id (tr w))) =
          h (FreeProduct_rec A A B f g (tr w)))
         (fun w : FreeProduct.Words A A =>
          Core.list_rect (A + A)
            (fun w0 : Core.list (A + A) =>
             h
               (g
                  (FreeProduct_rec A A A grp_homo_id
                     grp_homo_id (tr (...)))) =
             h
               (FreeProduct_rec A A B f g
                  (tr (coeq w0))))
            (ap h (grp_homo_unit g))
            (fun (a : A + A) (w0 : Core.list (A + A))
               (IHw : h
                        (g
                           (FreeProduct_rec A A A
                              grp_homo_id grp_homo_id
                              (...))) =
                      h
                        (FreeProduct_rec A A B f g
                           (tr (...)))) =>
             match
               a as s return (h (...) = h (...))
             with
             | inl g0 =>
                 (fun a0 : A =>
                  ap h (...) @ (... @ ...^)) g0
             | inr g0 =>
                 (fun a0 : A =>
                  ap h (...) @ (... @ ...^)) g0
             end
             :
             h
               (g
                  (FreeProduct_rec A A A grp_homo_id
                     grp_homo_id (tr ...))) =
             h
               (FreeProduct_rec A A B f g
                  (tr (coeq ...)))) w
          :
          (fun
             w0 : Coeq
                    (FreeProduct.map1 grp_trivial A A
                       (grp_trivial_rec A))
                    (FreeProduct.map2 grp_trivial A A
                       (grp_trivial_rec A)) =>
           h
             (g
                (FreeProduct_rec A A A grp_homo_id
                   grp_homo_id (tr w0))) =
           h (FreeProduct_rec A A B f g (tr w0)))
            (coeq w))
         (fun
            b : FreeProduct.pc1 A A +
                FreeProduct.pc2 A A +
                FreeProduct.pc3 grp_trivial A A +
                FreeProduct.pc4 A A +
                FreeProduct.pc5 A A =>
          path_ishprop
            (transport
               (fun
                  w : Coeq
                        (FreeProduct.map1 grp_trivial
                           A A (grp_trivial_rec A))
                        (FreeProduct.map2 grp_trivial
                           A A (grp_trivial_rec A)) =>
                h
                  (g
                     (FreeProduct_rec A A A
                        grp_homo_id grp_homo_id (tr w))) =
                h (FreeProduct_rec A A B f g (tr w)))
               (cglue b)
               ((fun w : FreeProduct.Words A A =>
                 Core.list_rect (A + A)
                   (fun w0 : ... => h ... = h ...)
                   (ap h (grp_homo_unit g))
                   (fun (a : ...) (w0 : ...)
                      (IHw : ...) =>
                    ...
                    ...
                    ...
                    end : ... = ...) w
                 :
                 (fun w0 : ... => h ... = h ...)
                   (coeq w))
                  (FreeProduct.map1 grp_trivial A A
                     (grp_trivial_rec A) b)))
            ((fun w : FreeProduct.Words A A =>
              Core.list_rect (A + A)
                (fun w0 : Core.list (...) =>
                 h (g ...) =
                 h (FreeProduct_rec A A B f g ...))
                (ap h (grp_homo_unit g))
                (fun (a : A + A)
                   (w0 : Core.list (...))
                   (IHw : h ... = h ...) =>
                 match ... ... with
                 | ... => ... g0
                 | ... => ... g0
                 end
                 :
                 h (...) = h (...)) w
              :
              (fun w0 : Coeq (...) (...) =>
               h (g ...) =
               h (FreeProduct_rec A A B f g ...))
                (coeq w))
               (FreeProduct.map2 grp_trivial A A
                  (grp_trivial_rec A) b)))) x)
   :
   (fun x : FreeProduct A A =>
    grp_homo_compose h f
      (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
   (fun x : FreeProduct A A =>
    h (FreeProduct_rec A A B f g x)))) == idmap
  {
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
(fun
   p : (fun x : A => h (f x)) ==
       (fun x : A => h (g x)) =>
 (grp_homo_compose h f;
 (fun x : FreeProduct A A =>
  p (FreeProduct_rec A A A grp_homo_id grp_homo_id x) @
  Trunc_ind
    (fun
       aa : Trunc 0
              (Coeq
                 (FreeProduct.map1 grp_trivial A A
                    (grp_trivial_rec A))
                 (FreeProduct.map2 grp_trivial A A
                    (grp_trivial_rec A))) =>
     h
       (g
          (FreeProduct_rec A A A grp_homo_id
             grp_homo_id aa)) =
     h (FreeProduct_rec A A B f g aa))
    (Coeq_ind
       (fun
          w : Coeq
                (FreeProduct.map1 grp_trivial A A
                   (grp_trivial_rec A))
                (FreeProduct.map2 grp_trivial A A
                   (grp_trivial_rec A)) =>
        h
          (g
             (FreeProduct_rec A A A grp_homo_id
                grp_homo_id (tr w))) =
        h (FreeProduct_rec A A B f g (tr w)))
       (fun w : FreeProduct.Words A A =>
        Core.list_rect (A + A)
          (fun w0 : Core.list (A + A) =>
           h
             (g
                (FreeProduct_rec A A A grp_homo_id
                   grp_homo_id (tr (...)))) =
           h
             (FreeProduct_rec A A B f g (tr (coeq w0))))
          (ap h (grp_homo_unit g))
          (fun (a : A + A) (w0 : Core.list (A + A))
             (IHw : h
                      (g
                         (FreeProduct_rec A A A
                            grp_homo_id grp_homo_id
                            (...))) =
                    h
                      (FreeProduct_rec A A B f g
                         (tr (...)))) =>
           match
             a as s return (h (...) = h (...))
           with
           | inl g0 =>
               (fun a0 : A =>
                ap h (...) @ (... @ ...^)) g0
           | inr g0 =>
               (fun a0 : A =>
                ap h (...) @ (... @ ...^)) g0
           end
           :
           h
             (g
                (FreeProduct_rec A A A grp_homo_id
                   grp_homo_id (tr ...))) =
           h
             (FreeProduct_rec A A B f g
                (tr (coeq ...)))) w
        :
        (fun
           w0 : Coeq
                  (FreeProduct.map1 grp_trivial A A
                     (grp_trivial_rec A))
                  (FreeProduct.map2 grp_trivial A A
                     (grp_trivial_rec A)) =>
         h
           (g
              (FreeProduct_rec A A A grp_homo_id
                 grp_homo_id (tr w0))) =
         h (FreeProduct_rec A A B f g (tr w0)))
          (coeq w))
       (fun
          b : FreeProduct.pc1 A A +
              FreeProduct.pc2 A A +
              FreeProduct.pc3 grp_trivial A A +
              FreeProduct.pc4 A A +
              FreeProduct.pc5 A A =>
        path_ishprop
          (transport
             (fun
                w : Coeq
                      (FreeProduct.map1 grp_trivial A
                         A (grp_trivial_rec A))
                      (FreeProduct.map2 grp_trivial A
                         A (grp_trivial_rec A)) =>
              h
                (g
                   (FreeProduct_rec A A A grp_homo_id
                      grp_homo_id (tr w))) =
              h (FreeProduct_rec A A B f g (tr w)))
             (cglue b)
             ((fun w : FreeProduct.Words A A =>
               Core.list_rect (A + A)
                 (fun w0 : ... => h ... = h ...)
                 (ap h (grp_homo_unit g))
                 (fun (a : ...) (w0 : ...) (IHw : ...)
                  => ...
                     ...
                     ...
                     end : ... = ...) w
               :
               (fun w0 : ... => h ... = h ...)
                 (coeq w))
                (FreeProduct.map1 grp_trivial A A
                   (grp_trivial_rec A) b)))
          ((fun w : FreeProduct.Words A A =>
            Core.list_rect (A + A)
              (fun w0 : Core.list (...) =>
               h (g ...) =
               h (FreeProduct_rec A A B f g ...))
              (ap h (grp_homo_unit g))
              (fun (a : A + A) (w0 : Core.list (...))
                 (IHw : h ... = h ...) =>
               match ... ... with
               | ... => ... g0
               | ... => ... g0
               end
               :
               h (...) = h (...)) w
            :
            (fun w0 : Coeq (...) (...) =>
             h (g ...) =
             h (FreeProduct_rec A A B f g ...))
              (coeq w))
             (FreeProduct.map2 grp_trivial A A
                (grp_trivial_rec A) b)))) x)
 :
 (fun x : FreeProduct A A =>
  grp_homo_compose h f
    (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
 (fun x : FreeProduct A A =>
  h (FreeProduct_rec A A B f g x))))
o (fun
     X : {b : GroupHomomorphism A C &
         (fun x : FreeProduct A A =>
          b
            (FreeProduct_rec A A A grp_homo_id
               grp_homo_id x)) ==
         (fun x : FreeProduct A A =>
          h (FreeProduct_rec A A B f g x))} =>
   (fun (k : GroupHomomorphism A C)
      (p : (fun x : FreeProduct A A =>
            k
              (FreeProduct_rec A A A grp_homo_id
                 grp_homo_id x)) ==
           (fun x : FreeProduct A A =>
            h (FreeProduct_rec A A B f g x))) =>
    (fun x : A =>
     let q1 := p (freeproduct_inl x) in
     let q2 := p (freeproduct_inr x) in
     let q3 :=
       internal_paths_rew
         (fun g : A => k g = h (f x * mon_unit)) q1
         (right_identity x) in
     let q4 :=
       internal_paths_rew
         (fun g0 : A => k g0 = h (g x * mon_unit)) q2
         (right_identity x) in
     let q5 :=
       internal_paths_rew (fun g : B => k x = h g) q3
         (right_identity (f x)) in
     let q6 :=
       internal_paths_rew (fun g : B => k x = h g) q4
         (right_identity (g x)) in
     q5^ @ q6)
    :
    (fun x : A => h (f x)) == (fun x : A => h (g x)))
     X.1 X.2) == idmap hnf.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
forall
x : {b : GroupHomomorphism A C &
    (fun x : FreeProduct A A =>
     b
       (FreeProduct_rec A A A grp_homo_id grp_homo_id
          x)) ==
    (fun x : FreeProduct A A =>
     h (FreeProduct_rec A A B f g x))},
(grp_homo_compose h f;
fun x0 : FreeProduct A A =>
(let q1 :=
   x.2
     (freeproduct_inl
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x0)) in
 let q2 :=
   x.2
     (freeproduct_inr
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x0)) in
 let q3 :=
   internal_paths_rew
     (fun g : A =>
      x.1 g =
      h
        (f
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x0) * mon_unit)) q1
     (right_identity
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x0)) in
 let q4 :=
   internal_paths_rew
     (fun g0 : A =>
      x.1 g0 =
      h
        (g
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x0) * mon_unit)) q2
     (right_identity
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x0)) in
 let q5 :=
   internal_paths_rew
     (fun g : B =>
      x.1
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x0) = h g) q3
     (right_identity
        (f
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x0))) in
 let q6 :=
   internal_paths_rew
     (fun g : B =>
      x.1
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x0) = h g) q4
     (right_identity
        (g
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x0))) in
 q5^ @ q6) @
Trunc_ind
  (fun
     aa : Trunc 0
            (Coeq
               (FreeProduct.map1 grp_trivial A A
                  (grp_trivial_rec A))
               (FreeProduct.map2 grp_trivial A A
                  (grp_trivial_rec A))) =>
   h
     (g
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           aa)) = h (FreeProduct_rec A A B f g aa))
  (Coeq_ind
     (fun
        w : Coeq
              (FreeProduct.map1 grp_trivial A A
                 (grp_trivial_rec A))
              (FreeProduct.map2 grp_trivial A A
                 (grp_trivial_rec A)) =>
      h
        (g
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id (tr w))) =
      h (FreeProduct_rec A A B f g (tr w)))
     (fun w : FreeProduct.Words A A =>
      Core.list_rect (A + A)
        (fun w0 : Core.list (A + A) =>
         h
           (g
              (FreeProduct_rec A A A grp_homo_id
                 grp_homo_id (tr (coeq w0)))) =
         h (FreeProduct_rec A A B f g (tr (coeq w0))))
        (ap h (grp_homo_unit g))
        (fun (a : A + A) (w0 : Core.list (A + A))
           (IHw : h
                    (g
                       (FreeProduct_rec A A A
                          grp_homo_id grp_homo_id
                          (tr (coeq w0)))) =
                  h
                    (FreeProduct_rec A A B f g
                       (tr (coeq w0)))) =>
         match
           a as s
           return
             (h
                (g
                   (match ... with
                    | ... | ... => ... => ...
                    end
                      (Core.fold_right (...) mon_unit
                         w0))) =
              h
                (match s with
                 | inl g => fun x1 : B => f g * x1
                 | inr g0 => fun x1 : B => g g0 * x1
                 end
                   (Core.fold_right
                      (fun ... => ...
                                  ...
                                  ...
                                  end) mon_unit w0)))
         with
         | inl g0 =>
             ap h
               (grp_homo_op g g0
                  (Core.fold_right
                     (fun X0 : A + A =>
                      match X0 with
                      | inl g | inr g =>
                          fun ... => g * x1
                      end) mon_unit w0)) @
             ((grp_homo_op h (g g0)
                 (g
                    (Core.fold_right (... => ...)
                       mon_unit w0)) @
               ap11
                 (ap11 1
                    (let q1 := x.2 ... in
                     let q2 := ... in ... ...)^) IHw) @
              (grp_homo_op h (f g0)
                 (Core.fold_right
                    (fun X0 : A + A =>
                     match ... with
                     | ... => ... => ...
                     | ... => ... => ...
                     end) mon_unit w0))^)
         | inr g0 =>
             ap h
               (grp_homo_op g g0
                  (Core.fold_right
                     (fun X0 : A + A =>
                      match X0 with
                      | inl g | inr g =>
                          fun ... => g * x1
                      end) mon_unit w0)) @
             ((grp_homo_op h (g g0)
                 (g
                    (Core.fold_right (... => ...)
                       mon_unit w0)) @ ap11 1 IHw) @
              (grp_homo_op h (g g0)
                 (Core.fold_right
                    (fun X0 : A + A =>
                     match ... with
                     | ... => ... => ...
                     | ... => ... => ...
                     end) mon_unit w0))^)
         end) w)
     (fun
        b : FreeProduct.pc1 A A + FreeProduct.pc2 A A +
            FreeProduct.pc3 grp_trivial A A +
            FreeProduct.pc4 A A + FreeProduct.pc5 A A
      =>
      path_ishprop
        (transport
           (fun
              w : Coeq
                    (FreeProduct.map1 grp_trivial A A
                       (grp_trivial_rec A))
                    (FreeProduct.map2 grp_trivial A A
                       (grp_trivial_rec A)) =>
            h
              (g
                 (FreeProduct_rec A A A grp_homo_id
                    grp_homo_id (tr w))) =
            h (FreeProduct_rec A A B f g (tr w)))
           (cglue b)
           (Core.list_rect (A + A)
              (fun w : Core.list (A + A) =>
               h
                 (g
                    (FreeProduct_rec A A A grp_homo_id
                       grp_homo_id (tr (coeq w)))) =
               h
                 (FreeProduct_rec A A B f g
                    (tr (coeq w))))
              (ap h (grp_homo_unit g))
              (fun (a : A + A) (w : Core.list (A + A))
                 (IHw : h
                          (g
                             (FreeProduct_rec A A A
                                grp_homo_id
                                grp_homo_id (tr ...))) =
                        h
                          (FreeProduct_rec A A B f g
                             (tr (coeq w)))) =>
               match
                 a as s
                 return
                   (h (g (...)) =
                    h (...
                       ...
                       ...
                       end (...)))
               with
               | inl g0 =>
                   ap h
                     (grp_homo_op g g0
                        (Core.fold_right (... => ...)
                           mon_unit w)) @
                   ((grp_homo_op h (g g0) (g ...) @
                     ap11 (ap11 1 ...^) IHw) @
                    (grp_homo_op h (f g0)
                       (Core.fold_right (...) mon_unit
                          w))^)
               | inr g0 =>
                   ap h
                     (grp_homo_op g g0
                        (Core.fold_right (... => ...)
                           mon_unit w)) @
                   ((grp_homo_op h (g g0) (g ...) @
                     ap11 1 IHw) @
                    (grp_homo_op h (g g0)
                       (Core.fold_right (...) mon_unit
                          w))^)
               end)
              (FreeProduct.map1 grp_trivial A A
                 (grp_trivial_rec A) b)))
        (Core.list_rect (A + A)
           (fun w : Core.list (A + A) =>
            h
              (g
                 (FreeProduct_rec A A A grp_homo_id
                    grp_homo_id (tr (coeq w)))) =
            h
              (FreeProduct_rec A A B f g (tr (coeq w))))
           (ap h (grp_homo_unit g))
           (fun (a : A + A) (w : Core.list (A + A))
              (IHw : h
                       (g
                          (FreeProduct_rec A A A
                             grp_homo_id grp_homo_id
                             (tr (coeq w)))) =
                     h
                       (FreeProduct_rec A A B f g
                          (tr (coeq w)))) =>
            match
              a as s
              return
                (h (g (...
                       ...
                       end (...))) =
                 h
                   (match ... with
                    | ... => ... => ...
                    | ... => ... => ...
                    end
                      (Core.fold_right (...) mon_unit
                         w)))
            with
            | inl g0 =>
                ap h
                  (grp_homo_op g g0
                     (Core.fold_right
                        (fun X0 : ... =>
                         match ... with
                         | ... ...
                         end) mon_unit w)) @
                ((grp_homo_op h (g g0)
                    (g
                       (Core.fold_right ... mon_unit w)) @
                  ap11 (ap11 1 (... ...)^) IHw) @
                 (grp_homo_op h (f g0)
                    (Core.fold_right
                       (fun ... => ...
                                   ...
                                   ...
                                   end) mon_unit w))^)
            | inr g0 =>
                ap h
                  (grp_homo_op g g0
                     (Core.fold_right
                        (fun X0 : ... =>
                         match ... with
                         | ... ...
                         end) mon_unit w)) @
                ((grp_homo_op h (g g0)
                    (g
                       (Core.fold_right ... mon_unit w)) @
                  ap11 1 IHw) @
                 (grp_homo_op h (g g0)
                    (Core.fold_right
                       (fun ... => ...
                                   ...
                                   ...
                                   end) mon_unit w))^)
            end)
           (FreeProduct.map2 grp_trivial A A
              (grp_trivial_rec A) b)))) x0) = x intros [k p].
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
(grp_homo_compose h f;
fun x : FreeProduct A A =>
(let q1 :=
   p
     (freeproduct_inl
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x)) in
 let q2 :=
   p
     (freeproduct_inr
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x)) in
 let q3 :=
   internal_paths_rew
     (fun g : A =>
      k g =
      h
        (f
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x) * mon_unit)) q1
     (right_identity
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x)) in
 let q4 :=
   internal_paths_rew
     (fun g0 : A =>
      k g0 =
      h
        (g
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x) * mon_unit)) q2
     (right_identity
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x)) in
 let q5 :=
   internal_paths_rew
     (fun g : B =>
      k
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x) = h g) q3
     (right_identity
        (f
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x))) in
 let q6 :=
   internal_paths_rew
     (fun g : B =>
      k
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x) = h g) q4
     (right_identity
        (g
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x))) in
 q5^ @ q6) @
Trunc_ind
  (fun
     aa : Trunc 0
            (Coeq
               (FreeProduct.map1 grp_trivial A A
                  (grp_trivial_rec A))
               (FreeProduct.map2 grp_trivial A A
                  (grp_trivial_rec A))) =>
   h
     (g
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           aa)) = h (FreeProduct_rec A A B f g aa))
  (Coeq_ind
     (fun
        w : Coeq
              (FreeProduct.map1 grp_trivial A A
                 (grp_trivial_rec A))
              (FreeProduct.map2 grp_trivial A A
                 (grp_trivial_rec A)) =>
      h
        (g
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id (tr w))) =
      h (FreeProduct_rec A A B f g (tr w)))
     (fun w : FreeProduct.Words A A =>
      Core.list_rect (A + A)
        (fun w0 : Core.list (A + A) =>
         h
           (g
              (FreeProduct_rec A A A grp_homo_id
                 grp_homo_id (tr (coeq w0)))) =
         h (FreeProduct_rec A A B f g (tr (coeq w0))))
        (ap h (grp_homo_unit g))
        (fun (a : A + A) (w0 : Core.list (A + A))
           (IHw : h
                    (g
                       (FreeProduct_rec A A A
                          grp_homo_id grp_homo_id
                          (tr (coeq w0)))) =
                  h
                    (FreeProduct_rec A A B f g
                       (tr (coeq w0)))) =>
         match
           a as s
           return
             (h
                (g
                   (match s with
                    | inl g | inr g =>
                        fun ... => g * x0
                    end
                      (Core.fold_right (... => ...)
                         mon_unit w0))) =
              h
                (match s with
                 | inl g => fun x0 : B => f g * x0
                 | inr g0 => fun x0 : B => g g0 * x0
                 end
                   (Core.fold_right
                      (fun X0 : ... =>
                       match ... with
                       | ... ...
                       | ... ...
                       end) mon_unit w0)))
         with
         | inl g0 =>
             ap h
               (grp_homo_op g g0
                  (Core.fold_right
                     (fun X0 : A + A =>
                      match X0 with
                      | inl g | inr g =>
                          fun x0 : A => g * x0
                      end) mon_unit w0)) @
             ((grp_homo_op h (g g0)
                 (g
                    (Core.fold_right
                       (fun ... => ...
                                   ...
                                   end) mon_unit w0)) @
               ap11
                 (ap11 1
                    (let q1 := p (...) in
                     let q2 := p ... in
                     let q3 := ... in ... ...)^) IHw) @
              (grp_homo_op h (f g0)
                 (Core.fold_right
                    (fun X0 : A + A =>
                     match X0 with
                     | inl g => fun ... => ... * x0
                     | inr g1 => fun ... => ... * x0
                     end) mon_unit w0))^)
         | inr g0 =>
             ap h
               (grp_homo_op g g0
                  (Core.fold_right
                     (fun X0 : A + A =>
                      match X0 with
                      | inl g | inr g =>
                          fun x0 : A => g * x0
                      end) mon_unit w0)) @
             ((grp_homo_op h (g g0)
                 (g
                    (Core.fold_right
                       (fun ... => ...
                                   ...
                                   end) mon_unit w0)) @
               ap11 1 IHw) @
              (grp_homo_op h (g g0)
                 (Core.fold_right
                    (fun X0 : A + A =>
                     match X0 with
                     | inl g => fun ... => ... * x0
                     | inr g1 => fun ... => ... * x0
                     end) mon_unit w0))^)
         end) w)
     (fun
        b : FreeProduct.pc1 A A + FreeProduct.pc2 A A +
            FreeProduct.pc3 grp_trivial A A +
            FreeProduct.pc4 A A + FreeProduct.pc5 A A
      =>
      path_ishprop
        (transport
           (fun
              w : Coeq
                    (FreeProduct.map1 grp_trivial A A
                       (grp_trivial_rec A))
                    (FreeProduct.map2 grp_trivial A A
                       (grp_trivial_rec A)) =>
            h
              (g
                 (FreeProduct_rec A A A grp_homo_id
                    grp_homo_id (tr w))) =
            h (FreeProduct_rec A A B f g (tr w)))
           (cglue b)
           (Core.list_rect (A + A)
              (fun w : Core.list (A + A) =>
               h
                 (g
                    (FreeProduct_rec A A A grp_homo_id
                       grp_homo_id (tr (coeq w)))) =
               h
                 (FreeProduct_rec A A B f g
                    (tr (coeq w))))
              (ap h (grp_homo_unit g))
              (fun (a : A + A) (w : Core.list (A + A))
                 (IHw : h
                          (g
                             (FreeProduct_rec A A A
                                grp_homo_id
                                grp_homo_id (tr (...)))) =
                        h
                          (FreeProduct_rec A A B f g
                             (tr (coeq w)))) =>
               match
                 a as s
                 return
                   (h (g (... ...)) =
                    h
                      (match ... with
                       | ... ...
                       | ... ...
                       end
                         (Core.fold_right ... mon_unit
                            w)))
               with
               | inl g0 =>
                   ap h
                     (grp_homo_op g g0
                        (Core.fold_right
                           (fun ... => ...
                                       ...
                                       end) mon_unit w)) @
                   ((grp_homo_op h (g g0) (g (...)) @
                     ap11 (ap11 1 (...)^) IHw) @
                    (grp_homo_op h (f g0)
                       (Core.fold_right (... => ...)
                          mon_unit w))^)
               | inr g0 =>
                   ap h
                     (grp_homo_op g g0
                        (Core.fold_right
                           (fun ... => ...
                                       ...
                                       end) mon_unit w)) @
                   ((grp_homo_op h (g g0) (g (...)) @
                     ap11 1 IHw) @
                    (grp_homo_op h (g g0)
                       (Core.fold_right (... => ...)
                          mon_unit w))^)
               end)
              (FreeProduct.map1 grp_trivial A A
                 (grp_trivial_rec A) b)))
        (Core.list_rect (A + A)
           (fun w : Core.list (A + A) =>
            h
              (g
                 (FreeProduct_rec A A A grp_homo_id
                    grp_homo_id (tr (coeq w)))) =
            h
              (FreeProduct_rec A A B f g (tr (coeq w))))
           (ap h (grp_homo_unit g))
           (fun (a : A + A) (w : Core.list (A + A))
              (IHw : h
                       (g
                          (FreeProduct_rec A A A
                             grp_homo_id grp_homo_id
                             (tr (coeq w)))) =
                     h
                       (FreeProduct_rec A A B f g
                          (tr (coeq w)))) =>
            match
              a as s
              return
                (h
                   (g
                      (match ... with
                       | ... ...
                       end
                         (Core.fold_right ... mon_unit
                            w))) =
                 h
                   (match s with
                    | inl g => fun ... => ... * x0
                    | inr g0 => fun ... => ... * x0
                    end
                      (Core.fold_right (... => ...)
                         mon_unit w)))
            with
            | inl g0 =>
                ap h
                  (grp_homo_op g g0
                     (Core.fold_right
                        (fun X0 : A + A =>
                         match ... with
                         | ... | ... => ... => ...
                         end) mon_unit w)) @
                ((grp_homo_op h (g g0)
                    (g
                       (Core.fold_right (...) mon_unit
                          w)) @
                  ap11
                    (ap11 1
                       (let q1 := ... in ... ...)^)
                    IHw) @
                 (grp_homo_op h (f g0)
                    (Core.fold_right
                       (fun X0 : ... =>
                        match ... with
                        | ... ...
                        | ... ...
                        end) mon_unit w))^)
            | inr g0 =>
                ap h
                  (grp_homo_op g g0
                     (Core.fold_right
                        (fun X0 : A + A =>
                         match ... with
                         | ... | ... => ... => ...
                         end) mon_unit w)) @
                ((grp_homo_op h (g g0)
                    (g
                       (Core.fold_right (...) mon_unit
                          w)) @ ap11 1 IHw) @
                 (grp_homo_op h (g g0)
                    (Core.fold_right
                       (fun X0 : ... =>
                        match ... with
                        | ... ...
                        | ... ...
                        end) mon_unit w))^)
            end)
           (FreeProduct.map2 grp_trivial A A
              (grp_trivial_rec A) b)))) x) = (k; p)
    apply path_sigma_hprop.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
(grp_homo_compose h f;
fun x : FreeProduct A A =>
(let q1 :=
   p
     (freeproduct_inl
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x)) in
 let q2 :=
   p
     (freeproduct_inr
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x)) in
 let q3 :=
   internal_paths_rew
     (fun g : A =>
      k g =
      h
        (f
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x) * mon_unit)) q1
     (right_identity
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x)) in
 let q4 :=
   internal_paths_rew
     (fun g0 : A =>
      k g0 =
      h
        (g
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x) * mon_unit)) q2
     (right_identity
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x)) in
 let q5 :=
   internal_paths_rew
     (fun g : B =>
      k
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x) = h g) q3
     (right_identity
        (f
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x))) in
 let q6 :=
   internal_paths_rew
     (fun g : B =>
      k
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           x) = h g) q4
     (right_identity
        (g
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id x))) in
 q5^ @ q6) @
Trunc_ind
  (fun
     aa : Trunc 0
            (Coeq
               (FreeProduct.map1 grp_trivial A A
                  (grp_trivial_rec A))
               (FreeProduct.map2 grp_trivial A A
                  (grp_trivial_rec A))) =>
   h
     (g
        (FreeProduct_rec A A A grp_homo_id grp_homo_id
           aa)) = h (FreeProduct_rec A A B f g aa))
  (Coeq_ind
     (fun
        w : Coeq
              (FreeProduct.map1 grp_trivial A A
                 (grp_trivial_rec A))
              (FreeProduct.map2 grp_trivial A A
                 (grp_trivial_rec A)) =>
      h
        (g
           (FreeProduct_rec A A A grp_homo_id
              grp_homo_id (tr w))) =
      h (FreeProduct_rec A A B f g (tr w)))
     (fun w : FreeProduct.Words A A =>
      Core.list_rect (A + A)
        (fun w0 : Core.list (A + A) =>
         h
           (g
              (FreeProduct_rec A A A grp_homo_id
                 grp_homo_id (tr (coeq w0)))) =
         h (FreeProduct_rec A A B f g (tr (coeq w0))))
        (ap h (grp_homo_unit g))
        (fun (a : A + A) (w0 : Core.list (A + A))
           (IHw : h
                    (g
                       (FreeProduct_rec A A A
                          grp_homo_id grp_homo_id
                          (tr (coeq w0)))) =
                  h
                    (FreeProduct_rec A A B f g
                       (tr (coeq w0)))) =>
         match
           a as s
           return
             (h
                (g
                   (match s with
                    | inl g | inr g =>
                        fun ... => g * x0
                    end
                      (Core.fold_right (... => ...)
                         mon_unit w0))) =
              h
                (match s with
                 | inl g => fun x0 : B => f g * x0
                 | inr g0 => fun x0 : B => g g0 * x0
                 end
                   (Core.fold_right
                      (fun X0 : ... =>
                       match ... with
                       | ... ...
                       | ... ...
                       end) mon_unit w0)))
         with
         | inl g0 =>
             ap h
               (grp_homo_op g g0
                  (Core.fold_right
                     (fun X0 : A + A =>
                      match X0 with
                      | inl g | inr g =>
                          fun x0 : A => g * x0
                      end) mon_unit w0)) @
             ((grp_homo_op h (g g0)
                 (g
                    (Core.fold_right
                       (fun ... => ...
                                   ...
                                   end) mon_unit w0)) @
               ap11
                 (ap11 1
                    (let q1 := p (...) in
                     let q2 := p ... in
                     let q3 := ... in ... ...)^) IHw) @
              (grp_homo_op h (f g0)
                 (Core.fold_right
                    (fun X0 : A + A =>
                     match X0 with
                     | inl g => fun ... => ... * x0
                     | inr g1 => fun ... => ... * x0
                     end) mon_unit w0))^)
         | inr g0 =>
             ap h
               (grp_homo_op g g0
                  (Core.fold_right
                     (fun X0 : A + A =>
                      match X0 with
                      | inl g | inr g =>
                          fun x0 : A => g * x0
                      end) mon_unit w0)) @
             ((grp_homo_op h (g g0)
                 (g
                    (Core.fold_right
                       (fun ... => ...
                                   ...
                                   end) mon_unit w0)) @
               ap11 1 IHw) @
              (grp_homo_op h (g g0)
                 (Core.fold_right
                    (fun X0 : A + A =>
                     match X0 with
                     | inl g => fun ... => ... * x0
                     | inr g1 => fun ... => ... * x0
                     end) mon_unit w0))^)
         end) w)
     (fun
        b : FreeProduct.pc1 A A + FreeProduct.pc2 A A +
            FreeProduct.pc3 grp_trivial A A +
            FreeProduct.pc4 A A + FreeProduct.pc5 A A
      =>
      path_ishprop
        (transport
           (fun
              w : Coeq
                    (FreeProduct.map1 grp_trivial A A
                       (grp_trivial_rec A))
                    (FreeProduct.map2 grp_trivial A A
                       (grp_trivial_rec A)) =>
            h
              (g
                 (FreeProduct_rec A A A grp_homo_id
                    grp_homo_id (tr w))) =
            h (FreeProduct_rec A A B f g (tr w)))
           (cglue b)
           (Core.list_rect (A + A)
              (fun w : Core.list (A + A) =>
               h
                 (g
                    (FreeProduct_rec A A A grp_homo_id
                       grp_homo_id (tr (coeq w)))) =
               h
                 (FreeProduct_rec A A B f g
                    (tr (coeq w))))
              (ap h (grp_homo_unit g))
              (fun (a : A + A) (w : Core.list (A + A))
                 (IHw : h
                          (g
                             (FreeProduct_rec A A A
                                grp_homo_id
                                grp_homo_id (tr (...)))) =
                        h
                          (FreeProduct_rec A A B f g
                             (tr (coeq w)))) =>
               match
                 a as s
                 return
                   (h (g (... ...)) =
                    h
                      (match ... with
                       | ... ...
                       | ... ...
                       end
                         (Core.fold_right ... mon_unit
                            w)))
               with
               | inl g0 =>
                   ap h
                     (grp_homo_op g g0
                        (Core.fold_right
                           (fun ... => ...
                                       ...
                                       end) mon_unit w)) @
                   ((grp_homo_op h (g g0) (g (...)) @
                     ap11 (ap11 1 (...)^) IHw) @
                    (grp_homo_op h (f g0)
                       (Core.fold_right (... => ...)
                          mon_unit w))^)
               | inr g0 =>
                   ap h
                     (grp_homo_op g g0
                        (Core.fold_right
                           (fun ... => ...
                                       ...
                                       end) mon_unit w)) @
                   ((grp_homo_op h (g g0) (g (...)) @
                     ap11 1 IHw) @
                    (grp_homo_op h (g g0)
                       (Core.fold_right (... => ...)
                          mon_unit w))^)
               end)
              (FreeProduct.map1 grp_trivial A A
                 (grp_trivial_rec A) b)))
        (Core.list_rect (A + A)
           (fun w : Core.list (A + A) =>
            h
              (g
                 (FreeProduct_rec A A A grp_homo_id
                    grp_homo_id (tr (coeq w)))) =
            h
              (FreeProduct_rec A A B f g (tr (coeq w))))
           (ap h (grp_homo_unit g))
           (fun (a : A + A) (w : Core.list (A + A))
              (IHw : h
                       (g
                          (FreeProduct_rec A A A
                             grp_homo_id grp_homo_id
                             (tr (coeq w)))) =
                     h
                       (FreeProduct_rec A A B f g
                          (tr (coeq w)))) =>
            match
              a as s
              return
                (h
                   (g
                      (match ... with
                       | ... ...
                       end
                         (Core.fold_right ... mon_unit
                            w))) =
                 h
                   (match s with
                    | inl g => fun ... => ... * x0
                    | inr g0 => fun ... => ... * x0
                    end
                      (Core.fold_right (... => ...)
                         mon_unit w)))
            with
            | inl g0 =>
                ap h
                  (grp_homo_op g g0
                     (Core.fold_right
                        (fun X0 : A + A =>
                         match ... with
                         | ... | ... => ... => ...
                         end) mon_unit w)) @
                ((grp_homo_op h (g g0)
                    (g
                       (Core.fold_right (...) mon_unit
                          w)) @
                  ap11
                    (ap11 1
                       (let q1 := ... in ... ...)^)
                    IHw) @
                 (grp_homo_op h (f g0)
                    (Core.fold_right
                       (fun X0 : ... =>
                        match ... with
                        | ... ...
                        | ... ...
                        end) mon_unit w))^)
            | inr g0 =>
                ap h
                  (grp_homo_op g g0
                     (Core.fold_right
                        (fun X0 : A + A =>
                         match ... with
                         | ... | ... => ... => ...
                         end) mon_unit w)) @
                ((grp_homo_op h (g g0)
                    (g
                       (Core.fold_right (...) mon_unit
                          w)) @ ap11 1 IHw) @
                 (grp_homo_op h (g g0)
                    (Core.fold_right
                       (fun X0 : ... =>
                        match ... with
                        | ... ...
                        | ... ...
                        end) mon_unit w))^)
            end)
           (FreeProduct.map2 grp_trivial A A
              (grp_trivial_rec A) b)))) x).1 =
(k; p).1
    simpl.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
grp_homo_compose h f = k
    apply equiv_path_grouphomomorphism.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
grp_homo_compose h f == k
    intro y.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
y: A
grp_homo_compose h f y = k y
    pose (q1 := p (freeproduct_inl y)).
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
y: A
q1:= p (freeproduct_inl y): (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) (freeproduct_inl y) =
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
  (freeproduct_inl y)
grp_homo_compose h f y = k y
    simpl in q1.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
y: A
q1:= p (amal_eta (Core.cons (inl y) Core.nil)): k (y * mon_unit) = h (f y * mon_unit)
grp_homo_compose h f y = k y
    rewrite 2 right_identity in q1.
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
k: GroupHomomorphism A C
p: (fun x : FreeProduct A A =>
 k
   (FreeProduct_rec A A A grp_homo_id grp_homo_id
      x)) ==
(fun x : FreeProduct A A =>
 h (FreeProduct_rec A A B f g x))
y: A
q1: k y = h (f y)
grp_homo_compose h f y = k y
    exact q1^. }
H: Funext
A, B, C: Group
f, g: GroupHomomorphism A B
h: B $-> C
(fun
   X : {b : GroupHomomorphism A C &
       (fun x : FreeProduct A A =>
        b
          (FreeProduct_rec A A A grp_homo_id
             grp_homo_id x)) ==
       (fun x : FreeProduct A A =>
        h (FreeProduct_rec A A B f g x))} =>
 (fun (k : GroupHomomorphism A C)
    (p : (fun x : FreeProduct A A =>
          k
            (FreeProduct_rec A A A grp_homo_id
               grp_homo_id x)) ==
         (fun x : FreeProduct A A =>
          h (FreeProduct_rec A A B f g x))) =>
  (fun x : A =>
   let q1 := p (freeproduct_inl x) in
   let q2 := p (freeproduct_inr x) in
   let q3 :=
     internal_paths_rew
       (fun g : A => k g = h (f x * mon_unit)) q1
       (right_identity x) in
   let q4 :=
     internal_paths_rew
       (fun g0 : A => k g0 = h (g x * mon_unit)) q2
       (right_identity x) in
   let q5 :=
     internal_paths_rew (fun g : B => k x = h g) q3
       (right_identity (f x)) in
   let q6 :=
     internal_paths_rew (fun g : B => k x = h g) q4
       (right_identity (g x)) in
   q5^ @ q6)
  :
  (fun x : A => h (f x)) == (fun x : A => h (g x)))
   X.1 X.2)
o (fun
     p : (fun x : A => h (f x)) ==
         (fun x : A => h (g x)) =>
   (grp_homo_compose h f;
   (fun x : FreeProduct A A =>
    p
      (FreeProduct_rec A A A grp_homo_id grp_homo_id x) @
    Trunc_ind
      (fun
         aa : Trunc 0
                (Coeq
                   (FreeProduct.map1 grp_trivial A A
                      (grp_trivial_rec A))
                   (FreeProduct.map2 grp_trivial A A
                      (grp_trivial_rec A))) =>
       h
         (g
            (FreeProduct_rec A A A grp_homo_id
               grp_homo_id aa)) =
       h (FreeProduct_rec A A B f g aa))
      (Coeq_ind
         (fun
            w : Coeq
                  (FreeProduct.map1 grp_trivial A A
                     (grp_trivial_rec A))
                  (FreeProduct.map2 grp_trivial A A
                     (grp_trivial_rec A)) =>
          h
            (g
               (FreeProduct_rec A A A grp_homo_id
                  grp_homo_id (tr w))) =
          h (FreeProduct_rec A A B f g (tr w)))
         (fun w : FreeProduct.Words A A =>
          Core.list_rect (A + A)
            (fun w0 : Core.list (A + A) =>
             h
               (g
                  (FreeProduct_rec A A A grp_homo_id
                     grp_homo_id (tr (...)))) =
             h
               (FreeProduct_rec A A B f g
                  (tr (coeq w0))))
            (ap h (grp_homo_unit g))
            (fun (a : A + A) (w0 : Core.list (A + A))
               (IHw : h
                        (g
                           (FreeProduct_rec A A A
                              grp_homo_id grp_homo_id
                              (...))) =
                      h
                        (FreeProduct_rec A A B f g
                           (tr (...)))) =>
             match
               a as s return (h (...) = h (...))
             with
             | inl g0 =>
                 (fun a0 : A =>
                  ap h (...) @ (... @ ...^)) g0
             | inr g0 =>
                 (fun a0 : A =>
                  ap h (...) @ (... @ ...^)) g0
             end
             :
             h
               (g
                  (FreeProduct_rec A A A grp_homo_id
                     grp_homo_id (tr ...))) =
             h
               (FreeProduct_rec A A B f g
                  (tr (coeq ...)))) w
          :
          (fun
             w0 : Coeq
                    (FreeProduct.map1 grp_trivial A A
                       (grp_trivial_rec A))
                    (FreeProduct.map2 grp_trivial A A
                       (grp_trivial_rec A)) =>
           h
             (g
                (FreeProduct_rec A A A grp_homo_id
                   grp_homo_id (tr w0))) =
           h (FreeProduct_rec A A B f g (tr w0)))
            (coeq w))
         (fun
            b : FreeProduct.pc1 A A +
                FreeProduct.pc2 A A +
                FreeProduct.pc3 grp_trivial A A +
                FreeProduct.pc4 A A +
                FreeProduct.pc5 A A =>
          path_ishprop
            (transport
               (fun
                  w : Coeq
                        (FreeProduct.map1 grp_trivial
                           A A (grp_trivial_rec A))
                        (FreeProduct.map2 grp_trivial
                           A A (grp_trivial_rec A)) =>
                h
                  (g
                     (FreeProduct_rec A A A
                        grp_homo_id grp_homo_id (tr w))) =
                h (FreeProduct_rec A A B f g (tr w)))
               (cglue b)
               ((fun w : FreeProduct.Words A A =>
                 Core.list_rect (A + A)
                   (fun w0 : ... => h ... = h ...)
                   (ap h (grp_homo_unit g))
                   (fun (a : ...) (w0 : ...)
                      (IHw : ...) =>
                    ...
                    ...
                    ...
                    end : ... = ...) w
                 :
                 (fun w0 : ... => h ... = h ...)
                   (coeq w))
                  (FreeProduct.map1 grp_trivial A A
                     (grp_trivial_rec A) b)))
            ((fun w : FreeProduct.Words A A =>
              Core.list_rect (A + A)
                (fun w0 : Core.list (...) =>
                 h (g ...) =
                 h (FreeProduct_rec A A B f g ...))
                (ap h (grp_homo_unit g))
                (fun (a : A + A)
                   (w0 : Core.list (...))
                   (IHw : h ... = h ...) =>
                 match ... ... with
                 | ... => ... g0
                 | ... => ... g0
                 end
                 :
                 h (...) = h (...)) w
              :
              (fun w0 : Coeq (...) (...) =>
               h (g ...) =
               h (FreeProduct_rec A A B f g ...))
                (coeq w))
               (FreeProduct.map2 grp_trivial A A
                  (grp_trivial_rec A) b)))) x)
   :
   (fun x : FreeProduct A A =>
    grp_homo_compose h f
      (FreeProduct_rec A A A grp_homo_id grp_homo_id x)) ==
   (fun x : FreeProduct A A =>
    h (FreeProduct_rec A A B f g x)))) == idmap
  hnf; intros; apply path_ishprop.
Defined.