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

Learn pure math with agda 🚀

Logical manifestations of topological concepts, and other things, via the univalent point of view.

A Coq library for Homotopy Type Theory

An experimental proof assistant based on a type theory for synthetic ∞-categories.

The agda-unimath library

Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda

Personal research notes

Ground Zero: Lean 4 HoTT Library

🧊 An indexed construction of semi-simplicial and semi-cubical types

🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory

Experimental implementation of a Cubical Type Theory modeled by presheaves over posets

Experiments with Cubical Agda

Generated deloopings in Agda.

WIP: Reedy fibrant diagrams in models of type theory

Lecture notes on univalent foundations of mathematics with Agda

I'm learning a Functional Programming by learning its pure math concepts and apply it on functional language like Haskell, Clojure, Elixir, etc.

Agda files used for a survey paper on Homotopy Type Theory

Trace monoids in Cubical Agda

Write function for one data type, let it work with all sorts of variations of it