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

[Dimitris Tsementzis <dtse...@princeton.edu>]

Ah thanks! This is exactly what I was looking for. (In fact, a strong generally accepted necessary condition is really what I should’ve asked for.)

Dimitris

> On Sep 21, 2016, at 17:43, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> 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.