Foundations

The series of notes about MLTT and Foundations.

10 OCT 2016 — Pure Type System
3 AUG 2017 — Mathematical Components
19 OCT 2017 — Recursion Schemes

Homotopy Theory

The series of notes on Homotopy Type Theory.

10 OCT 2017 — Isomorphism
30 DEC 2018 — Equivalence
20 JUN 2017 — Hopf Fibrations

Base Library

The examples of base library man pages.

16 JUL 2017 — Pi
5 NOV 2017 — Category
20 MAY 2018 — Bundle
25 JUL 2018 — Path
25 JUL 2018 — CW Complex
22 JAN 2019 — Homology

Articles

The series of articles on foundation and mathematics of Homotopy Type Theory.

Issue I: Internalizing MLTT
Issue III: Homotopy Type Theory
Issue VIII: Formal Set Topos
Addendum I: Pure Type System
Addendum II: Many Faces of Equality