##### https://github.com/jarlg/Yoneda-Ext
Tip revision: 0d8bfe8
Lemmas.v
``````From HoTT Require Import Basics Types Pointed WildCat
ExactSequence AbGroups AbSES.

(* Place in Homotopy.ExactSequence. *)
Definition isexact_homotopic_if n {F X Y : pType}
{i i' : F ->* X} (h : i' ==* i)
{f f' : X ->* Y} (k : f' ==* f)
`{IsExact n F X Y i f}
: IsExact n i' f'.
Proof.
refine (isexact_homotopic_i n h _).
exact (isexact_homotopic_f n _ k).
Defined.

(* Place in AbSES.Pullback. *)
Definition abses_pullback_trivial_factors_projection `{Univalence}
{B B' A : AbGroup} {g : B' \$-> B} {E : AbSES B A}
: pt = abses_pullback g E -> exists phi, g = projection E \$o phi.
Proof.
equiv_intros (equiv_path_abses (E:=pt) (F:=abses_pullback g E)) p.
destruct p as [phi [p q]].
exists (grp_pullback_pr1 _ _ \$o phi \$o ab_biprod_inr).
apply equiv_path_grouphomomorphism; intro b'; symmetry.
refine (right_square (abses_pullback_morphism E g) _ @ _).
exact (ap g (q _)^).
Defined.

(** ** [loops_abses] is a group isomorphism *)

(** The functorial action of [abses_pullback_pmap] on loops. *)
Definition abses_loops_pullback_data `{Univalence} {B B' A : AbGroup} (g : B \$-> B')
: forall p, fmap loops (abses_pullback_pmap (A:=A) g) p
= equiv_path_abses_iso
((abses_pullback_point' g)^\$
\$@ (fmap (abses_pullback g) (equiv_path_abses_iso^-1 p)
\$@ abses_pullback_point' g)).
Proof.
intro p.
refine (_ @ abses_path_data_compose_beta _ _).
refine (_ @ ap011 _ (abses_path_data_V _) (abses_path_data_compose_beta _ _)).
apply whiskerL.
apply whiskerR.
apply ap_abses_pullback.
Defined.

(** Loop spaces of a 1-truncated type are automatically groups. *)
Definition loops_1trunc (X : pType) `{IsTrunc 1 X} : Group.
Proof.
nrefine (Build_Group (loops X) concat idpath inverse _).
nrapply Build_IsGroup; repeat split.
- by apply istrunc_paths.
- rapply concat_p_pp.
- rapply concat_1p.
- rapply concat_p1.
- rapply concat_Vp.
- rapply concat_pV.
Defined.

Definition iso_loops_abses `{Univalence} {A B : AbGroup}
: GroupIsomorphism (ab_hom B A)
(loops_1trunc (AbSES B A)).
Proof.
srapply Build_GroupIsomorphism'.
1: apply loops_abses.
intros phi psi.
snrapply (equiv_ap_inv' equiv_path_abses).
apply path_sigma_hprop.
apply equiv_path_grouphomomorphism; intros [a b].
unfold loops_abses.
rewrite (eissect equiv_path_abses (abses_endomorphism_trivial^-1 (sg_op phi psi))).
unfold equiv_path_abses.
nrefine (_ @ ap (fun x => (equiv_path_abses^-1 x).1 _) _).
2: exact (abses_path_data_compose_beta _ _)^.
rewrite (equiv_inverse_compose _ _ _).
nrefine (_ @ ap (fun x => ((equiv_path_abses_data _ _)^-1 x).1 _) _^).
2: apply eissect.
cbn.
apply path_prod'.
- rewrite grp_unit_l.
apply associativity.
- exact (grp_unit_l _)^.
Defined.

(** The inverse of [loops_abses]. *)
Definition loops_abses_inv `{Univalence} {A B : AbGroup}
: loops (AbSES B A) <~> (B \$-> A)
:= abses_endomorphism_trivial oE equiv_path_abses^-1.

(** Under the equivalence [loops_abses], [fmap loops (abses_pullback g)] corresponds to precomposition by [g]. It's easiest to show this using [loops_abses_inv]. *)
Definition abses_loops_pullback_inv `{Univalence} {B B' A : AbGroup} (g : B \$-> B')
: Square (IsGraph0:=isgraph_type) loops_abses_inv loops_abses_inv
(fmap loops (abses_pullback_pmap (A:=A) g)) (fun f => f \$o g).
Proof.
intro phi; unfold loops_abses_inv.
refine (ap abses_endomorphism_trivial _
(x:=equiv_path_abses^-1%equiv (fmap loops _ phi))
@ _).
{ refine (ap _ (abses_loops_pullback_data _ _) @ _).
refine (equiv_inverse_compose _ _ _ @ _).
exact (ap _ (eissect _ _)). }
by apply equiv_path_grouphomomorphism.
Defined.

Definition abses_loops_pullback `{Univalence} {B B' A : AbGroup} (g : B \$-> B')
: Square (IsGraph0:=isgraph_type) loops_abses loops_abses
(fun f => f \$o g) (fmap loops (abses_pullback_pmap (A:=A) g)).
Proof.
intro phi.
rapply moveR_equiv_M'.
nrefine (_ @ (abses_loops_pullback_inv g (loops_abses phi))^).
refine (ap (fun f => f \$o g) (x:=phi) _^).
unfold loops_abses_inv, loops_abses.
refine (ap _ (eissect equiv_path_abses _) @ _).
apply eisretr.
Defined.
``````