miller. Miller/pattern unification in Agda
69cubical-demo. Agda
45parametric-demo. Agda
12hottest-talk. Agda
7hereditary. Hereditary Substitution
5cat. Formalizing Category Theory in Agda using Cubical Type Theory
3ITT9200. ITT9200 - A reading group on "Syntax and Semantics of Dependent Types" by Martin Hofmann
1guarded-exp. Experiments with models of "guarded recursion"
1