* Semantic Success Condition for the definability of Semi-Simplicial Types
@ 2016-09-21 12:48 Dimitris Tsementzis
2016-09-21 13:40 ` [HoTT] " Andrej Bauer
2016-09-21 17:18 ` Nicolai Kraus
0 siblings, 2 replies; 6+ messages in thread
From: Dimitris Tsementzis @ 2016-09-21 12:48 UTC (permalink / raw)
To: Homotopy Type Theory
Is there an agreed-upon semantic success condition for the definition of semi-simplicial types?
In particular, given the type theory T in the Simplicial Model paper, if X is a type definable in T, then what must the interpretation of X in the simplicial model satisfy in order to be regarded a successful definition of semi-simplicial types?
(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’’.)
Thank you,
Dimitris
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] Semantic Success Condition for the definability of Semi-Simplicial Types
2016-09-21 12:48 Semantic Success Condition for the definability of Semi-Simplicial Types Dimitris Tsementzis
@ 2016-09-21 13:40 ` Andrej Bauer
2016-09-21 17:18 ` Nicolai Kraus
1 sibling, 0 replies; 6+ messages in thread
From: Andrej Bauer @ 2016-09-21 13:40 UTC (permalink / raw)
To: Dimitris Tsementzis; +Cc: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 963 bytes --]
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.
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.
With kind regards,
Andrej
[-- Attachment #2: Type: text/html, Size: 1648 bytes --]
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] Semantic Success Condition for the definability of Semi-Simplicial Types
2016-09-21 12:48 Semantic Success Condition for the definability of Semi-Simplicial Types Dimitris Tsementzis
2016-09-21 13:40 ` [HoTT] " Andrej Bauer
@ 2016-09-21 17:18 ` Nicolai Kraus
2016-09-21 20:45 ` Dimitris Tsementzis
1 sibling, 1 reply; 6+ messages in thread
From: Nicolai Kraus @ 2016-09-21 17:18 UTC (permalink / raw)
To: Dimitris Tsementzis; +Cc: Homotopy Type Theory
[-- 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 --]
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] Semantic Success Condition for the definability of Semi-Simplicial Types
2016-09-21 17:18 ` Nicolai Kraus
@ 2016-09-21 20:45 ` Dimitris Tsementzis
2016-09-21 21:43 ` Michael Shulman
0 siblings, 1 reply; 6+ messages in thread
From: Dimitris Tsementzis @ 2016-09-21 20:45 UTC (permalink / raw)
To: Nicolai Kraus, Homotopy Type Theory, Andrej Bauer
[-- Attachment #1: Type: text/plain, Size: 5125 bytes --]
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 <mailto: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 <mailto:andrej...@andrej.com>> wrote:
>
> On Wed, Sep 21, 2016 at 2:48 PM, Dimitris Tsementzis <dtse...@princeton.edu <mailto: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: 7980 bytes --]
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] Semantic Success Condition for the definability of Semi-Simplicial Types
2016-09-21 20:45 ` Dimitris Tsementzis
@ 2016-09-21 21:43 ` Michael Shulman
2016-09-21 21:56 ` Dimitris Tsementzis
0 siblings, 1 reply; 6+ messages in thread
From: Michael Shulman @ 2016-09-21 21:43 UTC (permalink / raw)
To: Dimitris Tsementzis; +Cc: Nicolai Kraus, Homotopy Type Theory, Andrej Bauer
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.
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [HoTT] Semantic Success Condition for the definability of Semi-Simplicial Types
2016-09-21 21:43 ` Michael Shulman
@ 2016-09-21 21:56 ` Dimitris Tsementzis
0 siblings, 0 replies; 6+ messages in thread
From: Dimitris Tsementzis @ 2016-09-21 21:56 UTC (permalink / raw)
To: Michael Shulman, Homotopy Type Theory
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.
^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2016-09-21 21:56 UTC | newest]
Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2016-09-21 12:48 Semantic Success Condition for the definability of Semi-Simplicial Types Dimitris Tsementzis
2016-09-21 13:40 ` [HoTT] " Andrej Bauer
2016-09-21 17:18 ` Nicolai Kraus
2016-09-21 20:45 ` Dimitris Tsementzis
2016-09-21 21:43 ` Michael Shulman
2016-09-21 21:56 ` Dimitris Tsementzis
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).