Require Import Basics Types Limits.Pullback Cubical.PathSquare.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Algebra.Groups.Group.
Require Import WildCat.Core.

(** Pullbacks of groups are formalized by equipping the set-pullback with the desired group structure. The universal property in the category of groups is proved by saying that the corecursion principle (grp_pullback_corec) is an equivalence. *) 

Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

Section GrpPullback.

  (* Variables are named to correspond with Limits.Pullback. *)
  Context {A B C : Group} (f : B $-> A) (g : C $-> A).

  Local Instance grp_pullback_sgop : SgOp (Pullback f g).
A, B, C: Group
f: B $-> A
g: C $-> A
SgOp (Pullback f g)
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
SgOp (Pullback f g)
    intros [b [c p]] [d [e q]].
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
d: B
e: C
q: f d = g e
Pullback f g
    refine (b * d; c * e; _).
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
d: B
e: C
q: f d = g e
f (b * d) = g (c * e)
    refine (grp_homo_op f b d @ (_ @ _) @ (grp_homo_op g c e)^).
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
d: B
e: C
q: f d = g e
f b * f d = ?Goal
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
d: B
e: C
q: f d = g e
?Goal = g c * g e
    -
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
d: B
e: C
q: f d = g e
f b * f d = ?Goal exact (ap (fun y:A => f b * y) q).
    -
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
d: B
e: C
q: f d = g e
f b * g e = g c * g e exact (ap (fun x:A => x * g e) p).
  Defined.

  Local Instance grp_pullback_sgop_associative
    : Associative grp_pullback_sgop.
A, B, C: Group
f: B $-> A
g: C $-> A
Associative grp_pullback_sgop
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
Associative grp_pullback_sgop
    intros [x1 [x2 p]] [y1 [y2 q]] [z1 [z2 u]].
A, B, C: Group
f: B $-> A
g: C $-> A
x1: B
x2: C
p: f x1 = g x2
y1: B
y2: C
q: f y1 = g y2
z1: B
z2: C
u: f z1 = g z2
grp_pullback_sgop (x1; x2; p)
  (grp_pullback_sgop (y1; y2; q) (z1; z2; u)) =
grp_pullback_sgop
  (grp_pullback_sgop (x1; x2; p) (y1; y2; q))
  (z1; z2; u)
    apply equiv_path_pullback; simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
x1: B
x2: C
p: f x1 = g x2
y1: B
y2: C
q: f y1 = g y2
z1: B
z2: C
u: f z1 = g z2
{p0 : x1 * (y1 * z1) = x1 * y1 * z1 &
{q0 : x2 * (y2 * z2) = x2 * y2 * z2 &
PathSquare (ap f p0) (ap g q0)
  ((grp_homo_op f x1 (y1 * z1) @
    (ap (fun y : A => f x1 * y)
       ((grp_homo_op f y1 z1 @
         (ap (fun y : A => f y1 * y) u @
          ap (fun x : A => x * g z2) q)) @
        (grp_homo_op g y2 z2)^) @
     ap (fun x : A => x * g (y2 * z2)) p)) @
   (grp_homo_op g x2 (y2 * z2))^)
  ((grp_homo_op f (x1 * y1) z1 @
    (ap (fun y : A => f (x1 * y1) * y) u @
     ap (fun x : A => x * g z2)
       ((grp_homo_op f x1 y1 @
         (ap (fun y : A => f x1 * y) q @
          ap (fun x : A => x * g y2) p)) @
        (grp_homo_op g x2 y2)^))) @
   (grp_homo_op g (x2 * y2) z2)^)}}
    refine (associativity _ _ _; associativity _ _ _; _).
A, B, C: Group
f: B $-> A
g: C $-> A
x1: B
x2: C
p: f x1 = g x2
y1: B
y2: C
q: f y1 = g y2
z1: B
z2: C
u: f z1 = g z2
PathSquare (ap f (associativity x1 y1 z1))
  (ap g (associativity x2 y2 z2))
  ((grp_homo_op f x1 (y1 * z1) @
    (ap (fun y : A => f x1 * y)
       ((grp_homo_op f y1 z1 @
         (ap (fun y : A => f y1 * y) u @
          ap (fun x : A => x * g z2) q)) @
        (grp_homo_op g y2 z2)^) @
     ap (fun x : A => x * g (y2 * z2)) p)) @
   (grp_homo_op g x2 (y2 * z2))^)
  ((grp_homo_op f (x1 * y1) z1 @
    (ap (fun y : A => f (x1 * y1) * y) u @
     ap (fun x : A => x * g z2)
       ((grp_homo_op f x1 y1 @
         (ap (fun y : A => f x1 * y) q @
          ap (fun x : A => x * g y2) p)) @
        (grp_homo_op g x2 y2)^))) @
   (grp_homo_op g (x2 * y2) z2)^)
    apply equiv_sq_path.
A, B, C: Group
f: B $-> A
g: C $-> A
x1: B
x2: C
p: f x1 = g x2
y1: B
y2: C
q: f y1 = g y2
z1: B
z2: C
u: f z1 = g z2
ap f (associativity x1 y1 z1) @
((grp_homo_op f (x1 * y1) z1 @
  (ap (fun y : A => f (x1 * y1) * y) u @
   ap (fun x : A => x * g z2)
     ((grp_homo_op f x1 y1 @
       (ap (fun y : A => f x1 * y) q @
        ap (fun x : A => x * g y2) p)) @
      (grp_homo_op g x2 y2)^))) @
 (grp_homo_op g (x2 * y2) z2)^) =
((grp_homo_op f x1 (y1 * z1) @
  (ap (fun y : A => f x1 * y)
     ((grp_homo_op f y1 z1 @
       (ap (fun y : A => f y1 * y) u @
        ap (fun x : A => x * g z2) q)) @
      (grp_homo_op g y2 z2)^) @
   ap (fun x : A => x * g (y2 * z2)) p)) @
 (grp_homo_op g x2 (y2 * z2))^) @
