An experimental library for Cubical Agda

Development of homotopy type theory in Agda

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

An introductory course to Homotopy Type Theory

The agda-unimath library

Agda formalisation of the Introduction to Homotopy Type Theory

Cartesian Cubical Type Theory

A work-in-progress core language for Agda, in Agda

Differential cohesion in Homotopy Type Theory by an axiomatized infinitesimal shape modality

H.O.T.T. using rewriting in Agda

antifunext

Extensions to cubical for categorical logic/type theory

Mechanizations of Type Theories

An attempt towards univalent classical mathematics in Cubical Agda.

quotient types in cubical Agda

Solutions of the exercises of the HoTT book

Experiments with higher-order abstract syntax in Agda

Code for tutorials, papers and experiments. Mostly Agda, Coq and Haskell.

formalization of an equivariant cartesian cubical set model of type theory

Formalization of 2LTT in Agda

Simply-typed lambda calculus as a QIT in cubical Agda + normalization

An embedding of ZFC into Agda

My Agda blog/lab/playground

Semisimplicial types in Agda

Formalization of the James construction in Agda

Various attempts to model version control systems in Homotopy Type Theory

Formalization of 2LTT in Agda

Mechanized classifications of 2-groups

Formalizing the fact that countable choice implies postnikov effectiveness in HoTT