univalent-mathematics

There are 10 repositories under univalent-mathematics topic.

martinescardo/TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
Language:Agda233 15 3742
UniMath/agda-unimath
The agda-unimath library
Language:Agda223 9 14771
martinescardo/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
Language:Agda220 15 1319
HoTT-Intro/Agda
Agda formalisation of the Introduction to Homotopy Type Theory
Language:Agda123 11 05
ayberkt/formal-topology-in-UF
Formal Topology in Univalent Foundations (WIP).
Language:CSS35 5 62
rahulc29/realizability
Experiments with Realizability in Univalent Type Theory
Language:HTML17 2 151
lane-core/kitcat
Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda
Language:Agda6 3 00
amato-gianluca/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Language:Coq3 5 01
fredrik-bakke/forest
Language:Shell3 2 00
amato-gianluca/MyHOTT
My implementation of the HOTT/UF book
Language:Coq0 2 00