ap g (associativity x2 y2 z2)
    apply path_ishprop.
  Defined.

  Local Instance grp_pullback_issemigroup : IsSemiGroup (Pullback f g) := {}.

  Local Instance grp_pullback_mon_unit : MonUnit (Pullback f g)
    := (1; 1; grp_homo_unit f @ (grp_homo_unit g)^).

  Local Instance grp_pullback_leftidentity
    : LeftIdentity grp_pullback_sgop grp_pullback_mon_unit.
A, B, C: Group
f: B $-> A
g: C $-> A
LeftIdentity grp_pullback_sgop grp_pullback_mon_unit
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
LeftIdentity grp_pullback_sgop grp_pullback_mon_unit
    intros [b [c p]]; simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
grp_pullback_sgop grp_pullback_mon_unit (b; c; p) =
(b; c; p)
    apply equiv_path_pullback; simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
{p0 : 1 * b = b &
{q : 1 * c = c &
PathSquare (ap f p0) (ap g q)
  ((grp_homo_op f one b @
    (ap (fun y : A => f one * y) p @
     ap (fun x : A => x * g c)
       (grp_homo_unit f @ (grp_homo_unit g)^))) @
   (grp_homo_op g one c)^) p}}
    refine (left_identity _; left_identity _; _).
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
PathSquare (ap f (left_identity b))
  (ap g (left_identity c))
  ((grp_homo_op f one b @
    (ap (fun y : A => f one * y) p @
     ap (fun x : A => x * g c)
       (grp_homo_unit f @ (grp_homo_unit g)^))) @
   (grp_homo_op g one c)^) p
    apply equiv_sq_path.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
ap f (left_identity b) @ p =
((grp_homo_op f one b @
  (ap (fun y : A => f one * y) p @
   ap (fun x : A => x * g c)
     (grp_homo_unit f @ (grp_homo_unit g)^))) @
 (grp_homo_op g one c)^) @ ap g (left_identity c)
    apply path_ishprop.
  Defined.

  Local Instance grp_pullback_rightidentity
    : RightIdentity grp_pullback_sgop grp_pullback_mon_unit.
A, B, C: Group
f: B $-> A
g: C $-> A
RightIdentity grp_pullback_sgop grp_pullback_mon_unit
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
RightIdentity grp_pullback_sgop grp_pullback_mon_unit
    intros [b [c p]]; simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
grp_pullback_sgop (b; c; p) grp_pullback_mon_unit =
(b; c; p)
    apply equiv_path_pullback; simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
{p0 : b * 1 = b &
{q : c * 1 = c &
PathSquare (ap f p0) (ap g q)
  ((grp_homo_op f b one @
    (ap (fun y : A => f b * y)
       (grp_homo_unit f @ (grp_homo_unit g)^) @
     ap (fun x : A => x * g one) p)) @
   (grp_homo_op g c one)^) p}}
    refine (right_identity _; right_identity _; _).
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
PathSquare (ap f (right_identity b))
  (ap g (right_identity c))
  ((grp_homo_op f b one @
    (ap (fun y : A => f b * y)
       (grp_homo_unit f @ (grp_homo_unit g)^) @
     ap (fun x : A => x * g one) p)) @
   (grp_homo_op g c one)^) p
    apply equiv_sq_path.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
ap f (right_identity b) @ p =
((grp_homo_op f b one @
  (ap (fun y : A => f b * y)
     (grp_homo_unit f @ (grp_homo_unit g)^) @
   ap (fun x : A => x * g one) p)) @
 (grp_homo_op g c one)^) @ ap g (right_identity c)
    apply path_ishprop.
  Defined.

  Local Instance ismonoid_grp_pullback : IsMonoid (Pullback f g) := {}.

  Local Instance grp_pullback_negate : Negate (Pullback f g).
A, B, C: Group
f: B $-> A
g: C $-> A
Negate (Pullback f g)
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
Negate (Pullback f g)
    intros [b [c p]].
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
Pullback f g
    refine (-b; -c; grp_homo_inv f b @ _ @ (grp_homo_inv g c)^).
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
- f b = - g c
    exact (ap (fun a => -a) p).
  Defined.

  Local Instance grp_pullback_leftinverse
    : LeftInverse grp_pullback_sgop grp_pullback_negate grp_pullback_mon_unit.
A, B, C: Group
f: B $-> A
g: C $-> A
LeftInverse grp_pullback_sgop grp_pullback_negate
  grp_pullback_mon_unit
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
LeftInverse grp_pullback_sgop grp_pullback_negate
  grp_pullback_mon_unit
    unfold LeftInverse.
A, B, C: Group
f: B $-> A
g: C $-> A
forall x : Pullback f g,
grp_pullback_sgop (grp_pullback_negate x) x =
grp_pullback_mon_unit
    intros [b [c p]].
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
grp_pullback_sgop (grp_pullback_negate (b; c; p))
  (b; c; p) = grp_pullback_mon_unit
    unfold grp_pullback_sgop; simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
(- b * b; - c * c;
(grp_homo_op f (- b) b @
 (ap (fun y : A => f (- b) * y) p @
  ap (fun x : A => x * g c)
    ((grp_homo_inv f b @ ap (fun a : A => - a) p) @
     (grp_homo_inv g c)^))) @ (grp_homo_op g (- c) c)^) =
grp_pullback_mon_unit
    apply equiv_path_pullback; simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
{p0 : - b * b = 1 &
{q : - c * c = 1 &
PathSquare (ap f p0) (ap g q)
  ((grp_homo_op f (- b) b @
    (ap (fun y : A => f (- b) * y) p @
     ap (fun x : A => x * g c)
       ((grp_homo_inv f b @ ap (fun a : A => - a) p) @
        (grp_homo_inv g c)^))) @
   (grp_homo_op g (- c) c)^)
  (grp_homo_unit f @ (grp_homo_unit g)^)}}
    refine (left_inverse _; left_inverse _; _).
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
PathSquare (ap f (left_inverse b))
  (ap g (left_inverse c))
  ((grp_homo_op f (- b) b @
    (ap (fun y : A => f (- b) * y) p @
     ap (fun x : A => x * g c)
       ((grp_homo_inv f b @ ap (fun a : A => - a) p) @
        (grp_homo_inv g c)^))) @
   (grp_homo_op g (- c) c)^)
  (grp_homo_unit f @ (grp_homo_unit g)^)
    apply equiv_sq_path.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
