rahulc29 / realizability

Experiments with Realizability in Univalent Type Theory
https://rahulc29.github.io/realizability/
Apache License 2.0
10 stars 1 forks source link
category-theory cubical-type-theory realizability univalent-foundations univalent-mathematics univalent-type-theory

Experiments with Realizability in Univalent Type Theory

This project formalises categorical realizability from the ground up in Cubical Agda.

Notable results include :

Current formalisation targets include :