A dependently-typed construction of semi-simplicial types. (June 2015)