cubical-type-theory

There are 29 repositories under cubical-type-theory topic.

mortberg/cubicaltt
Experimental implementation of Cubical Type Theory
Language:Haskell571 45 6176
agda/cubical
An experimental library for Cubical Agda
Language:Agda460 27 243141
RedPRL/sml-redprl
The People's Refinement Logic
Language:Standard ML227 32 30918
RedPRL/cooltt
😎TT
Language:OCaml220 20 14316
RedPRL/redtt
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Language:OCaml204 26 23512
molikto/mlang
Towards changing things and see if it proofs
Language:Scala59 7 93
forked-from-1kasper/ground_zero
Ground Zero: Lean 4 HoTT Library
Language:Lean47 3 01
owo-lang/intellij-dtlc
IntelliJ plugin for several experimental programming languages here
Language:Kotlin35 5 155
artagnon/bonak
🧊 An indexed construction of semi-simplicial and semi-cubical types
Language:TeX25 4 13
kcsmnt0/quotient
quotient types in cubical Agda
Language:Agda22 2 00
marcinjangrzybowski/cubeViz2
Language:Haskell22 2 62
TOTBWF/cubical-categories
Category theory formalized in cubical agda
Language:Agda21 6 10
groupoid/anders
🧊 Модальний гомотопічний верифікатор математики
Language:OCaml20 0 02
RedPRL/kado
🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory
Language:OCaml19 3 51
forked-from-1kasper/anders
Anders: Cubical Type Checker
Language:OCaml18 1 01
rahulc29/realizability
Experiments with Realizability in Univalent Type Theory
Language:HTML17 2 151
fsestini/tt-in-cubical
Type Theory in Type Theory using Cubical Agda
Language:Agda12 2 00
L-TChen/FiniteSets
Fintie Sets in Cubical Agda
Language:Agda12 3 00
JonasHoefer/poset-type-theory
Experimental implementation of a Cubical Type Theory modeled by presheaves over posets
Language:Haskell7 3 22
ncfavier/cubical-experiments
Experiments with Cubical Agda
Language:Agda5 2 01
vikraman/generalised-species
Espèces généralisées de structures sur les groupoïdes
Language:Agda5 3 01
wkolowski/Type-Theory-Wishlist
Personal research notes
Language:Coq5 2 00
gergoerdi/cubical-freemonoids
Free monoids take a price HIT
Language:TeX3 3 0
konn/vscode-redtt-diagnostics
Diagnostic extension for redtt prover
Language:TypeScript3 3 11
ReubenHillyard/beta
Dependently-typed programming language.
Language:Rust1 1 0
ruza-net/kry
An experimental typechecker with dependent types, homogeneous path types, and cubical composition
Language:Rust1 2 00
sergey-goncharov/hybrid-agda
Duration monad and hybrid semantics in cubical Agda
Language:Agda1 1 00
wrrnhttn/agda-cubical-multidimensional
Multidimensional data in Cubical Agda.
Language:Agda0 1 40
InnovativeInventor/proof-repair-quotients
Artifact for "Proof Repair across Quotient Type Equivalences" paper (under submission)
Language:Agda2 0

cubical-type-theory

mortberg/cubicaltt

agda/cubical

RedPRL/sml-redprl

RedPRL/cooltt

RedPRL/redtt

molikto/mlang

forked-from-1kasper/ground_zero

owo-lang/intellij-dtlc

artagnon/bonak

kcsmnt0/quotient

marcinjangrzybowski/cubeViz2

TOTBWF/cubical-categories

groupoid/anders

RedPRL/kado

forked-from-1kasper/anders

rahulc29/realizability

fsestini/tt-in-cubical

L-TChen/FiniteSets

JonasHoefer/poset-type-theory

ncfavier/cubical-experiments

vikraman/generalised-species

wkolowski/Type-Theory-Wishlist

gergoerdi/cubical-freemonoids

konn/vscode-redtt-diagnostics

ReubenHillyard/beta

ruza-net/kry

sergey-goncharov/hybrid-agda

wrrnhttn/agda-cubical-multidimensional

InnovativeInventor/proof-repair-quotients