Popular repositories Loading

1. ptt ptt Public

   Experimental type-checker for internally parametric type theory

   OCaml 32

2. equivariant-cartesian equivariant-cartesian Public

   formalization of an equivariant cartesian cubical set model of type theory

   Agda 18

3. cubical-topos-experiments cubical-topos-experiments Public

   Forked from IanOrton/cubical-topos-experiments

   Agda code for experimenting with internal models of cubical type theory

   Agda

4. cubical cubical Public

   Forked from agda/cubical

   Agda

5. cubicaltt cubicaltt Public

   Forked from mortberg/cubicaltt

   Experimental implementation of Cubical Type Theory

   Haskell

6. redtt redtt Public

   Forked from RedPRL/redtt

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

   OCaml