Topic: "univalent-foundations"
HoTT/Coq-HoTT
A Coq library for Homotopy Type Theory
Language: Coq - Size: 25.9 MB - Last synced at: about 14 hours ago - Pushed at: 13 days ago - Stars: 1,313 - Forks: 196
mortberg/cubicaltt
Experimental implementation of Cubical Type Theory
Language: Haskell - Size: 2.43 MB - Last synced at: 5 days ago - Pushed at: over 1 year ago - Stars: 582 - Forks: 76
martinescardo/TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
Language: Agda - Size: 16.9 MB - Last synced at: about 13 hours ago - Pushed at: about 14 hours ago - Stars: 253 - Forks: 46
UniMath/agda-unimath
The agda-unimath library
Language: Agda - Size: 28.6 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 253 - Forks: 79
martinescardo/HoTT-UF-Agda-Lecture-Notes
Lecture notes on univalent foundations of mathematics with Agda
Language: Agda - Size: 5.8 MB - Last synced at: 21 days ago - Pushed at: about 1 year ago - Stars: 227 - Forks: 20
HoTT-Intro/Agda
Agda formalisation of the Introduction to Homotopy Type Theory
Language: Agda - Size: 6.82 MB - Last synced at: over 1 year ago - Pushed at: over 3 years ago - Stars: 110 - Forks: 4
ayberkt/formal-topology-in-UF
Formal Topology in Univalent Foundations (WIP).
Language: CSS - Size: 10.5 MB - Last synced at: about 1 month ago - Pushed at: almost 3 years ago - Stars: 36 - Forks: 2
rahulc29/realizability
Experiments with Realizability in Univalent Type Theory
Language: HTML - Size: 8.21 MB - Last synced at: about 1 month ago - Pushed at: 7 months ago - Stars: 18 - Forks: 1
langston-barrett/reed-thesis
My undergradate thesis on coinductive types in univalent type theory
Language: TeX - Size: 1.27 MB - Last synced at: 28 days ago - Pushed at: about 7 years ago - Stars: 17 - Forks: 0
forked-from-1kasper/bravo
Castle Bravo: Experimental HoTT Implementation
Language: OCaml - Size: 381 KB - Last synced at: 28 days ago - Pushed at: almost 2 years ago - Stars: 7 - Forks: 1
lane-core/kitcat
Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda
Language: Agda - Size: 134 KB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 5 - Forks: 0
amato-gianluca/UniMath Fork of UniMath/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Language: Coq - Size: 28.9 MB - Last synced at: 3 days ago - Pushed at: 2 months ago - Stars: 3 - Forks: 1
AnthonyBordg/UniLab
Formalized Mathematics
Language: Coq - Size: 76.2 KB - Last synced at: about 1 month ago - Pushed at: over 7 years ago - Stars: 1 - Forks: 0
amato-gianluca/MyHOTT
My implementation of the HOTT/UF book
Language: Coq - Size: 27.3 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0