Mature library for HoTT: https://unimath.github.io/agda-unimath/
Rest are my naive attempts, as I understand mathematics by writing code :)
Notes in Agda about
- Homotopy Type Theory (based on
- Introduction to Univalent Foundations of Mathematics with Agda by Martín Hötzel Escardó, (arxiv 1911.00580),
- Introduction to Homotopy Type Theory by Egbert Rijke,
- HoTTEST Summer School 2022 (Agda), (lectures & exercises), (videos), (GH),
- Homotopy type theory by Andrej Bauer (videos),
- Math 721: Homotopy Type Theory by Emily Riehl)
- Category Theory (based on
- CS410 Advanced Functional Programming at the University of Strathclyde by Conor McBride (videos), (GH repo with code), (lecture notes), (GH 2018),
- agda-categories)
- Patterns of Functional Programming (inspired by category theory that can be found in Haskell, Scala, PureScript, Idris)
Patters of FP can be seen as continuation of scala_typeclassopedia - this time in Agda).
Section zio-prelude aims at formally verifying encoding from Scala library zio-prelude (that improve usuall encoding of FP abstractions e.g. by adding Zivariant, introducing novel definitions like ZRerf that is a generalization of optics).
Category theory definitions are strict - use equality (agda-categories are parametrized by equivalence relation).