Homological algebra lemmas about coq-hott

[jdchristensen]

Can you give a reference for how the short 5-lemma + regularity is enough to get all the other standard homological results?

Also, is it really true that pType will satisfy this? How do you define exactness in that generality? E.g. I have sequences

   1 → 2 → 2

and

   1 → 3 → 2

where in both cases the second map sends the base point to the base point and the other point(s) to the non-base point in 2. In both cases, the preimage of the base point agrees with the image of the previous map. Are both sequences exact? There's a map from the second to the first that isn't an equivalence in the middle.

[Alizter]

@jdchristensen I think i misremembered pType. I believe it might work for connected spaces however.

[Alizter]

Can you give a reference for how the short 5-lemma + regularity is enough to get all the other standard homological results?

In Borceux's book "Mal'cev, Protomodular, Homological and Semi-Abelian Categories" a "homological category is defined as a pointed regular protomodular category (4.1.1). Theorem 4.1.10 states that a pointed regular category is homological iff the short 5-lemma holds.

Here is Bergman's Salamander Lemma which is general enough to produce most other homological lemmas. Here is a slick proof by Jonathan Wise that avoids talking about elements.

Now the five lemma, snake lemma and nine lemma are all proven in Borceux's book, so I don't think it would be a huge stretch to prove the salamander lemma and derive the rest from that. This is a bit flaky as I haven't actually checked it and there is a chance there might be some property of abelian categories that remains essential.