jcreedcmu/semisimplicial

Some thoughts about semisimplicial types in type theory

Defining semi-simplicial types

The file all.agda includes everything else.