A type theory playground
This is a place for experimental implementations of type theories that may well be busted, as well as a place for me to learn Racket.
No guarantees about any of it!
Presently, everything is tested on Racket 6.3. Older versions probably don’t work.
A Refiner for a CTT Dialect
(prove (⊢ empty '(⋂ ((t Type)) (Π ((y t)) t))))
You’ll get a little proof editor. In the top of the proof editor,
there’s a tree view that shows the overall structure of the
proof. Click on the proof goal, and the bottom half of the proof
editor will display its details. In the text field labeled “by”, type
intersection-membership and click the Refine button. You’ll get two
In the first of these subgoals, type
(lambda-intro '(x)) and
refine. This will give two goals: solve them with
(hypothesis 0) and
(hypothesis-equality 0) respectively. As you solve these goals, the
goal overview is updated to show the incrementally-constructed
Solve the last goal with
type-in-type. Proper universe polymorphism
and perhaps typical ambiguity remain to be implemented.