From HoTT Require Import Basics Types Limits.Pullback Cubical.PathSquare.From HoTT Require Import Basics Types Limits.Pullback Cubical.PathSquare.
Require Import Truncations.Core ReflectiveSubuniverse HIT.epi.
Require Import Algebra.Groups.Group.
Require Import WildCat.Core WildCat.Pullbacks WildCat.EpiStable.

(** 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)
    exact (grp_homo_op_agree _ _ p q).
  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_agree f g p (grp_homo_op_agree f g q u))
  (grp_homo_op_agree f g (grp_homo_op_agree f g p q) u)}}
    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_agree f g p (grp_homo_op_agree f g q u))
  (grp_homo_op_agree f g (grp_homo_op_agree f g p q) u)
    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_agree f g (grp_homo_op_agree f g p q) u =
grp_homo_op_agree f g p (grp_homo_op_agree f g q u) @
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_agree f g (grp_homo_unit f @ (grp_homo_unit g)^) p) 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_agree f g (grp_homo_unit f @ (grp_homo_unit g)^) p) 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_agree f g (grp_homo_unit f @ (grp_homo_unit g)^) p @
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_agree f g p (grp_homo_unit f @ (grp_homo_unit g)^)) 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_agree f g p (grp_homo_unit f @ (grp_homo_unit g)^)) 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_agree f g p (grp_homo_unit f @ (grp_homo_unit g)^) @
ap g (right_identity c)
    apply path_ishprop.
  Defined.

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

  Local Instance grp_pullback_inverse : Inverse (Pullback f g).
A, B, C: Group
f: B $-> A
g: C $-> A
Inverse (Pullback f g)
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
Inverse (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 (^) p).
  Defined.

  Local Instance grp_pullback_leftinverse : LeftInverse (.*.) (^) mon_unit.
A, B, C: Group
f: B $-> A
g: C $-> A
LeftInverse sg_op inv 1
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
LeftInverse sg_op inv 1
    unfold LeftInverse.