ap f (left_inverse b) @
(grp_homo_unit f @ (grp_homo_unit g)^) =
((grp_homo_op f (- b) b @
  (ap (fun y : A => f (- b) * y) p @
   ap (fun x : A => x * g c)
     ((grp_homo_inv f b @ ap (fun a : A => - a) p) @
      (grp_homo_inv g c)^))) @
 (grp_homo_op g (- c) c)^) @ ap g (left_inverse c)
    apply path_ishprop.
  Defined.

  Local Instance grp_pullback_rightinverse
    : RightInverse grp_pullback_sgop grp_pullback_negate grp_pullback_mon_unit.
A, B, C: Group
f: B $-> A
g: C $-> A
RightInverse grp_pullback_sgop grp_pullback_negate
  grp_pullback_mon_unit
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
RightInverse grp_pullback_sgop grp_pullback_negate
  grp_pullback_mon_unit
    intros [b [c p]].
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
grp_pullback_sgop (b; c; p)
  (grp_pullback_negate (b; c; p)) =
grp_pullback_mon_unit
    unfold grp_pullback_sgop; simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
(b * - b; c * - c;
(grp_homo_op f b (- b) @
 (ap (fun y : A => f b * y)
    ((grp_homo_inv f b @ ap (fun a : A => - a) p) @
     (grp_homo_inv g c)^) @
  ap (fun x : A => x * g (- c)) p)) @
(grp_homo_op g c (- c))^) = grp_pullback_mon_unit
    apply equiv_path_pullback; simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
{p0 : b * - b = 1 &
{q : c * - c = 1 &
PathSquare (ap f p0) (ap g q)
  ((grp_homo_op f b (- b) @
    (ap (fun y : A => f b * y)
       ((grp_homo_inv f b @ ap (fun a : A => - a) p) @
        (grp_homo_inv g c)^) @
     ap (fun x : A => x * g (- c)) p)) @
   (grp_homo_op g c (- c))^)
  (grp_homo_unit f @ (grp_homo_unit g)^)}}
    refine (right_inverse _; right_inverse _; _).
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
PathSquare (ap f (right_inverse b))
  (ap g (right_inverse c))
  ((grp_homo_op f b (- b) @
    (ap (fun y : A => f b * y)
       ((grp_homo_inv f b @ ap (fun a : A => - a) p) @
        (grp_homo_inv g c)^) @
     ap (fun x : A => x * g (- c)) p)) @
   (grp_homo_op g c (- c))^)
  (grp_homo_unit f @ (grp_homo_unit g)^)
    apply equiv_sq_path.
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
ap f (right_inverse b) @
(grp_homo_unit f @ (grp_homo_unit g)^) =
((grp_homo_op f b (- b) @
  (ap (fun y : A => f b * y)
     ((grp_homo_inv f b @ ap (fun a : A => - a) p) @
      (grp_homo_inv g c)^) @
   ap (fun x : A => x * g (- c)) p)) @
 (grp_homo_op g c (- c))^) @ ap g (right_inverse c)
    apply path_ishprop.
  Defined.

  Global Instance isgroup_grp_pullback : IsGroup (Pullback f g) := {}.

  Definition grp_pullback : Group
    := Build_Group (Pullback f g) _ _ _ _.

  Definition grp_pullback_pr1 : grp_pullback $-> B.
A, B, C: Group
f: B $-> A
g: C $-> A
grp_pullback $-> B
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
grp_pullback $-> B
    snrapply Build_GroupHomomorphism.
A, B, C: Group
f: B $-> A
g: C $-> A
grp_pullback -> B
A, B, C: Group
f: B $-> A
g: C $-> A
IsSemiGroupPreserving ?f
    -
A, B, C: Group
f: B $-> A
g: C $-> A
grp_pullback -> B apply pullback_pr1.
    -
A, B, C: Group
f: B $-> A
g: C $-> A
IsSemiGroupPreserving pullback_pr1 intros x y.
A, B, C: Group
f: B $-> A
g: C $-> A
x, y: grp_pullback
pullback_pr1 (x * y) = pullback_pr1 x * pullback_pr1 y reflexivity.
  Defined.

  Definition grp_pullback_pr2 : grp_pullback $-> C.
A, B, C: Group
f: B $-> A
g: C $-> A
grp_pullback $-> C
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
grp_pullback $-> C
    snrapply Build_GroupHomomorphism.
A, B, C: Group
f: B $-> A
g: C $-> A
grp_pullback -> C
A, B, C: Group
f: B $-> A
g: C $-> A
IsSemiGroupPreserving ?f
    -
A, B, C: Group
f: B $-> A
g: C $-> A
grp_pullback -> C apply pullback_pr2.
    -
A, B, C: Group
f: B $-> A
g: C $-> A
IsSemiGroupPreserving pullback_pr2 intros x y.
A, B, C: Group
f: B $-> A
g: C $-> A
x, y: grp_pullback
pullback_pr2 (x * y) = pullback_pr2 x * pullback_pr2 y reflexivity.
  Defined.

  Proposition grp_pullback_corec {X : Group}
              (b : X $-> B) (c : X $-> C)
              (p : f o b == g o c)
    : X $-> grp_pullback.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
X $-> grp_pullback
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
X $-> grp_pullback
    snrapply Build_GroupHomomorphism.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
X -> grp_pullback
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
IsSemiGroupPreserving ?f
    -
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
X -> grp_pullback exact (fun x => (b x; c x; p x)).
    -
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
IsSemiGroupPreserving (fun x : X => (b x; c x; p x)) intros x y.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
(b (x * y); c (x * y); p (x * y)) =
(b x; c x; p x) * (b y; c y; p y)
      srapply path_sigma.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
(b (x * y); c (x * y); p (x * y)).1 =
((b x; c x; p x) * (b y; c y; p y)).1
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
transport (fun b : B => {c : C & f b = g c}) ?p
  (b (x * y); c (x * y); p (x * y)).2 =
