Agda dependent types (Norell)

Layer 0 — Mathematicsin the Type Theory subtree

Agda based on Martin-Lof type theory; Norell 2007 thesis introduced unicode-friendly syntax + interactive editing; widely used for verified-functional-programming + HoTT formalization.