A, B, C: Group
f: B $-> A
g: C $-> A
forall x : Pullback f g, x^ * x = 1
    intros [b [c p]].
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
(b; c; p)^ * (b; c; p) = 1
    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; c; p)^ * (b; c; p) = 1
    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_agree f g
     ((grp_homo_inv f b @ ap inv p) @ (grp_homo_inv g c)^) p)
  (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_agree f g
     ((grp_homo_inv f b @ ap inv p) @ (grp_homo_inv g c)^) p)
  (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_agree f g ((grp_homo_inv f b @ ap inv p) @ (grp_homo_inv g c)^) p @
ap g (left_inverse c)
    apply path_ishprop.
  Defined.

  Local Instance grp_pullback_rightinverse : RightInverse (.*.) (^) mon_unit.
A, B, C: Group
f: B $-> A
g: C $-> A
RightInverse sg_op inv 1
  Proof.
A, B, C: Group
f: B $-> A
g: C $-> A
RightInverse sg_op inv 1
    intros [b [c p]].
A, B, C: Group
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
(b; c; p) * (b; c; p)^ = 1
    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; c; p) * (b; c; p)^ = 1
    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_agree f g p
     ((grp_homo_inv f b @ ap inv p) @ (grp_homo_inv g 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_agree f g p
     ((grp_homo_inv f b @ ap inv p) @ (grp_homo_inv g 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_agree f g p ((grp_homo_inv f b @ ap inv p) @ (grp_homo_inv g c)^) @
ap g (right_inverse c)
    apply path_ishprop.
  Defined.

  #[export] 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
    snapply 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 ?grp_homo_map
    -
A, B, C: Group
f: B $-> A
g: C $-> A
grp_pullback -> B exact 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
    snapply 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 ?grp_homo_map
    -
A, B, C: Group
f: B $-> A
g: C $-> A
grp_pullback -> C exact 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
    snapply 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 ?grp_homo_map
    -
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 b0 : B => {c0 : C & f b0 = g c0}) ?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 b0 : B => {c0 : C & f b0 = g c0})
  (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 b0 : B => {c0 : C & f b0 = g c0}) (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_agree f g (p x) (p 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_agree f g (p x) (p 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_agree f g (p x) (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
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 x0 : Y' => g (g' x0)) 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
      symmetry; 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)
    snapply 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.

(** The category of groups of 1-pullbacks in the wild sense.  Note that we do not need [Funext] for this. *)
Instance haspullbacks_group : HasPullbacks Group.
HasPullbacks Group
Proof.
HasPullbacks Group
  intros A B C f g.
A, B, C: Group
f: A $-> C
g: B $-> C
CatPullback f g
  snapply Build_CatPullback.
A, B, C: Group
f: A $-> C
g: B $-> C
Group
A, B, C: Group
f: A $-> C
g: B $-> C
?cat_pb $-> A
A, B, C: Group
f: A $-> C
g: B $-> C
?cat_pb $-> B
A, B, C: Group
f: A $-> C
g: B $-> C
f $o ?cat_pb_pr1 $== g $o ?cat_pb_pr2
A, B, C: Group
f: A $-> C
g: B $-> C
forall z : Group,
ZeroGroupoid.carrier
  (ZeroGroupoid.pullback_0gpd (fmap (Yoneda.opyon_0gpd z) f)
     (fmap (Yoneda.opyon_0gpd z) g)) ->
z $-> ?cat_pb
A, B, C: Group
f: A $-> C
g: B $-> C
forall (z : Group)
(khp : ZeroGroupoid.carrier
         (ZeroGroupoid.pullback_0gpd (fmap (Yoneda.opyon_0gpd z) f)
            (fmap (Yoneda.opyon_0gpd z) g))),
?cat_pb_pr1 $o ?cat_pb_corec z khp $-> khp.1
A, B, C: Group
f: A $-> C
g: B $-> C
forall (z : Group)
(khp : ZeroGroupoid.carrier
         (ZeroGroupoid.pullback_0gpd (fmap (Yoneda.opyon_0gpd z) f)
            (fmap (Yoneda.opyon_0gpd z) g))),
?cat_pb_pr2 $o ?cat_pb_corec z khp $-> (khp.2).1
A, B, C: Group
f: A $-> C
g: B $-> C
forall (z : Group) (k h : z $-> ?cat_pb),
?cat_pb_pr1 $o k $== ?cat_pb_pr1 $o h ->
?cat_pb_pr2 $o k $== ?cat_pb_pr2 $o h -> k $== h
  -
A, B, C: Group
f: A $-> C
g: B $-> C
Group exact (grp_pullback f g).
  -
A, B, C: Group
f: A $-> C
g: B $-> C
grp_pullback f g $-> A apply grp_pullback_pr1.
  -
A, B, C: Group
f: A $-> C
g: B $-> C
grp_pullback f g $-> B apply grp_pullback_pr2.
  -
A, B, C: Group
f: A $-> C
g: B $-> C
f $o grp_pullback_pr1 f g $== g $o grp_pullback_pr2 f g apply pullback_commsq.
  -
A, B, C: Group
f: A $-> C
g: B $-> C
forall z : Group,
ZeroGroupoid.carrier
  (ZeroGroupoid.pullback_0gpd (fmap (Yoneda.opyon_0gpd z) f)
     (fmap (Yoneda.opyon_0gpd z) g)) ->
z $-> grp_pullback f g apply grp_pullback_corec'.
  -
A, B, C: Group
f: A $-> C
g: B $-> C
forall (z : Group)
(khp : ZeroGroupoid.carrier
         (ZeroGroupoid.pullback_0gpd (fmap (Yoneda.opyon_0gpd z) f)
            (fmap (Yoneda.opyon_0gpd z) g))),
grp_pullback_pr1 f g $o grp_pullback_corec' f g z khp $-> khp.1 simpl.
A, B, C: Group
f: A $-> C
g: B $-> C
forall (z : Group)
(khp : {x : GroupHomomorphism z A &
       {y : GroupHomomorphism z B &
       (fun x0 : z => f (x x0)) == (fun x0 : z => g (y x0))}}),
(fun x : z => khp.1 x) == khp.1 reflexivity.
  -
A, B, C: Group
f: A $-> C
g: B $-> C
forall (z : Group)
(khp : ZeroGroupoid.carrier
         (ZeroGroupoid.pullback_0gpd (fmap (Yoneda.opyon_0gpd z) f)
            (fmap (Yoneda.opyon_0gpd z) g))),
grp_pullback_pr2 f g $o grp_pullback_corec' f g z khp $-> (khp.2).1 cbn.
A, B, C: Group
f: A $-> C
g: B $-> C
forall (z : Group)
(khp : {x : GroupHomomorphism z A &
       {y : GroupHomomorphism z B &
       (fun x0 : z => f (x x0)) == (fun x0 : z => g (y x0))}}),
(fun x : z => (khp.2).1 x) == (khp.2).1 reflexivity.
  -
A, B, C: Group
f: A $-> C
g: B $-> C
forall (z : Group) (k h : z $-> grp_pullback f g),
grp_pullback_pr1 f g $o k $== grp_pullback_pr1 f g $o h ->
grp_pullback_pr2 f g $o k $== grp_pullback_pr2 f g $o h -> k $== h intros Z k h p1 p2.
A, B, C: Group
f: A $-> C
g: B $-> C
Z: Group
k, h: Z $-> grp_pullback f g
p1: grp_pullback_pr1 f g $o k $== grp_pullback_pr1 f g $o h
p2: grp_pullback_pr2 f g $o k $== grp_pullback_pr2 f g $o h
k $== h
    srapply (pullback_homotopic k h p1 p2).
A, B, C: Group
f: A $-> C
g: B $-> C
Z: Group
k, h: Z $-> grp_pullback f g
p1: grp_pullback_pr1 f g $o k $== grp_pullback_pr1 f g $o h
p2: grp_pullback_pr2 f g $o k $== grp_pullback_pr2 f g $o h
forall a : Z, ap f (p1 a) @ ((h a).2).2 = ((k a).2).2 @ ap g (p2 a)
    intro z.
A, B, C: Group
f: A $-> C
g: B $-> C
Z: Group
k, h: Z $-> grp_pullback f g
p1: grp_pullback_pr1 f g $o k $== grp_pullback_pr1 f g $o h
p2: grp_pullback_pr2 f g $o k $== grp_pullback_pr2 f g $o h
z: Z
ap f (p1 z) @ ((h z).2).2 = ((k z).2).2 @ ap g (p2 z)
    apply path_ishprop. (* Here we use that [C] is 0-truncated. *)
Defined.