ext_cyclic_ab@{u v w | u < v, v < w} `{Univalence} (n : nat) `{emb : IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}} : ab_cokernel@{v w} (ab_mul (A:=A) n) $<~> ab_ext@{u v} (cyclic'@{u v} n) A. Proof. pose (E := abses_from_inclusion (Z1_mul_nat n)). snrefine (abses_cokernel_iso (ab_mul n) _). - exact (grp_homo_compose (abses_pushout_ext E) (grp_iso_inverse (equiv_Z1_hom A))). - apply (conn_map_compose _ (grp_iso_inverse (equiv_Z1_hom A))). 1: rapply conn_map_isequiv. exact (isconnmap_O_isexact_base_contr _ _ (fmap (pTr 0) (abses_pullback_pmap (A:=A) (projection E)))). - srapply isexact_homotopic_f. 1: exact (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n)) o* (pequiv_groupisomorphism (equiv_Z1_hom A))^-1*). 1: by apply phomotopy_homotopy_hset. apply ext_cyclic_exact. Defined.
Require Import Basics Types WildCat HSet Pointed.Core Pointed.pTrunc Pointed.pEquiv