Spectral sequences about coq-hott

[jdchristensen]

Interesting idea. I haven't tried to formalize anything about spectral sequences, so I don't know what the best approach is.

One minor comment about:

I also observed an interesting fact that such a shift functor would give A the structure of a triangulated category.

Abelian categories are very rarely triangulated, so this won't be true in general. (There's a lemma due to Verdier, stated at https://math.stackexchange.com/questions/189769/when-is-the-derived-category-abelian, which characterizes triangulated categories that are also abelian.)

[jdchristensen]

Just to add a bit more, in a triangulated category, every epimorphism has a section and every monomorphism has a retraction.

[Alizter]

I see where I was confused about the triangulated category. I was thinking about chain complexes in an abelian category forming a triangulated category with distinguished triangles given by exact sequences. This is however not at all true! The example I was misremembering was the homotopy category of chain complexes where you localize the quasiisomorphsims. Anyway, thanks for the correction. Let's drop this silly example from the discussion.

[Alizter]

Interesting idea. I haven't tried to formalize anything about spectral sequences, so I don't know what the best approach is.

One thing I learnt from Floris' attempt at formalising Serre spectral sequence is that the bureaucracy of integer arithmetic can get very heavy. I believe this is what motivated him to introduce successor structures.

[mikeshulman]

The definition using automorphisms $T_r$ does seem likely to lend itself well to a successor-structures version.

Another thing I've wondered about is whether, in this and other cases where the bureaucracy of integer arithmetic gets heavy, it could be improved by using a relational rather than functional definition of arithmetic. E.g. addition is

Inductive plus : nat -> nat -> nat -> Type :=
| plus_O : forall {n : nat}, plus n O n
| plus_S : forall {m n mn : nat}, plus m n mn -> plus m (S n) (S mn).

One advantage of this is that associativity can be phrased without any equalities: it says that if plus m n mn and plus mn p mnp and plus n p np, then also plus m np mnp. So there is no transport, but the cost of course is carrying around witnesses of plus in various places.

The reason this occurred to me is that I've recently been using this idiom a lot with type-level natural numbers in OCaml (for intrinsically well-scoped De Bruijn indices), where it is the only possibility since you can't define recursive functions on types, and I've been impressed by how cleanly things generally work out.