PTS (pure type systems)

[ilya-klyuchnikov]

For educational purposes it is good to have just PTSs. Ideally, I would like to have the whole lambda cube.

[ilya-klyuchnikov]

In order to "calculate" something, there should be a facility introduce base types via assume (like in lambdapi).