From HoTT Require Import Basics Types.Universe.From HoTT Require Import Basics Types.Universe.
Require Import Truncations.Core HIT.epi Modalities.ReflectiveSubuniverse.
Require Import Limits.Pullback Cubical.PathSquare.
Require Export Algebra.Groups.GrpPullback.
Require Import AbelianGroup AbHom.
Require Import WildCat.Core WildCat.Pullbacks WildCat.EpiStable.

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.

Instance haspullbacks_abgroup : HasPullbacks AbGroup.
HasPullbacks AbGroup
Proof.
HasPullbacks AbGroup
  rapply (haspullbacks_induced abgroup_group).
forall (a b c : AbGroup) (f : a $-> c) (g : b $-> c),
{q : AbGroup & q = cat_pb f g}
  intros A B C f g.
A, B, C: AbGroup
f: A $-> C
g: B $-> C
{q : AbGroup & q = cat_pb f g}
  exists (ab_pullback f g).
A, B, C: AbGroup
f: A $-> C
g: B $-> C
ab_pullback f g = cat_pb f g
  reflexivity.
Defined.

Instance isepistable_abgroup `{Univalence} : IsEpiStable AbGroup.
H: Univalence
IsEpiStable AbGroup
Proof.
H: Univalence
IsEpiStable AbGroup
  srapply Build_IsEpiStable.
H: Univalence
HasPullbacks AbGroup
H: Univalence
forall (a b c : AbGroup) (f : a $-> c) (g : b $-> c),
Epic f -> Epic cat_pb_pr2
  1: exact _. (* By the above, [AbGroup] has pullbacks. *)
H: Univalence
forall (a b c : AbGroup) (f : a $-> c) (g : b $-> c),
Epic f -> Epic cat_pb_pr2
  (* We have to show that the categorical epimorphisms are stable under pullback. *)
  intros A B C f g ef.
H: Univalence
A, B, C: AbGroup
f: A $-> C
g: B $-> C
ef: Epic f
Epic cat_pb_pr2
  intros Z k1 k2.
H: Univalence
A, B, C: AbGroup
f: A $-> C
g: B $-> C
ef: Epic f
Z: AbGroup
k1, k2: B $-> Z
k1 $o cat_pb_pr2 $== k2 $o cat_pb_pr2 -> k1 $== k2
  (* Since surjections are epimorphisms in [Type], it's enough to show that the pulled back map is a surjection. *)
  rapply issurj_isepi_funext.
H: Univalence
A, B, C: AbGroup
f: A $-> C
g: B $-> C
ef: Epic f
Z: AbGroup
k1, k2: B $-> Z
IsConnMap (Tr (-1)) cat_pb_pr2
  (* Since surjections are stable under pullback, it's enough to show that [f] is a surjection. *)
  apply issurj_pullback_pr2.
H: Univalence
A, B, C: AbGroup
f: A $-> C
g: B $-> C
ef: Epic f
Z: AbGroup
k1, k2: B $-> Z
IsConnMap (Tr (-1)) f
  (* This follows from the fact the epimorphisms of abelian groups are surjections. *)
  by apply ab_issurj_epi.
Defined.

(** Combining [isepistable_abgroup] with [abenriched_abgroup] from AbHom.v gives: *)
Instance isabepistable_abgroup `{Univalence} : IsAbEpiStable AbGroup := {}.