This is a repository of Cubical Agda code to accompany the paper
A computer formalisation of the Serre finiteness theorem Reid Barton, Axel Ljungström, Owen Milner, Anders Mörtberg
Checked against the agda/cubical library (commit d0b9c7b0e9e4f816422c3447d7983b03274dd829, Wed May 13 2026) using Agda 2.8.0