homotopy-type-theory
There are 54 repositories under homotopy-type-theory topic.
HoTT/Coq-HoTT
A Coq library for Homotopy Type Theory
mortberg/cubicaltt
Experimental implementation of Cubical Type Theory
the1lab/1lab
A formalised, cross-linked reference resource for mathematics done in Homotopy 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
rzk-lang/rzk
An experimental proof assistant based on a type theory for synthetic ∞-categories.
HoTT-Intro/Agda
Agda formalisation of the Introduction to Homotopy Type Theory
fredefox/cat
A formalization of category theory in cubical Agda
forked-from-1kasper/ground_zero
Ground Zero: Lean 4 HoTT Library
ayberkt/formal-topology-in-UF
Formal Topology in Univalent Foundations (WIP).
jaycech3n/Isabelle-HoTT
An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
annenkov/two-level
Two-Level Type Theory
artagnon/bonak
🧊 An indexed construction of semi-simplicial and semi-cubical types
kcsmnt0/quotient
quotient types in cubical Agda
jaredloomis/Idris-HoTT
Homotopy Type Theory proofs in Idris
RedPRL/kado
🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory
forked-from-1kasper/anders
Anders: Cubical Type Checker
jdolson/univalence-from-scratch
Univalence from scratch in Idris
ixaxaar/monoid.space
Learn pure math with agda :rocket:
L-TChen/FiniteSets
Fintie Sets in Cubical Agda
jonaprieto/hott-cheatsheets
Homotopy type theory cheatsheets to read the HoTT Book
VITA-Group/SparseADV_Homotopy
[ICML 2021 Long Talk] "Sparse and Imperceptible Adversarial Attack via a Homotopy Algorithm" by Mingkang Zhu, Tianlong Chen, Zhangyang Wang
annenkov/trace-monoids
Trace monoids in Cubical Agda
JonasHoefer/poset-type-theory
Experimental implementation of a Cubical Type Theory modeled by presheaves over posets
lane-core/kitcat
Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda
forked-from-1kasper/bravo
Castle Bravo: Experimental HoTT Implementation
ncfavier/cubical-experiments
Experiments with Cubical Agda
wkolowski/Type-Theory-Wishlist
Personal research notes
wonks/type-theory-reading-group
IU Type Theory reading group
amato-gianluca/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
gergoerdi/cubical-freemonoids
Free monoids take a price HIT
konn/vscode-redtt-diagnostics
Diagnostic extension for redtt prover
LebrancWorkshop/Lebranc-Learn-Functional-Programming
I'm learning a Functional Programming by learning its pure math concepts and apply it on functional language like Haskell, Clojure, Elixir, etc.
smimram/div2
An Agda formalization of "division by 2" in classical ZF without choice.