Re: [HoTT] Semantic Success Condition for the definability of Semi-Simplicial Types

[Michael Shulman <shu...@sandiego.edu>]

In any oo-topos C we can talk about a classifying object for
semisimplicial objects.  This would be an object T together with, for
any object X, an equivalence (natural in X) between the
hom-oo-groupoid Hom_C(X,T) and the oo-groupoid of (small)
semisimplicial objects in the slice oo-category C/X.  So one semantic
criterion for correctness would be that "the type of semisimplicial
types" interprets in any oo-topos (or, specifically in the oo-topos of
oo-groupoids, as presented by simplicial sets) to such a classifying
object.  Other stronger conditions could also be given -- in
particular, this one says nothing about Reedy fibrancy -- but this
seems to me to be certainly a necessary condition for correctness.

On Wed, Sep 21, 2016 at 1:45 PM, Dimitris Tsementzis
<dtse...@princeton.edu> wrote:
> 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.
>
> Best,
>
> Dimitris
>
> 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
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.