((b x; c x; p x) * (b y; c y; p y)).2
      +
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
(b (x * y); c (x * y); p (x * y)).1 =
((b x; c x; p x) * (b y; c y; p y)).1 simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
b (x * y) = b x * b y
        apply (grp_homo_op b).
      +
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
transport (fun b : B => {c : C & f b = g c})
  (grp_homo_op b x y
   :
   (b (x * y); c (x * y); p (x * y)).1 =
   ((b x; c x; p x) * (b y; c y; p y)).1)
  (b (x * y); c (x * y); p (x * y)).2 =
((b x; c x; p x) * (b y; c y; p y)).2 unfold pr2.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
transport (fun b : B => {c : C & f b = g c})
  (grp_homo_op b x y) (c (x * y); p (x * y)) =
((b x; c x; p x) * (b y; c y; p y)).2
        refine (transport_sigma' _ _ @ _).
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
((c (x * y); p (x * y)).1;
transport
  (fun x0 : B => f x0 = g (c (x * y); p (x * y)).1)
  (grp_homo_op b x y) (c (x * y); p (x * y)).2) =
(c x * c y;
(grp_homo_op f (b x) (b y) @
 (ap (fun y : A => f (b x) * y) (p y) @
  ap (fun x : A => x * g (c y)) (p x))) @
(grp_homo_op g (c x) (c y))^) unfold pr1.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
(c (x * y);
transport (fun x0 : B => f x0 = g (c (x * y)))
  (grp_homo_op b x y) (c (x * y); p (x * y)).2) =
(c x * c y;
(grp_homo_op f (b x) (b y) @
 (ap (fun y : A => f (b x) * y) (p y) @
  ap (fun x : A => x * g (c y)) (p x))) @
(grp_homo_op g (c x) (c y))^)
        apply path_sigma_hprop.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
(c (x * y);
transport (fun x0 : B => f x0 = g (c (x * y)))
  (grp_homo_op b x y) (c (x * y); p (x * y)).2).1 =
(c x * c y;
(grp_homo_op f (b x) (b y) @
 (ap (fun y : A => f (b x) * y) (p y) @
  ap (fun x : A => x * g (c y)) (p x))) @
(grp_homo_op g (c x) (c y))^).1
        simpl.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
x, y: X
c (x * y) = c x * c y
        apply (grp_homo_op c).
  Defined.

  Corollary grp_pullback_corec' (X : Group)
    : {b : X $-> B & { c : X $-> C & f o b == g o c}}
      -> (X $-> grp_pullback).
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
{b : X $-> B & {c : X $-> C & f o b == g o c}} ->
X $-> grp_pullback
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
{b : X $-> B & {c : X $-> C & f o b == g o c}} ->
X $-> grp_pullback
    intros [b [c p]]; exact (grp_pullback_corec b c p).
  Defined.

End GrpPullback.

Definition functor_grp_pullback {A A' B B' C C' : Group}
           (f : B $-> A) (f' : B' $-> A')
           (g : C $-> A) (g' : C' $-> A')
           (alpha : A $-> A') (beta : B $-> B') (gamma : C $-> C')
           (h : f' o beta == alpha o f)
           (k : alpha o g == g' o gamma)
  : grp_pullback f g $-> grp_pullback f' g'.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
grp_pullback f g $-> grp_pullback f' g'
Proof.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
grp_pullback f g $-> grp_pullback f' g'
  srapply grp_pullback_corec.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
grp_pullback f g $-> B'
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
grp_pullback f g $-> C'
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
f' o ?b == g' o ?c
  -
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
grp_pullback f g $-> B' exact (beta $o grp_pullback_pr1 f g).
  -
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
grp_pullback f g $-> C' exact (gamma $o grp_pullback_pr2 f g).
  -
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
f' o (beta $o grp_pullback_pr1 f g) ==
g' o (gamma $o grp_pullback_pr2 f g) intro x; cbn.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
x: grp_pullback f g
f' (beta (pullback_pr1 x)) =
g' (gamma (pullback_pr2 x))
    refine (h _ @ ap alpha _ @ k _).
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: A $-> A'
beta: B $-> B'
gamma: C $-> C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
x: grp_pullback f g
f (pullback_pr1 x) = g (pullback_pr2 x)
    apply pullback_commsq.
Defined.

Definition equiv_functor_grp_pullback {A A' B B' C C' : Group}
           (f : B $-> A) (f' : B' $-> A')
           (g : C $-> A) (g' : C' $-> A')
           (alpha : GroupIsomorphism A A')
           (beta : GroupIsomorphism B B')
           (gamma : GroupIsomorphism C C')
           (h : f' o beta == alpha o f)
           (k : alpha o g == g' o gamma)
  : GroupIsomorphism (grp_pullback f g) (grp_pullback f' g').
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
GroupIsomorphism (grp_pullback f g)
  (grp_pullback f' g')
Proof.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
GroupIsomorphism (grp_pullback f g)
  (grp_pullback f' g')
  srapply Build_GroupIsomorphism.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
GroupHomomorphism (grp_pullback f g)
  (grp_pullback f' g')
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
IsEquiv ?grp_iso_homo
  1: exact (functor_grp_pullback f f' g g' _ _ _ h k).
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
IsEquiv
  (functor_grp_pullback f f' g g' alpha beta gamma h k)
  srapply isequiv_adjointify.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
grp_pullback f' g' -> grp_pullback f g
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
functor_grp_pullback f f' g g' alpha beta gamma h k
o ?g == idmap
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
?g
o functor_grp_pullback f f' g g' alpha beta gamma h k ==
idmap
  {
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
grp_pullback f' g' -> grp_pullback f g srapply (functor_grp_pullback f' f g' g).
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
A' $-> A
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
B' $-> B
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
C' $-> C
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
f o ?beta == ?alpha o f'
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
?alpha o g' == g o ?gamma
    1-3: rapply grp_iso_inverse; assumption.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
f o grp_iso_inverse beta == grp_iso_inverse alpha o f'
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
grp_iso_inverse alpha o g' ==
g o grp_iso_inverse gamma
    +
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
f o grp_iso_inverse beta == grp_iso_inverse alpha o f' rapply (equiv_ind beta); intro b.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
b: B
f (grp_iso_inverse beta (beta b)) =
grp_iso_inverse alpha (f' (beta b))
      refine (ap f (eissect _ _) @ _).
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
b: B
f b = grp_iso_inverse alpha (f' (beta b))
      apply (equiv_ap' alpha _ _)^-1.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
b: B
alpha (f b) =
alpha (grp_iso_inverse alpha (f' (beta b)))
      exact ((h b)^ @ (eisretr _ _)^).
    +
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
grp_iso_inverse alpha o g' ==
g o grp_iso_inverse gamma rapply (equiv_ind gamma); intro c.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
c: C
grp_iso_inverse alpha (g' (gamma c)) =
g (grp_iso_inverse gamma (gamma c))
      refine (_ @ ap g (eissect _ _)^).
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
c: C
grp_iso_inverse alpha (g' (gamma c)) = g c
      apply (equiv_ap' alpha _ _)^-1.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
c: C
alpha (grp_iso_inverse alpha (g' (gamma c))) =
alpha (g c)
      exact (eisretr _ _ @ (k c)^). }
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
functor_grp_pullback f f' g g' alpha beta gamma h k
o functor_grp_pullback f' f g' g
    (grp_iso_inverse alpha) (grp_iso_inverse beta)
    (grp_iso_inverse gamma)
    (equiv_ind beta
       (fun y : B' =>
        (f o grp_iso_inverse beta) y =
        (grp_iso_inverse alpha o f') y)
       (fun b : B =>
        ap f (eissect beta b) @
        (equiv_ap' alpha (f b)
           (grp_iso_inverse alpha (f' (beta b))))^-1
          ((h b)^ @ (eisretr alpha (f' (beta b)))^)))
    (equiv_ind gamma
       (fun y : C' =>
        (grp_iso_inverse alpha o g') y =
        (g o grp_iso_inverse gamma) y)
       (fun c : C =>
        (equiv_ap' alpha
           (grp_iso_inverse alpha (g' (gamma c)))
           (g c))^-1
          (eisretr alpha (g' (gamma c)) @ (k c)^) @
        ap g (eissect gamma c)^)) == idmap
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
functor_grp_pullback f' f g' g 
  (grp_iso_inverse alpha) 
  (grp_iso_inverse beta) 
  (grp_iso_inverse gamma)
  (equiv_ind beta
     (fun y : B' =>
      (f o grp_iso_inverse beta) y =
      (grp_iso_inverse alpha o f') y)
     (fun b : B =>
      ap f (eissect beta b) @
      (equiv_ap' alpha (f b)
         (grp_iso_inverse alpha (f' (beta b))))^-1
        ((h b)^ @ (eisretr alpha (f' (beta b)))^)))
  (equiv_ind gamma
     (fun y : C' =>
      (grp_iso_inverse alpha o g') y =
      (g o grp_iso_inverse gamma) y)
     (fun c : C =>
      (equiv_ap' alpha
         (grp_iso_inverse alpha (g' (gamma c))) 
         (g c))^-1
        (eisretr alpha (g' (gamma c)) @ (k c)^) @
      ap g (eissect gamma c)^))
o functor_grp_pullback f f' g g' alpha beta gamma h k ==
idmap
  all: intro x;
    apply equiv_path_pullback_hset; split; cbn.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
x: grp_pullback f' g'
beta (beta^-1 (pullback_pr1 x)) = x.1
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
x: grp_pullback f' g'
gamma (gamma^-1 (pullback_pr2 x)) = (x.2).1
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
x: grp_pullback f g
beta^-1 (beta (pullback_pr1 x)) = x.1
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
x: grp_pullback f g
gamma^-1 (gamma (pullback_pr2 x)) = (x.2).1
  1-2: apply eisretr.
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
x: grp_pullback f g
beta^-1 (beta (pullback_pr1 x)) = x.1
A, A', B, B', C, C': Group
f: B $-> A
f': B' $-> A'
g: C $-> A
g': C' $-> A'
alpha: GroupIsomorphism A A'
beta: GroupIsomorphism B B'
gamma: GroupIsomorphism C C'
h: f' o beta == alpha o f
k: alpha o g == g' o gamma
x: grp_pullback f g
gamma^-1 (gamma (pullback_pr2 x)) = (x.2).1
  1-2: apply eissect.
Defined.

(** Pulling back along some [g : Y $-> Z] and then [g' : Y' $-> Y] is the same as pulling back along [g $o g']. *)
Definition equiv_grp_pullback_compose_r {X Z Y Y' : Group} (f : X $-> Z) (g' : Y' $-> Y) (g : Y $-> Z)
  : GroupIsomorphism (grp_pullback (grp_pullback_pr2 f g) g') (grp_pullback f (g $o g')).
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
GroupIsomorphism
  (grp_pullback (grp_pullback_pr2 f g) g')
  (grp_pullback f (g $o g'))
Proof.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
GroupIsomorphism
  (grp_pullback (grp_pullback_pr2 f g) g')
  (grp_pullback f (g $o g'))
  srapply Build_GroupIsomorphism.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
GroupHomomorphism
  (grp_pullback (grp_pullback_pr2 f g) g')
  (grp_pullback f (g $o g'))
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
IsEquiv ?grp_iso_homo
  -
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
GroupHomomorphism
  (grp_pullback (grp_pullback_pr2 f g) g')
  (grp_pullback f (g $o g')) srapply grp_pullback_corec.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback (grp_pullback_pr2 f g) g' $-> X
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback (grp_pullback_pr2 f g) g' $-> Y'
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
f o ?b == g $o g' o ?c
    +
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback (grp_pullback_pr2 f g) g' $-> X exact (grp_pullback_pr1 _ _ $o grp_pullback_pr1 _ _).
    +
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback (grp_pullback_pr2 f g) g' $-> Y' apply grp_pullback_pr2.
    +
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
f
o (grp_pullback_pr1 f g $o
   grp_pullback_pr1 (grp_pullback_pr2 f g) g') ==
g $o g' o grp_pullback_pr2 (grp_pullback_pr2 f g) g' intro x; cbn.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
x: grp_pullback (grp_pullback_pr2 f g) g'
f (pullback_pr1 (pullback_pr1 x)) =
g (g' (pullback_pr2 x))
      exact (pullback_commsq _ _ _ @ ap g (pullback_commsq _ _ _)).
  -
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
IsEquiv
  (grp_pullback_corec f (g $o g')
     (grp_pullback_pr1 f g $o
      grp_pullback_pr1 (grp_pullback_pr2 f g) g')
     (grp_pullback_pr2 (grp_pullback_pr2 f g) g')
     ((fun x : grp_pullback (grp_pullback_pr2 f g) g'
       =>
       pullback_commsq f g (pullback_pr1 x) @
       ap g (pullback_commsq pullback_pr2 g' x)
       :
       f
         ((grp_pullback_pr1 f g $o
           grp_pullback_pr1 (grp_pullback_pr2 f g) g')
            x) =
       (g $o g')
         (grp_pullback_pr2 (grp_pullback_pr2 f g) g' x))
      :
      f
      o (grp_pullback_pr1 f g $o
         grp_pullback_pr1 (grp_pullback_pr2 f g) g') ==
      g $o g'
      o grp_pullback_pr2 (grp_pullback_pr2 f g) g')) srapply isequiv_adjointify.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback f (g $o g') ->
grp_pullback (grp_pullback_pr2 f g) g'
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback_corec f (g $o g')
  (grp_pullback_pr1 f g $o
   grp_pullback_pr1 (grp_pullback_pr2 f g) g')
  (grp_pullback_pr2 (grp_pullback_pr2 f g) g')
  ((fun x : grp_pullback (grp_pullback_pr2 f g) g' =>
    pullback_commsq f g (pullback_pr1 x) @
    ap g (pullback_commsq pullback_pr2 g' x)
    :
    f
      ((grp_pullback_pr1 f g $o
        grp_pullback_pr1 (grp_pullback_pr2 f g) g') x) =
    (g $o g')
      (grp_pullback_pr2 (grp_pullback_pr2 f g) g' x))
   :
   f
   o (grp_pullback_pr1 f g $o
      grp_pullback_pr1 (grp_pullback_pr2 f g) g') ==
   g $o g'
   o grp_pullback_pr2 (grp_pullback_pr2 f g) g') o 
?g == idmap
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
?g
o grp_pullback_corec f (g $o g')
    (grp_pullback_pr1 f g $o
     grp_pullback_pr1 (grp_pullback_pr2 f g) g')
    (grp_pullback_pr2 (grp_pullback_pr2 f g) g')
    ((fun x : grp_pullback (grp_pullback_pr2 f g) g'
      =>
      pullback_commsq f g (pullback_pr1 x) @
      ap g (pullback_commsq pullback_pr2 g' x)
      :
      f
        ((grp_pullback_pr1 f g $o
          grp_pullback_pr1 (grp_pullback_pr2 f g) g')
           x) =
      (g $o g')
        (grp_pullback_pr2 (grp_pullback_pr2 f g) g' x))
     :
     f
     o (grp_pullback_pr1 f g $o
        grp_pullback_pr1 (grp_pullback_pr2 f g) g') ==
     g $o g'
     o grp_pullback_pr2 (grp_pullback_pr2 f g) g') ==
idmap
    +
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback f (g $o g') ->
grp_pullback (grp_pullback_pr2 f g) g' srapply grp_pullback_corec.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback f (g $o g') $-> grp_pullback f g
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback f (g $o g') $-> Y'
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback_pr2 f g o ?b == g' o ?c
      *
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback f (g $o g') $-> grp_pullback f g srapply functor_grp_pullback.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
Z $-> Z
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
X $-> X
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
Y' $-> Y
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
f o ?beta == ?alpha o f
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
?alpha o (g $o g') == g o ?gamma
        1,2: exact grp_homo_id.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
Y' $-> Y
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
f o grp_homo_id == grp_homo_id o f
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_homo_id o (g $o g') == g o ?gamma
        1: exact g'.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
f o grp_homo_id == grp_homo_id o f
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_homo_id o (g $o g') == g o g'
        all: reflexivity.
      *
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback f (g $o g') $-> Y' apply grp_pullback_pr2.
      *
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback_pr2 f g
o functor_grp_pullback f f (g $o g') g grp_homo_id
    grp_homo_id g' (fun x0 : X => 1%path)
    (fun x0 : Y' => 1%path) ==
g' o grp_pullback_pr2 f (g $o g') reflexivity.
    +
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback_corec f (g $o g')
  (grp_pullback_pr1 f g $o
   grp_pullback_pr1 (grp_pullback_pr2 f g) g')
  (grp_pullback_pr2 (grp_pullback_pr2 f g) g')
  ((fun x : grp_pullback (grp_pullback_pr2 f g) g' =>
    pullback_commsq f g (pullback_pr1 x) @
    ap g (pullback_commsq pullback_pr2 g' x)
    :
    f
      ((grp_pullback_pr1 f g $o
        grp_pullback_pr1 (grp_pullback_pr2 f g) g') x) =
    (g $o g')
      (grp_pullback_pr2 (grp_pullback_pr2 f g) g' x))
   :
   f
   o (grp_pullback_pr1 f g $o
      grp_pullback_pr1 (grp_pullback_pr2 f g) g') ==
   g $o g'
   o grp_pullback_pr2 (grp_pullback_pr2 f g) g')
o grp_pullback_corec (grp_pullback_pr2 f g) g'
    (functor_grp_pullback f f (g $o g') g grp_homo_id
       grp_homo_id g' (fun x0 : X => 1%path)
       (fun x0 : Y' => 1%path))
    (grp_pullback_pr2 f (g $o g'))
    (fun x0 : Pullback f (fun x : Y' => g (g' x)) =>
     1%path) == idmap intro x; cbn.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
x: grp_pullback f (g $o g')
(pullback_pr1 x; pullback_pr2 x;
((1 @
  ap idmap
    (pullback_commsq f (fun x : Y' => g (g' x)) x)) @
 1) @ 1) = x
      by srapply equiv_path_pullback_hset.
    +
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
grp_pullback_corec (grp_pullback_pr2 f g) g'
  (functor_grp_pullback f f (g $o g') g grp_homo_id
     grp_homo_id g' (fun x0 : X => 1%path)
     (fun x0 : Y' => 1%path))
  (grp_pullback_pr2 f (g $o g'))
  (fun x0 : Pullback f (fun x : Y' => g (g' x)) =>
   1%path)
o grp_pullback_corec f (g $o g')
    (grp_pullback_pr1 f g $o
     grp_pullback_pr1 (grp_pullback_pr2 f g) g')
    (grp_pullback_pr2 (grp_pullback_pr2 f g) g')
    ((fun x : grp_pullback (grp_pullback_pr2 f g) g'
      =>
      pullback_commsq f g (pullback_pr1 x) @
      ap g (pullback_commsq pullback_pr2 g' x)
      :
      f
        ((grp_pullback_pr1 f g $o
          grp_pullback_pr1 (grp_pullback_pr2 f g) g')
           x) =
      (g $o g')
        (grp_pullback_pr2 (grp_pullback_pr2 f g) g' x))
     :
     f
     o (grp_pullback_pr1 f g $o
        grp_pullback_pr1 (grp_pullback_pr2 f g) g') ==
     g $o g'
     o grp_pullback_pr2 (grp_pullback_pr2 f g) g') ==
idmap intros [[x [y z0]] [y' z1]]; srapply equiv_path_pullback_hset; split; cbn.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
x: X
y: Y
z0: f x = g y
y': Y'
z1: grp_pullback_pr2 f g (x; y; z0) = g' y'
(x; g' y'; (1 @ ap idmap (z0 @ ap g z1)) @ 1) =
(x; y; z0)
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
x: X
y: Y
z0: f x = g y
y': Y'
z1: grp_pullback_pr2 f g (x; y; z0) = g' y'
y' = y'
      2: reflexivity.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
x: X
y: Y
z0: f x = g y
y': Y'
z1: grp_pullback_pr2 f g (x; y; z0) = g' y'
(x; g' y'; (1 @ ap idmap (z0 @ ap g z1)) @ 1) =
(x; y; z0)
      srapply equiv_path_pullback_hset; split; cbn.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
x: X
y: Y
z0: f x = g y
y': Y'
z1: grp_pullback_pr2 f g (x; y; z0) = g' y'
x = x
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
x: X
y: Y
z0: f x = g y
y': Y'
z1: grp_pullback_pr2 f g (x; y; z0) = g' y'
g' y' = y
      1: reflexivity.
X, Z, Y, Y': Group
f: X $-> Z
g': Y' $-> Y
g: Y $-> Z
x: X
y: Y
z0: f x = g y
y': Y'
z1: grp_pullback_pr2 f g (x; y; z0) = g' y'
g' y' = y
      exact z1^.
Defined.

Section IsEquivGrpPullbackCorec.

  (* New section with Funext at the start of the Context. *)
  Context `{Funext} {A B C : Group} (f : B $-> A) (g : C $-> A).

  Lemma grp_pullback_corec_pr1 {X : Group}
        (b : X $-> B) (c : X $-> C)
        (p : f o b == g o c)
    : grp_pullback_pr1 f g $o grp_pullback_corec f g b c p = b.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
grp_pullback_pr1 f g $o grp_pullback_corec f g b c p =
b
  Proof.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
grp_pullback_pr1 f g $o grp_pullback_corec f g b c p =
b
    apply equiv_path_grouphomomorphism; reflexivity.
  Defined.

  Lemma grp_pullback_corec_pr2 {X : Group}
        (b : X $-> B) (c : X $-> C)
        (p : f o b == g o c)
    : grp_pullback_pr2 f g $o grp_pullback_corec f g b c p = c.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
grp_pullback_pr2 f g $o grp_pullback_corec f g b c p =
c
  Proof.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
b: X $-> B
c: X $-> C
p: f o b == g o c
grp_pullback_pr2 f g $o grp_pullback_corec f g b c p =
c
    apply equiv_path_grouphomomorphism; reflexivity.
  Defined.

  Theorem isequiv_grp_pullback_corec (X : Group)
    : IsEquiv (grp_pullback_corec' f g X).
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
IsEquiv (grp_pullback_corec' f g X)
  Proof.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
IsEquiv (grp_pullback_corec' f g X)
    snrapply isequiv_adjointify.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
(X $-> grp_pullback f g) ->
{b : X $-> B & {c : X $-> C & f o b == g o c}}
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
grp_pullback_corec' f g X o ?g == idmap
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
?g o grp_pullback_corec' f g X == idmap
    -
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
(X $-> grp_pullback f g) ->
{b : X $-> B & {c : X $-> C & f o b == g o c}} intro phi.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
phi: X $-> grp_pullback f g
{b : X $-> B & {c : X $-> C & f o b == g o c}}
      refine (grp_pullback_pr1 f g $o phi; grp_pullback_pr2 f g $o phi; _).
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
phi: X $-> grp_pullback f g
(fun x : X => f ((grp_pullback_pr1 f g $o phi) x)) ==
(fun x : X => g ((grp_pullback_pr2 f g $o phi) x))
      intro x; exact (pullback_commsq f g (phi x)).
    -
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
grp_pullback_corec' f g X
o (fun phi : X $-> grp_pullback f g =>
   (grp_pullback_pr1 f g $o phi;
   grp_pullback_pr2 f g $o phi;
   (fun x : X => pullback_commsq f g (phi x))
   :
   (fun x : X => f ((grp_pullback_pr1 f g $o phi) x)) ==
   (fun x : X => g ((grp_pullback_pr2 f g $o phi) x)))) ==
idmap intro phi.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
phi: X $-> grp_pullback f g
grp_pullback_corec' f g X
  (grp_pullback_pr1 f g $o phi;
  grp_pullback_pr2 f g $o phi;
  fun x : X => pullback_commsq f g (phi x)) = phi
      apply equiv_path_grouphomomorphism; reflexivity.
    -
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
(fun phi : X $-> grp_pullback f g =>
 (grp_pullback_pr1 f g $o phi;
 grp_pullback_pr2 f g $o phi;
 (fun x : X => pullback_commsq f g (phi x))
 :
 (fun x : X => f ((grp_pullback_pr1 f g $o phi) x)) ==
 (fun x : X => g ((grp_pullback_pr2 f g $o phi) x))))
o grp_pullback_corec' f g X == idmap intro bcp; simpl.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
bcp: {b : X $-> B &
{c : X $-> C & (fun x : X => f (b x)) == (fun x : X => g (c x))}}
(grp_homo_compose (grp_pullback_pr1 f g)
   (grp_pullback_corec' f g X bcp);
grp_homo_compose (grp_pullback_pr2 f g)
  (grp_pullback_corec' f g X bcp);
fun x : X =>
pullback_commsq f g
  (bcp.1 x; (bcp.2).1 x; (bcp.2).2 x)) = bcp
      srapply path_sigma.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
bcp: {b : X $-> B &
{c : X $-> C & (fun x : X => f (b x)) == (fun x : X => g (c x))}}
(grp_homo_compose (grp_pullback_pr1 f g)
   (grp_pullback_corec' f g X bcp);
grp_homo_compose (grp_pullback_pr2 f g)
  (grp_pullback_corec' f g X bcp);
fun x : X =>
pullback_commsq f g
  (bcp.1 x; (bcp.2).1 x; (bcp.2).2 x)).1 = bcp.1
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
bcp: {b : X $-> B &
{c : X $-> C & (fun x : X => f (b x)) == (fun x : X => g (c x))}}
transport
  (fun b : GroupHomomorphism X B =>
   {c : GroupHomomorphism X C &
   (fun x : X => f (b x)) == (fun x : X => g (c x))})
  ?p
  (grp_homo_compose (grp_pullback_pr1 f g)
     (grp_pullback_corec' f g X bcp);
  grp_homo_compose (grp_pullback_pr2 f g)
    (grp_pullback_corec' f g X bcp);
  fun x : X =>
  pullback_commsq f g
    (bcp.1 x; (bcp.2).1 x; (bcp.2).2 x)).2 = bcp.2
      +
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
bcp: {b : X $-> B &
{c : X $-> C & (fun x : X => f (b x)) == (fun x : X => g (c x))}}
(grp_homo_compose (grp_pullback_pr1 f g)
   (grp_pullback_corec' f g X bcp);
grp_homo_compose (grp_pullback_pr2 f g)
  (grp_pullback_corec' f g X bcp);
fun x : X =>
pullback_commsq f g
  (bcp.1 x; (bcp.2).1 x; (bcp.2).2 x)).1 = bcp.1 simpl.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
bcp: {b : X $-> B &
{c : X $-> C & (fun x : X => f (b x)) == (fun x : X => g (c x))}}
grp_homo_compose (grp_pullback_pr1 f g)
  (grp_pullback_corec' f g X bcp) = bcp.1 apply grp_pullback_corec_pr1.
      +
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
bcp: {b : X $-> B &
{c : X $-> C & (fun x : X => f (b x)) == (fun x : X => g (c x))}}
transport
  (fun b : GroupHomomorphism X B =>
   {c : GroupHomomorphism X C &
   (fun x : X => f (b x)) == (fun x : X => g (c x))})
  (grp_pullback_corec_pr1 bcp.1 (bcp.2).1 (bcp.2).2
   :
   (grp_homo_compose (grp_pullback_pr1 f g)
      (grp_pullback_corec' f g X bcp);
   grp_homo_compose (grp_pullback_pr2 f g)
     (grp_pullback_corec' f g X bcp);
   fun x : X =>
   pullback_commsq f g
     (bcp.1 x; (bcp.2).1 x; (bcp.2).2 x)).1 = bcp.1)
  (grp_homo_compose (grp_pullback_pr1 f g)
     (grp_pullback_corec' f g X bcp);
  grp_homo_compose (grp_pullback_pr2 f g)
    (grp_pullback_corec' f g X bcp);
  fun x : X =>
  pullback_commsq f g
    (bcp.1 x; (bcp.2).1 x; (bcp.2).2 x)).2 = bcp.2 refine (transport_sigma' _ _ @ _).
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
bcp: {b : X $-> B &
{c : X $-> C & (fun x : X => f (b x)) == (fun x : X => g (c x))}}
(((grp_homo_compose (grp_pullback_pr1 f g)
     (grp_pullback_corec' f g X bcp);
  grp_homo_compose (grp_pullback_pr2 f g)
    (grp_pullback_corec' f g X bcp);
  fun x : X =>
  pullback_commsq f g
    (bcp.1 x; (bcp.2).1 x; (bcp.2).2 x)).2).1;
transport
  (fun x : GroupHomomorphism X B =>
   (fun x0 : X => f (x x0)) ==
   (fun x0 : X =>
    g
      (((grp_homo_compose (grp_pullback_pr1 f g)
           (grp_pullback_corec' f g X bcp);
        grp_homo_compose (grp_pullback_pr2 f g)
          (grp_pullback_corec' f g X bcp);
        fun x1 : X =>
        pullback_commsq f g
          (bcp.1 x1; (bcp.2).1 x1; (bcp.2).2 x1)).2).1
         x0)))
  (grp_pullback_corec_pr1 bcp.1 (bcp.2).1 (bcp.2).2)
  ((grp_homo_compose (grp_pullback_pr1 f g)
      (grp_pullback_corec' f g X bcp);
   grp_homo_compose (grp_pullback_pr2 f g)
     (grp_pullback_corec' f g X bcp);
   fun x : X =>
   pullback_commsq f g
     (bcp.1 x; (bcp.2).1 x; (bcp.2).2 x)).2).2) =
bcp.2
        apply path_sigma_hprop; simpl pr1.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
bcp: {b : X $-> B &
{c : X $-> C & (fun x : X => f (b x)) == (fun x : X => g (c x))}}
grp_homo_compose (grp_pullback_pr2 f g)
  (grp_pullback_corec' f g X bcp) = (bcp.2).1
        simpl.
H: Funext
A, B, C: Group
f: B $-> A
g: C $-> A
X: Group
bcp: {b : X $-> B &
{c : X $-> C & (fun x : X => f (b x)) == (fun x : X => g (c x))}}
grp_homo_compose (grp_pullback_pr2 f g)
  (grp_pullback_corec' f g X bcp) = (bcp.2).1 apply grp_pullback_corec_pr2.
  Defined.

End IsEquivGrpPullbackCorec.