mortberg/cubicaltt

Experimental implementation of Cubical Type Theory

Language: Haskell - Size: 2.43 MB - Last synced at: 7 months ago - Pushed at: over 1 year ago - Stars: 569 - Forks: 76

agda/cubical

An experimental library for Cubical Agda

Language: Agda - Size: 313 MB - Last synced at: 16 days ago - Pushed at: about 1 month ago - Stars: 477 - Forks: 145

RedPRL/sml-redprl 📦

The People's Refinement Logic

Language: Standard ML - Size: 11.3 MB - Last synced at: 5 months ago - Pushed at: over 2 years ago - Stars: 227 - Forks: 18

RedPRL/cooltt

😎TT

Language: OCaml - Size: 3.48 MB - Last synced at: 18 days ago - Pushed at: over 1 year ago - Stars: 225 - Forks: 14

RedPRL/redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

Language: OCaml - Size: 3.02 MB - Last synced at: 1 day ago - Pushed at: about 3 years ago - Stars: 208 - Forks: 12

molikto/mlang 📦

Towards changing things and see if it proofs

Language: Scala - Size: 1.31 MB - Last synced at: 12 months ago - Pushed at: almost 4 years ago - Stars: 60 - Forks: 3

forked-from-1kasper/ground_zero

Ground Zero: Lean 4 HoTT Library

Language: Lean - Size: 3.56 MB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 57 - Forks: 1

owo-lang/intellij-dtlc

IntelliJ plugin for several experimental programming languages here

Language: Kotlin - Size: 1.38 MB - Last synced at: 5 months ago - Pushed at: over 3 years ago - Stars: 34 - Forks: 5

artagnon/bonak

🧊 An indexed construction of semi-simplicial and semi-cubical sets

Language: TeX - Size: 4.06 MB - Last synced at: 28 days ago - Pushed at: 28 days ago - Stars: 28 - Forks: 3

forked-from-1kasper/anders

Anders: Cubical Type Checker

Language: OCaml - Size: 4.02 MB - Last synced at: 3 days ago - Pushed at: over 1 year ago - Stars: 24 - Forks: 1

groupoid/anders

🧊 Модальний гомотопічний верифікатор математики

Language: OCaml - Size: 14.4 MB - Last synced at: 7 days ago - Pushed at: 9 days ago - Stars: 22 - Forks: 2

kcsmnt0/quotient

quotient types in cubical Agda

Language: Agda - Size: 8.79 KB - Last synced at: almost 2 years ago - Pushed at: about 6 years ago - Stars: 22 - Forks: 0

TOTBWF/cubical-categories

Category theory formalized in cubical agda

Language: Agda - Size: 37.1 KB - Last synced at: about 2 months ago - Pushed at: about 5 years ago - Stars: 20 - Forks: 0

RedPRL/kado

🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory

Language: OCaml - Size: 648 KB - Last synced at: 1 day ago - Pushed at: 7 months ago - Stars: 19 - Forks: 1

rahulc29/realizability

Experiments with Realizability in Univalent Type Theory

Language: HTML - Size: 8.21 MB - Last synced at: 16 days ago - Pushed at: 6 months ago - Stars: 18 - Forks: 1

marcinjangrzybowski/cubeViz2

Language: Haskell - Size: 6.66 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 18 - Forks: 2

L-TChen/FiniteSets

Fintie Sets in Cubical Agda

Language: Agda - Size: 69.3 KB - Last synced at: 23 days ago - Pushed at: over 5 years ago - Stars: 12 - Forks: 0

fsestini/tt-in-cubical

Type Theory in Type Theory using Cubical Agda

Language: Agda - Size: 70.3 KB - Last synced at: 5 months ago - Pushed at: about 6 years ago - Stars: 12 - Forks: 0

ncfavier/cubical-experiments

Experiments with Cubical Agda

Language: Agda - Size: 163 KB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 9 - Forks: 1

phijor/cubical-containers

Language: Agda - Size: 493 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 5 - Forks: 0

wkolowski/Type-Theory-Wishlist

Personal research notes

Language: Coq - Size: 1.13 MB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 5 - Forks: 0

vikraman/generalised-species

Espèces généralisées de structures sur les groupoïdes

Language: Agda - Size: 150 KB - Last synced at: 2 months ago - Pushed at: over 2 years ago - Stars: 5 - Forks: 1

konn/vscode-redtt-diagnostics 📦

Diagnostic extension for redtt prover

Language: TypeScript - Size: 120 KB - Last synced at: 12 months ago - Pushed at: about 3 years ago - Stars: 3 - Forks: 1

gergoerdi/cubical-freemonoids

Free monoids take a price HIT

Language: TeX - Size: 148 KB - Last synced at: about 2 months ago - Pushed at: over 5 years ago - Stars: 3 - Forks: 0

ReubenHillyard/beta

Dependently-typed programming language.

Language: Rust - Size: 179 KB - Last synced at: 11 months ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

sergey-goncharov/hybrid-agda

Duration monad and hybrid semantics in cubical Agda

Language: Agda - Size: 59.6 KB - Last synced at: over 1 year ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0

ruza-net/kry

An experimental typechecker with dependent types, homogeneous path types, and cubical composition

Language: Rust - Size: 24.4 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0

JonasHoefer/poset-type-theory

Experimental implementation of a Cubical Type Theory modeled by presheaves over posets

Language: Haskell - Size: 366 KB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 0 - Forks: 1

InnovativeInventor/proof-repair-quotients

Artifact for "Proof Repair across Quotient Type Equivalences" paper (under submission)

Language: Agda - Size: 76.2 KB - Last synced at: about 2 months ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

wrrnhttn/agda-cubical-multidimensional

Multidimensional data in Cubical Agda.

Language: Agda - Size: 81.1 KB - Last synced at: over 1 year ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0