From HoTT Require Import Basics Types Truncations.Core.From HoTT Require Import Basics Types Truncations.Core.
From HoTT.WildCat Require Import Core Universe Opposite Bifunctor.
Require Import Pointed.Core Pointed.pTrunc.
Require Import Truncations.SeparatedTrunc.
Require Import AbelianGroup AbHom AbProjective.
Require Import AbSES.Pullback AbSES.Pushout AbSES.BaerSum AbSES.Core.

Local Open Scope mc_scope.
Local Open Scope mc_add_scope.

(** * The set [Ext B A] of abelian group extensions *)

Definition Ext (B A : AbGroup@{u}) := pTr 0 (AbSES B A).

Instance is0bifunctor_ext `{Univalence}
  : Is0Bifunctor (Ext : AbGroup^op -> AbGroup -> pType)
  := is0bifunctor_postcompose _ _ (bf:=is0bifunctor_abses).

Instance is1bifunctor_ext `{Univalence}
  : Is1Bifunctor (Ext : AbGroup^op -> AbGroup -> pType)
  := is1bifunctor_postcompose _ _ (bf:=is1bifunctor_abses).

(** An extension [E : AbSES B A] is trivial in [Ext B A] if and only if [E] merely splits. *)
Proposition iff_ab_ext_trivial_split `{Univalence} {B A : AbGroup} (E : AbSES B A)
  : merely {s : GroupHomomorphism B E & (projection _) $o s == idmap}
           <~> (tr E = point (Ext B A)).
H: Univalence
B, A: AbGroup
E: AbSES B A
merely {s : GroupHomomorphism B E & projection E $o s == idmap} <~>
tr E = point (Ext B A)
Proof.
H: Univalence
B, A: AbGroup
E: AbSES B A
merely {s : GroupHomomorphism B E & projection E $o s == idmap} <~>
tr E = point (Ext B A)
  refine (equiv_path_Tr _ _ oE _).
H: Univalence
B, A: AbGroup
E: AbSES B A
merely {s : GroupHomomorphism B E & projection E $o s == idmap} <~>
Tr (-1) (E = point (AbSES B A))
  srapply equiv_iff_hprop;
    apply Trunc_functor;
    apply iff_abses_trivial_split.
Defined.

Definition Ext' (B A : AbGroup@{u}) := Tr 0 (AbSES' B A).

Instance is0bifunctor_ext' `{Univalence}
  : Is0Bifunctor (Ext' : AbGroup^op -> AbGroup -> Type)
  := is0bifunctor_postcompose _ _ (bf:=is0bifunctor_abses').

Instance is1bifunctor_ext' `{Univalence}
  : Is1Bifunctor (Ext' : AbGroup^op -> AbGroup -> Type)
  := is1bifunctor_postcompose _ _ (bf:=is1bifunctor_abses').

(** [Ext B A] is an abelian group for any [A B : AbGroup]. The proof of commutativity is a bit faster if we separate out the proof that [Ext B A] is a group. *)
Definition grp_ext `{Univalence} (B A : AbGroup@{u}) : Group.
H: Univalence
B, A: AbGroup
Group
Proof.
H: Univalence
B, A: AbGroup
Group
  snapply (Build_Group (Ext B A)).
H: Univalence
B, A: AbGroup
SgOp (Ext B A)
H: Univalence
B, A: AbGroup
MonUnit (Ext B A)
H: Univalence
B, A: AbGroup
Inverse (Ext B A)
H: Univalence
B, A: AbGroup
IsGroup (Ext B A)
  -
H: Univalence
B, A: AbGroup
SgOp (Ext B A) intros E F.
H: Univalence
B, A: AbGroup
E, F: Ext B A
Ext B A
    strip_truncations.
H: Univalence
B, A: AbGroup
F, E: AbSES B A
Ext B A
    exact (tr (abses_baer_sum E F)).
  -
H: Univalence
B, A: AbGroup
MonUnit (Ext B A) exact (point (Ext B A)).
  -
H: Univalence
B, A: AbGroup
Inverse (Ext B A) unfold Inverse.
H: Univalence
B, A: AbGroup
Ext B A -> Ext B A
    exact (Trunc_functor _ (abses_pullback (- grp_homo_id))).
  -
H: Univalence
B, A: AbGroup
IsGroup (Ext B A) repeat split.
H: Univalence
B, A: AbGroup
IsHSet (Ext B A)
H: Univalence
B, A: AbGroup
Associative sg_op
H: Univalence
B, A: AbGroup
LeftIdentity sg_op 0
H: Univalence
B, A: AbGroup
RightIdentity sg_op 0
H: Univalence
B, A: AbGroup
LeftInverse sg_op inv 0
H: Univalence
B, A: AbGroup
RightInverse sg_op inv 0
    1: apply istrunc_truncation.
H: Univalence
B, A: AbGroup
Associative sg_op
H: Univalence
B, A: AbGroup
LeftIdentity sg_op 0
H: Univalence
B, A: AbGroup
RightIdentity sg_op 0
H: Univalence
B, A: AbGroup
LeftInverse sg_op inv 0
H: Univalence
B, A: AbGroup
RightInverse sg_op inv 0
    all: intro E.
H: Univalence
B, A: AbGroup
E: Ext B A
forall y z : Ext B A, E + (y + z) = E + y + z
H: Univalence
B, A: AbGroup
E: Ext B A
0 + E = E
H: Univalence
B, A: AbGroup
E: Ext B A
E + 0 = E
H: Univalence
B, A: AbGroup
E: Ext B A
- E + E = 0
H: Univalence
B, A: AbGroup
E: Ext B A
E - E = 0  1: intros F G.
H: Univalence
B, A: AbGroup
E, F, G: Ext B A
E + (F + G) = E + F + G
H: Univalence
B, A: AbGroup
E: Ext B A
0 + E = E
H: Univalence
B, A: AbGroup
E: Ext B A
E + 0 = E
H: Univalence
B, A: AbGroup
E: Ext B A
- E + E = 0
H: Univalence
B, A: AbGroup
E: Ext B A
E - E = 0
    all: strip_truncations; unfold mon_unit, point; apply (ap tr).
H: Univalence
B, A: AbGroup
G, F, E: AbSES B A
abses_baer_sum E (abses_baer_sum F G) = abses_baer_sum (abses_baer_sum E F) G
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum (point (AbSES B A)) E = E
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum E (point (AbSES B A)) = E
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum (abses_pullback (- grp_homo_id) E) E = point (AbSES B A)
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum E (abses_pullback (- grp_homo_id) E) = point (AbSES B A)
    +
H: Univalence
B, A: AbGroup
G, F, E: AbSES B A
abses_baer_sum E (abses_baer_sum F G) = abses_baer_sum (abses_baer_sum E F) G symmetry; apply baer_sum_associative.
    +
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum (point (AbSES B A)) E = E apply baer_sum_unit_l.
    +
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum E (point (AbSES B A)) = E apply baer_sum_unit_r.
    +
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum (abses_pullback (- grp_homo_id) E) E = point (AbSES B A) apply baer_sum_inverse_r.
    +
H: Univalence
B, A: AbGroup
E: AbSES B A
abses_baer_sum E (abses_pullback (- grp_homo_id) E) = point (AbSES B A) apply baer_sum_inverse_l.
Defined.

(** ** The bifunctor [ab_ext] *)

Definition ab_ext@{u v|u < v} `{Univalence} (B : AbGroup@{u}^op) (A : AbGroup@{u}) : AbGroup@{v}.
H: Univalence
B: AbGroup^op
A: AbGroup
AbGroup
Proof.
H: Univalence
B: AbGroup^op
A: AbGroup
AbGroup
  snapply (Build_AbGroup (grp_ext@{u v} B A)).
H: Univalence
B: AbGroup^op
A: AbGroup
Commutative sg_op
  intros E F.
H: Univalence
B: AbGroup^op
A: AbGroup
E, F: grp_ext B A
E + F = F + E
  strip_truncations; cbn.
H: Univalence
B: AbGroup^op
A: AbGroup
F, E: AbSES B A
tr (abses_baer_sum E F) = tr (abses_baer_sum F E)
  apply ap.
H: Univalence
B: AbGroup^op
A: AbGroup
F, E: AbSES B A
abses_baer_sum E F = abses_baer_sum F E
  apply baer_sum_commutative.
Defined.

Instance is0functor_abext01 `{Univalence} (B : AbGroup^op)
  : Is0Functor (ab_ext B).
H: Univalence
B: AbGroup^op
Is0Functor (ab_ext B)
Proof.
H: Univalence
B: AbGroup^op
Is0Functor (ab_ext B)
  srapply Build_Is0Functor; intros ? ? f.
H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
ab_ext B a $-> ab_ext B b
  snapply Build_GroupHomomorphism.
H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
ab_ext B a -> ab_ext B b
H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fmap (Ext B) f).
H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
IsSemiGroupPreserving (fmap (pTr 0 o AbSES B) f)
  rapply Trunc_ind; intro E0.
H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
E0: AbSES B a
forall y : ab_ext B a,
fmap (pTr 0 o AbSES B) f (tr E0 + y) =
fmap (pTr 0 o AbSES B) f (tr E0) + fmap (pTr 0 o AbSES B) f y
  rapply Trunc_ind; intro E1.
H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
E0, E1: AbSES B a
fmap (pTr 0 o AbSES B) f (tr E0 + tr E1) =
fmap (pTr 0 o AbSES B) f (tr E0) + fmap (pTr 0 o AbSES B) f (tr E1)
  apply (ap tr); cbn.
H: Univalence
B: AbGroup^op
a, b: AbGroup
f: a $-> b
E0, E1: AbSES B a
abses_pushout f (abses_baer_sum E0 E1) =
abses_baer_sum (abses_pushout f E0) (abses_pushout f E1)
  apply baer_sum_pushout.
Defined.

Instance is0functor_abext10 `{Univalence} (A : AbGroup)
  : Is0Functor (fun B : AbGroup^op => ab_ext B A).
H: Univalence
A: AbGroup
Is0Functor (fun B : AbGroup^op => ab_ext B A)
Proof.
H: Univalence
A: AbGroup
Is0Functor (fun B : AbGroup^op => ab_ext B A)
  srapply Build_Is0Functor; intros ? ? f; cbn.
H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
GroupHomomorphism (grp_ext a A) (grp_ext b A)
  snapply Build_GroupHomomorphism.
H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
grp_ext a A -> grp_ext b A
H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fmap (fun (B : AbGroup^op) => Ext B A) f).
H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
IsSemiGroupPreserving (fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f)
  rapply Trunc_ind; intro E0.
H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
E0: AbSES a A
forall y : grp_ext a A,
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f (tr E0 + y) =
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f (tr E0) +
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f y
  rapply Trunc_ind; intro E1.
H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
E0, E1: AbSES a A
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f (tr E0 + tr E1) =
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f (tr E0) +
fmap (pTr 0 o (fun x : AbGroup^op => AbSES x A)) f (tr E1)
  apply (ap tr); cbn.
H: Univalence
A: AbGroup
a, b: AbGroup^op
f: a $-> b
E0, E1: AbSES a A
abses_pullback f (abses_baer_sum E0 E1) =
abses_baer_sum (abses_pullback f E0) (abses_pullback f E1)
  apply baer_sum_pullback.
Defined.

Instance is1functor_abext01 `{Univalence} (B : AbGroup^op)
  : Is1Functor (ab_ext B).
H: Univalence
B: AbGroup^op
Is1Functor (ab_ext B)
Proof.
H: Univalence
B: AbGroup^op
Is1Functor (ab_ext B)
  snapply Build_Is1Functor.
H: Univalence
B: AbGroup^op
forall (a b : AbGroup) (f g : a $-> b),
f $== g -> fmap (ab_ext B) f $== fmap (ab_ext B) g
H: Univalence
B: AbGroup^op
forall a : AbGroup, fmap (ab_ext B) (Id a) $== Id (ab_ext B a)
H: Univalence
B: AbGroup^op
forall (a b c : AbGroup) (f : a $-> b) (g : b $-> c),
fmap (ab_ext B) (g $o f) $== fmap (ab_ext B) g $o fmap (ab_ext B) f
  -
H: Univalence
B: AbGroup^op
forall (a b : AbGroup) (f g : a $-> b),
f $== g -> fmap (ab_ext B) f $== fmap (ab_ext B) g intros A C f g.
H: Univalence
B: AbGroup^op
A, C: AbGroup
f, g: A $-> C
f $== g -> fmap (ab_ext B) f $== fmap (ab_ext B) g
    exact (fmap2 (Ext B)).
  -
H: Univalence
B: AbGroup^op
forall a : AbGroup, fmap (ab_ext B) (Id a) $== Id (ab_ext B a) exact (fmap_id (Ext B)).
  -
H: Univalence
B: AbGroup^op
forall (a b c : AbGroup) (f : a $-> b) (g : b $-> c),
fmap (ab_ext B) (g $o f) $== fmap (ab_ext B) g $o fmap (ab_ext B) f intros A C D.
H: Univalence
B: AbGroup^op
A, C, D: AbGroup
forall (f : A $-> C) (g : C $-> D),
fmap (ab_ext B) (g $o f) $== fmap (ab_ext B) g $o fmap (ab_ext B) f
    exact (fmap_comp (Ext B)).
Defined.

Instance is1functor_abext10 `{Univalence} (A : AbGroup)
  : Is1Functor (fun B : AbGroup^op => ab_ext B A).
H: Univalence
A: AbGroup
Is1Functor (fun B : AbGroup^op => ab_ext B A)
Proof.
H: Univalence
A: AbGroup
Is1Functor (fun B : AbGroup^op => ab_ext B A)
  snapply Build_Is1Functor.
H: Univalence
A: AbGroup
forall (a b : AbGroup^op) (f g : a $-> b),
f $== g ->
fmap (fun B : AbGroup^op => ab_ext B A) f $==
fmap (fun B : AbGroup^op => ab_ext B A) g
H: Univalence
A: AbGroup
forall a : AbGroup^op,
fmap (fun B : AbGroup^op => ab_ext B A) (Id a) $==
Id ((fun B : AbGroup^op => ab_ext B A) a)
H: Univalence
A: AbGroup
forall (a b c : AbGroup^op) (f : a $-> b) (g : b $-> c),
fmap (fun B : AbGroup^op => ab_ext B A) (g $o f) $==
fmap (fun B : AbGroup^op => ab_ext B A) g $o
fmap (fun B : AbGroup^op => ab_ext B A) f
  -
H: Univalence
A: AbGroup
forall (a b : AbGroup^op) (f g : a $-> b),
f $== g ->
fmap (fun B : AbGroup^op => ab_ext B A) f $==
fmap (fun B : AbGroup^op => ab_ext B A) g intros B C f g.
H: Univalence
A: AbGroup
B, C: AbGroup^op
f, g: B $-> C
f $== g ->
fmap (fun B0 : AbGroup^op => ab_ext B0 A) f $==
fmap (fun B0 : AbGroup^op => ab_ext B0 A) g
    exact (fmap2 (fun B : AbGroup^op => Ext B A)).
  -
H: Univalence
A: AbGroup
forall a : AbGroup^op,
fmap (fun B : AbGroup^op => ab_ext B A) (Id a) $==
Id ((fun B : AbGroup^op => ab_ext B A) a) exact (fmap_id (fun B : AbGroup^op => Ext B A)).
  -
H: Univalence
A: AbGroup
forall (a b c : AbGroup^op) (f : a $-> b) (g : b $-> c),
fmap (fun B : AbGroup^op => ab_ext B A) (g $o f) $==
fmap (fun B : AbGroup^op => ab_ext B A) g $o
fmap (fun B : AbGroup^op => ab_ext B A) f intros B C D.
H: Univalence
A: AbGroup
B, C, D: AbGroup^op
forall (f : B $-> C) (g : C $-> D),
fmap (fun B0 : AbGroup^op => ab_ext B0 A) (g $o f) $==
fmap (fun B0 : AbGroup^op => ab_ext B0 A) g $o
fmap (fun B0 : AbGroup^op => ab_ext B0 A) f
    exact (fmap_comp (fun B : AbGroup^op => Ext B A)).
Defined.

Instance is0bifunctor_abext `{Univalence}
  : Is0Bifunctor (A:=AbGroup^op) ab_ext
  := Build_Is0Bifunctor'' _.

Instance is1bifunctor_abext `{Univalence}
  : Is1Bifunctor (A:=AbGroup^op) ab_ext.
H: Univalence
Is1Bifunctor ab_ext
Proof.
H: Univalence
Is1Bifunctor ab_ext
  snapply Build_Is1Bifunctor''.
H: Univalence
forall a : AbGroup^op, Is1Functor (ab_ext a)
H: Univalence
forall b : AbGroup, Is1Functor (flip ab_ext b)
H: Univalence
forall (a0 a1 : AbGroup^op) (f : a0 $-> a1) (b0 b1 : AbGroup)
(g : b0 $-> b1),
fmap01 ab_ext a1 g $o fmap10 ab_ext f b0 $==
fmap10 ab_ext f b1 $o fmap01 ab_ext a0 g
  1,2: exact _.
H: Univalence
forall (a0 a1 : AbGroup^op) (f : a0 $-> a1) (b0 b1 : AbGroup)
(g : b0 $-> b1),
fmap01 ab_ext a1 g $o fmap10 ab_ext f b0 $==
fmap10 ab_ext f b1 $o fmap01 ab_ext a0 g
  intros A B.
H: Univalence
A, B: AbGroup^op
forall (f : A $-> B) (b0 b1 : AbGroup) (g : b0 $-> b1),
fmap01 ab_ext B g $o fmap10 ab_ext f b0 $==
fmap10 ab_ext f b1 $o fmap01 ab_ext A g
  exact (bifunctor_coh (Ext : AbGroup^op -> AbGroup -> pType)).
Defined.

(** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)
Definition abses_pushout_ext `{Univalence}
  {B A G : AbGroup@{u}} (E : AbSES B A)
  : GroupHomomorphism (ab_hom A G) (ab_ext B G).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
GroupHomomorphism (ab_hom A G) (ab_ext B G)
Proof.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
GroupHomomorphism (ab_hom A G) (ab_ext B G)
  snapply Build_GroupHomomorphism.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
ab_hom A G -> ab_ext B G
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fun f => fmap01 (A:=AbGroup^op) Ext' _ f (tr E)).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
IsSemiGroupPreserving (fun f : ab_hom A G => fmap01 Ext' B f (tr E))
  intros f g; cbn.
H: Univalence
B, A, G: AbGroup
E: AbSES B A
f, g: ab_hom A G
tr (abses_pushout (sgop_hom f g) E) =
tr (abses_baer_sum (abses_pushout f E) (abses_pushout g E))
  napply (ap tr).
H: Univalence
B, A, G: AbGroup
E: AbSES B A
f, g: ab_hom A G
abses_pushout (sgop_hom f g) E =
abses_baer_sum (abses_pushout f E) (abses_pushout g E)
  exact (baer_sum_distributive_pushouts f g).
Defined.

(** ** Extensions ending in a projective are trivial *)

Proposition abext_trivial_projective `{Univalence}
  (P : AbGroup) `{IsAbProjective P}
  : forall A, forall E : AbSES P A, tr E = point (Ext P A).
H: Univalence
P: AbGroup
H0: IsAbProjective P
forall (A : AbGroup) (E : AbSES P A), tr E = point (Ext P A)
Proof.
H: Univalence
P: AbGroup
H0: IsAbProjective P
forall (A : AbGroup) (E : AbSES P A), tr E = point (Ext P A)
  intros A E.
H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
E: AbSES P A
tr E = point (Ext P A)
  apply iff_ab_ext_trivial_split.
H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
E: AbSES P A
merely {s : GroupHomomorphism P E & projection E $o s == idmap}
  exact (fst (iff_isabprojective_surjections_split P) _ _ _ _).
Defined.

(** It follows that when [P] is projective, [Ext P A] is contractible. *)
Instance contr_abext_projective `{Univalence}
  (P : AbGroup) `{IsAbProjective P} {A : AbGroup}
  : Contr (Ext P A).
H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
Contr (Ext P A)
Proof.
H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
Contr (Ext P A)
  apply (Build_Contr _ (point _)); intro E.
H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
E: Ext P A
point (Ext P A) = E
  strip_truncations.
H: Univalence
P: AbGroup
H0: IsAbProjective P
A: AbGroup
E: AbSES P A
point (Ext P A) = tr E
  symmetry; by apply abext_trivial_projective.
Defined.

(* Conversely, if all extensions ending in [P] are trivial, then [P] is projective. *)
Proposition abext_projective_trivial `{Univalence} (P : AbGroup)
  (ext_triv : forall A, forall E : AbSES P A, tr E = point (Ext P A))
  : IsAbProjective P.
H: Univalence
P: AbGroup
ext_triv: forall (A : AbGroup) (E : AbSES P A), tr E = point (Ext P A)
IsAbProjective P
Proof.
H: Univalence
P: AbGroup
ext_triv: forall (A : AbGroup) (E : AbSES P A), tr E = point (Ext P A)
IsAbProjective P
  apply iff_isabprojective_surjections_split.
H: Univalence
P: AbGroup
ext_triv: forall (A : AbGroup) (E : AbSES P A), tr E = point (Ext P A)
forall (A : AbGroup) (p : A $-> P),
ReflectiveSubuniverse.IsConnMap (Tr (-1)) p ->
merely {s : P $-> A & p $o s == grp_homo_id}
  intros E p issurj_p.
H: Univalence
P: AbGroup
ext_triv: forall (A : AbGroup) (E0 : AbSES P A), tr E0 = point (Ext P A)
E: AbGroup
p: E $-> P
issurj_p: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
merely {s : P $-> E & p $o s == grp_homo_id}
  apply (iff_ab_ext_trivial_split (abses_from_surjection p))^-1.
H: Univalence
P: AbGroup
ext_triv: forall (A : AbGroup) (E0 : AbSES P A), tr E0 = point (Ext P A)
E: AbGroup
p: E $-> P
issurj_p: ReflectiveSubuniverse.IsConnMap (Tr (-1)) p
tr (abses_from_surjection p) = point (Ext P (ab_kernel p))
  apply ext_triv.
Defined.