Formalized Mathematics
-
Updated
Nov 9, 2017 - Coq
Formalized Mathematics
My undergradate thesis on coinductive types in univalent type theory
Agda formalisation of the Introduction to Homotopy Type Theory
Formal Topology in Univalent Foundations (WIP).
My implementation of the HOTT/UF book
Castle Bravo: Experimental HoTT Implementation
Experimental implementation of Cubical Type Theory
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Lecture notes on univalent foundations of mathematics with Agda
Experiments with Realizability in Univalent Type Theory
A Coq library for Homotopy Type Theory
Logical manifestations of topological concepts, and other things, via the univalent point of view.
The agda-unimath library
Add a description, image, and links to the univalent-foundations topic page so that developers can more easily learn about it.
To associate your repository with the univalent-foundations topic, visit your repo's landing page and select "manage topics."