My undergradate thesis on coinductive types in univalent type theory
-
Updated
May 10, 2018 - TeX
My undergradate thesis on coinductive types in univalent type theory
Formalized Mathematics
My implementation of the HOTT/UF book
Castle Bravo: Experimental HoTT Implementation
Experiments with Realizability in Univalent Type Theory
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Formal Topology in Univalent Foundations (WIP).
Agda formalisation of the Introduction to Homotopy Type Theory
Lecture notes on univalent foundations of mathematics with Agda
Logical manifestations of topological concepts, and other things, via the univalent point of view.
The agda-unimath library
Experimental implementation of Cubical Type Theory
A Coq library for Homotopy Type Theory
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."