Skip to content

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

License

Notifications You must be signed in to change notification settings

JonasHoefer/poset-type-theory

Repository files navigation

Poset Type Theory

Experimental Haskell implementation of a version of cubical type theory with a model in presheaves over finite, non-empty posets. Some additional information can be found in the file located in doc, a PDF version of which can be found here.

Setup

The project is built using cabal. To install the type checker and evaluator, clone the repository and run cabal install --overwrite-policy=always. This will install an executable called postt in ~/.cabal/bin/ (and potentially remove old versions).

Usage

To see all options use postt --help. To type check all definitions in a file, and evaluate the last one use postt eval <path>. To start a read-eval-print-loop (repl) use postt repl. In the repl, use :help to see all available commands.

References

This implementation is inspired by cctt by András Kovács and cubicaltt by Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg.

Versions

About

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

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 4

  •  
  •  
  •  
  •