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

The agda-unimath library

Lecture notes on univalent foundations of mathematics with Agda

Agda formalisation of the Introduction to Homotopy Type Theory

Formal Topology in Univalent Foundations (WIP).

Experiments with Realizability in Univalent Type Theory

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

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

My implementation of the HOTT/UF book