`{Univalence} {B A G : AbGroup} (E : AbSES B A) (F : AbSES B G) (p : abses_pullback (projection E) F = pt) : AbSESMorphism E F. Proof. pose (p' := equiv_path_abses^-1 p^); destruct p' as [p' [pl pr]]. srefine (Build_AbSESMorphism _ _ grp_homo_id _ _). - refine (grp_homo_compose (grp_iso_inverse (abses_kernel_iso (inclusion F) (projection F))) _). snrapply grp_kernel_corec. 1: exact (grp_pullback_pr1 _ _ $o p' $o ab_biprod_inr $o inclusion E). intro x. refine (right_square (abses_pullback_morphism F _) _ @ _). refine (ap (projection E) (pr _)^ @ _); cbn. apply isexact_inclusion_projection. - exact (grp_pullback_pr1 _ _ $o p' $o ab_biprod_inr). - intro a. nrapply abses_kernel_iso_inv_beta. - intro e. refine (right_square (abses_pullback_morphism F _) _ @ ap (projection E) _). exact (pr _)^. Defined.
Require Import Basics Types WildCat HSet Pointed.Core Pointed.pTrunc Pointed.pEquiv