Experimental implementation of a Cubical Type Theory modeled by presheaves over posets
-
Updated
May 24, 2024 - Haskell
Experimental implementation of a Cubical Type Theory modeled by presheaves over posets
Experiments with Realizability in Univalent Type Theory
Ground Zero: Lean 4 HoTT Library
Personal research notes
🧊 Модальний гомотопічний верифікатор математики
🧊 An indexed construction of semi-simplicial and semi-cubical types
Experiments with Cubical Agda
Artifact for "Proof Repair across Quotient Type Equivalences" paper (under submission)
🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory
Anders: Cubical Type Checker
😎TT
Dependently-typed programming language.
Experimental implementation of Cubical Type Theory
The People's Refinement Logic
Espèces généralisées de structures sur les groupoïdes
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Diagnostic extension for redtt prover
IntelliJ plugin for several experimental programming languages here
Add a description, image, and links to the cubical-type-theory topic page so that developers can more easily learn about it.
To associate your repository with the cubical-type-theory topic, visit your repo's landing page and select "manage topics."