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.

Local Open Scope mc_add_scope.

(** * 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).

  #[export] 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 : b + d = d + b &
{q0 : c + e = e + c &
PathSquare (ap f p0) (ap g q0)
  (grp_homo_op_agree f g p q)
  (grp_homo_op_agree f g q p)}}
    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_agree f g p q)
  (grp_homo_op_agree f g q p)
    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_agree f g q p =
grp_homo_op_agree f g p q @ ap g (commutativity c e)
    apply path_ishprop.
  Defined.

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

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

End AbPullback.