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

[Nicolai Kraus <nicola...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2500 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 3870 bytes --]