Georg Struth, Tanguy Massacrier: Cubical Categories. Arch. Formal Proofs 2024 (2024)