Links

• ​Learn you an Agda​

• ​Agda Standard Library​

• ​Introductions to Agda​

• ​Category Theory in Agda - Learning exercise.

• ​Categories - Categories parametrized by morphism equality, in Agda.

• ​Programming Language Foundations in Agda (2018)​

• ​(n,r)-categories in agda​

• ​Higher-Order Pattern Unification in Agda​

• ​Experimental library for Cubical Agda​

• ​Functional Reactive Programming with Agda​

• ​Agda standard library​

• ​Introduction to Agda (2011) - Daniel Peebles' Introduction to Agda, presented at Boston Haskell.

• ​Programming with Dependent Types Summer School​

• ​Agda Prelude - Alternative to the Agda standard library that focuses more on programming and type checking time performance.