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

(** * Pullbacks of abelian groups *)

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

  Global Instance ab_pullback_commutative
    : Commutative (@group_sgop (grp_pullback f g)).
A, B, C: AbGroup
f: B $-> A
g: C $-> A
Commutative group_sgop
  Proof.
A, B, C: AbGroup
f: B $-> A
g: C $-> A
Commutative group_sgop
    unfold Commutative.
A, B, C: AbGroup
f: B $-> A
g: C $-> A
forall x y : grp_pullback f g,
group_sgop x y = group_sgop y x
    intros [b [c p]] [d [e q]].
A, B, C: AbGroup
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
d: B
e: C
q: f d = g e
group_sgop (b; c; p) (d; e; q) =
group_sgop (d; e; q) (b; c; p)
    apply equiv_path_pullback; simpl.
A, B, C: AbGroup
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
d: B
e: C
q: f d = g e
{p0 : sg_op b d = sg_op d b &
{q0 : sg_op c e = sg_op e c &
PathSquare (ap f p0) (ap g q0)
  ((grp_homo_op f b d @
    (ap (fun y : A => sg_op (f b) y) q @
     ap (fun x : A => sg_op x (g e)) p)) @
   (grp_homo_op g c e)^)
  ((grp_homo_op f d b @
    (ap (fun y : A => sg_op (f d) y) p @
     ap (fun x : A => sg_op x (g c)) q)) @
   (grp_homo_op g e c)^)}}
    refine (commutativity _ _; commutativity _ _; _).
A, B, C: AbGroup
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
d: B
e: C
q: f d = g e
PathSquare (ap f (commutativity b d))
  (ap g (commutativity c e))
  ((grp_homo_op f b d @
    (ap (fun y : A => sg_op (f b) y) q @
     ap (fun x : A => sg_op x (g e)) p)) @
   (grp_homo_op g c e)^)
  ((grp_homo_op f d b @
    (ap (fun y : A => sg_op (f d) y) p @
     ap (fun x : A => sg_op x (g c)) q)) @
   (grp_homo_op g e c)^)
    apply equiv_sq_path.
A, B, C: AbGroup
f: B $-> A
g: C $-> A
b: B
c: C
p: f b = g c
d: B
e: C
q: f d = g e
ap f (commutativity b d) @
((grp_homo_op f d b @
  (ap (fun y : A => sg_op (f d) y) p @
   ap (fun x : A => sg_op x (g c)) q)) @
 (grp_homo_op g e c)^) =
((grp_homo_op f b d @
  (ap (fun y : A => sg_op (f b) y) q @
   ap (fun x : A => sg_op x (g e)) p)) @
 (grp_homo_op g c e)^) @ ap g (commutativity c e)
    apply path_ishprop.
  Defined.

  Global Instance isabgroup_ab_pullback
    : IsAbGroup (grp_pullback f g) := {}.

  Definition ab_pullback
    : AbGroup := Build_AbGroup (grp_pullback f g) _.

  (** The corecursion principle is inherited from Groups; use grp_pullback_corec and friends from Groups/GrpPullback.v. *)

End AbPullback.