##### Haskell 101

- [Learn You a Haskell for Great Good: A Beginner's Guide (Miran Lipovača)](https://learnyouahaskell.com/)
- [Haskell - Wikibook](https://en.wikibooks.org/wiki/Haskell)

##### (Not Quick) Start

- [Modern dependent type theory (Lecture note spring 2024)](https://www.danielgratzer.com/courses/type-theory-s-2024/index.html)
- [Agda Tutorial (people.inf.elte.hu/divip)](https://people.inf.elte.hu/divip/AgdaTutorial/Index.html)
- [Introduction to Type Theory ([e-mail], 2008)](https://www.cs.ru.nl/~herman/onderwijs/provingwithCA/paper-lncs.pdf)
- [type theory (ncatlab.org)](https://ncatlab.org/nlab/show/type+theory)
- [Introduction to Univalent Foundations of Mathematics with Agda ([e-mail])](https://arxiv.org/abs/1911.00580)

##### Overviews

- [relation between type theory and category theory (ncatlab.org)](https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory)
- [Group-like structures (en.wikipedia.org)](https://en.wikipedia.org/wiki/Template:Group-like_structures)
- [Major topics in Foundations of Mathematics (en.wikipedia.org)](https://en.wikipedia.org/wiki/Template:Foundations-footer)

##### Type Theory

- [Homotopy Type Theory: Univalent Foundations of Mathematics (Univalent Foundations Program of IAS, 2013)](https://arxiv.org/abs/1308.0729)
- [The Lambda Calculus (plato.stanford.edu)](https://plato.stanford.edu/entries/lambda-calculus/)
- [Function Totality: Abstraction Tool in Programming (dimjasevic.net)](https://dimjasevic.net/marko/2018/11/20/function-totality-abstraction-tool-in-programming/)

##### *Uncategorized*

- [Structure and Interpretation of Computer Programs (mit.edu, 1996)](https://mitp-content-server.mit.edu/books/content/sectbyfn/books_pres_0/6515/sicp.zip/index.html)
- [Linear Logic (plato.stanford.edu)](https://plato.stanford.edu/entries/logic-linear/)
- [Object-oriented programming in dependent type theory([e-mail], 2006)](https://www.cs.nott.ac.uk/~psznhn/TFP2006/Papers/26-AntonSetzer-OOPInDependentTypeTheory.pdf)
- [What is Agda? — Agda 2.6.4.1 documentation](https://agda.readthedocs.io/en/v2.6.4.1/getting-started/what-is-agda.html)
- [Introductory books on Category Theory (Youtube video in Japanese)](https://youtu.be/AFZ-KC8zcEk)
- [Basic Category Theory (Tom Leinster, 2016)](https://arxiv.org/abs/1612.09375)
- Category Theory (Steve Awodey, 2010)
- Categories for the Working Mathematician (Saunders MacLane, 1971)
- [Category Theory in Context (Emily Riehl, 2014)](https://math.jhu.edu/~eriehl/context.pdf)

##### Links

- [Functional Thursday: FP Community in Taipei (youtube.com)](https://www.youtube.com/@thursdayfunctional9801)
- [FLOLAC (Formosan Summer School on Logic, Language, and Computation)](https://flolac.iis.sinica.edu.tw)
- [Kerodon: an online resource for homotopy-coherent mathematics (lurie@isa)](https://kerodon.net/)
- [nlab (ncatlab.org)](https://ncatlab.org/nlab/show/HomePage)

##### Authors' pages (Maybe useful)

- [Jacob Luries \<lurie@isa>](https://www.math.ias.edu/~lurie/)
- [Herman Geuvers \<[e-mail]>](http://cs.ru.nl/~herman/)

*This is a reading list created by a functional programming study circle that is also new to type theory.*