univalent-foundations
There are 14 repositories under univalent-foundations topic.
HoTT/Coq-HoTT
A Coq library for Homotopy Type Theory
mortberg/cubicaltt
Experimental implementation of Cubical Type Theory
martinescardo/TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
UniMath/agda-unimath
The agda-unimath library
martinescardo/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
HoTT-Intro/Agda
Agda formalisation of the Introduction to Homotopy Type Theory
ayberkt/formal-topology-in-UF
Formal Topology in Univalent Foundations (WIP).
langston-barrett/reed-thesis
My undergradate thesis on coinductive types in univalent type theory
rahulc29/realizability
Experiments with Realizability in Univalent Type Theory
forked-from-1kasper/bravo
Castle Bravo: Experimental HoTT Implementation
lane-core/kitcat
Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda
amato-gianluca/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
AnthonyBordg/UniLab
Formalized Mathematics
amato-gianluca/MyHOTT
My implementation of the HOTT/UF book