Thanks a lot, Andrej and Nicolai. I’m merging your responses together.

The external criterion of success is that for some (many) semantic model the internal definition correspond to an established notion of semi-simplicial objects.

Right, exactly. My question then is: in the case of the simplicial model is there a generally accepted way of expressing that the "internal definition corresponds to the established notion" without referring to some property the internal definition satisfies (e.g. Nicolai’s way of making it precise below)?

the goal would be to write a function f : Nat -> U' (where U' is e.g. the second universe) in type theory such that, for every numeral n, f(n) and P(n) are equivalent.

In those terms, what I am asking for is this: If you interpret such an f into the simplicial model, then what would be something that we can say about the interpreted f (call it “F") that would count as a successful definition? Obviously, one answer would be that F is the interpretation of a term f that satisfies the property you outlined. This would be a formula in set theory too because we can take the syntax to have been encoded in set theory.

But I was wondering whether there is something that does not refer to a property that F would satisfy simply because it is the interpretation of something in the syntax. For example, something in terms of (external) Reedy diagrams in semi-simplicial sets?

(There is nothing constraining me to the simplicial model, but I would imagine stating a semantic success condition for the simplicial model would be the easier first step.)

. I don't really know what exactly "a formula P in set theory” means.

The simplicial model is constructed in set theory (in particular in ZFC+2 inaccessibles). A possible solution f: Nat -> U’ (to use Nicolai’s notation) in the syntax will then be interpreted as something in set theory (in particular, a section F in some category). In that setting we can talk about F using formulas of set theory. So I was wondering whether such a formula φ(x) has been stated, for which we can say that

exists x φ(x) encodes that “there is a definition of semi-simplicial types in T”

As I said above, we could simply take φ(x)=“x is the interpretation of a function f: N -> U’ in T that satisfies Nicolai’s condition”. But I’m asking whether there is a φ that is (more) semantic in character.

On Sep 21, 2016, at 13:18, Nicolai Kraus <nicola...@gmail.com> wrote:

On Wed, Sep 21, 2016 at 1:48 PM, Dimitris Tsementzis <dtse...@princeton.edu> wrote:
Is there an agreed-upon semantic success condition for the definition of semi-simplicial types?

I'm not sure whether the following is helpful because I won't refer to the simplicial sets model.
Given a fixed numeral n, we know what the type of semi-simplicial types up to level n should be (up to equivalence). If you want, you can take some programming language and write a program P : Nat -> String such that P(n) is a syntactical representation of semi-simplicial types up to n (two years ago or so, I wrote a Haskell script which generated Agda code). Then, you can take this P to make the challenge precise: the goal would be to write a function f : Nat -> U' (where U' is e.g. the second universe) in type theory such that, for every numeral n, f(n) and P(n) are equivalent.
However, this would only cover the first point of Andrej's success criteria (it would give you something with the expected structure, but it's not clear whether it will be useful).

An alternative way of phrasing what I said above would be: take the Altenkirch-Capriotti-K paper "Extending Homotopy Type Theory with Strict Equality" which presents an HTS-style two-level system with a fibrant type Nat of natural numbers and a non-fibrant type Nat_s of strict natural numbers. We have a family S : Nat_s -> U of semi-simplicial types. The challenge here would be to define a family S' : Nat -> U which extends S. By the conservativity construction of Paolo Capriotti's forthcoming PhD thesis, this can then be translated back to types in "book HoTT".
I think this could make it easier to see whether we can actually do something useful with such a construction of semi-simplicial types.

Andrej, I am not sure about this:

On Wed, Sep 21, 2016 at 2:40 PM, Andrej Bauer <andrej...@andrej.com> wrote:

On Wed, Sep 21, 2016 at 2:48 PM, Dimitris Tsementzis <dtse...@princeton.edu> wrote:
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.

If P(x) was a formula in type theory, then maybe, yes. I don't really know what exactly "a formula P in set theory" means, but I don't think such a formula would solve the problem, given that we can say externally what semi-simplicial types ought to be.

Best,
Nicolai