{A E B X F Y : AbGroup} (i : A $-> E) (p : E $-> B) `{ex0 : IsExact (Tr (-1)) _ _ _ i p} (j : X $-> F) (q : F $-> Y) `{ex1 : IsExact (Tr (-1)) _ _ _ j q} : IsExact (Tr (-1)) (functor_ab_biprod i j) (functor_ab_biprod p q). Proof. snrapply Build_IsExact. - snrapply phomotopy_homotopy_hset. 1: exact _. intro x; apply path_prod; cbn. + apply ex0. + apply ex1. - intros [[e f] u]; cbn. rapply contr_inhabited_hprop. pose (U := (equiv_path_prod _ _)^-1 u); cbn in U. pose proof (a := isexact_preimage _ i p e (fst U)). pose proof (x := isexact_preimage _ j q f (snd U)). strip_truncations; apply tr. exists (ab_biprod_inl a.1 + ab_biprod_inr x.1); cbn. pose (IS := sg_set (ab_biprod B Y)). apply path_sigma_hprop; cbn. apply path_prod; cbn. + rewrite right_identity. exact a.2. + rewrite left_identity. exact x.2. Defined.
Require Import Basics Types Truncations.Core. Require Import Pointed.Core. Require Import WildCat.Core Homotopy.ExactSequence. Require Import AbGroups.AbelianGroup AbSES.Core AbGroups.Biproduct.