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
Artifact for "Proof Repair across Quotient Type Equivalences" paper (under submission)
Duration monad and hybrid semantics in cubical Agda
An experimental typechecker with dependent types, homogeneous path types, and cubical composition
Dependently-typed programming language.
Diagnostic extension for redtt prover
Free monoids take a price HIT
Personal research notes
Experiments with Cubical Agda
Espèces généralisées de structures sur les groupoïdes
Experiments with Realizability in Univalent Type Theory
Fintie Sets in Cubical Agda
Type Theory in Type Theory using Cubical Agda
🧊 Модальний гомотопічний верифікатор математики
Anders: Cubical Type Checker
🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory
Category theory formalized in cubical agda
quotient types in cubical Agda
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."