Require Import Basics.
Require Import Limits.Pullback Cubical.PathSquare.
Require Export Algebra.Groups.GrpPullback.
Require Import Algebra.AbGroups.AbelianGroup.
Require Import WildCat.Core.

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)).
  Proof.
    unfold Commutative.
    intros [b [c p]] [d [e q]].
    apply equiv_path_pullback; simpl.
    refine (commutativity _ _; commutativity _ _; _).
    apply equiv_sq_path.
    apply path_ishprop.
  Defined.

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

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

End AbPullback.