A dependently-typed construction of semi-simplicial types ————————————————————————————————————————————————————————— (ERRATUM) Page 1, last sentence: read "mapped" instead of "associated", i.e. "Each element x ∈ Xn+1 can be canonically mapped to the set of its faces {di (x)|0 ≤ n−1 n i j≤ n}, the set of the faces of its faces, {di (dj (x))|0 ≤ j ≤ i ≤ n − 1}, etc."