What I am asking for ideally is a formula P(x) of set theory that expresses âx is a successful definition of semi-simplicial types in Tââ.
I think having such a formula counts as success.
A good definition of semi-simplicial types should satisfying the following criteria:
1. The semi-simplicial types have the expected structure, and
2. It is possible to actually do something useful with them, inside type theory.
For instance, how do we know that the usual HIT definition of the circle is the right one? I was not really convinced until Mike calculated its fundamental group to be Z. This goes under "the object has the expected structure".
The external criterion of success is that for some (many) semantic model the internal definition correspond to an established notion of semi-simplicial objects.