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)
- Functional Programming (abstractions from category theory used in Haskell, Scala, PureScript, Idris)
Abstractions in FP can be seen as continuation of scala_typeclassopedia - this time in Agda :)
src/FP/zio-prelude aims at formally verifying encoding from Scala library zio-prelude (that improve usual 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).
If you are nix user you can get shell with recent Agda by running:
nix develop