Re: [HoTT] Conjecture

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

On Fri, Apr 7, 2017 at 2:49 AM, 'Martin Escardo' via Homotopy Type
Theory <HomotopyT...@googlegroups.com> wrote:
> (1) Indeed, I do like to think of the fragment of univalent type
> theory consisting of function extensionality + proposition
> extensionality + propositional truncation as essentially the same
> thing as topos logic, provided we have propositional resizing. (But,
> as discussed, much can be done without propositional resizing (but not
> all), and one way of looking at HIT's is as a mechanism to avoid
> resizing.)

I would say that to really be talking about (elementary) topos logic,
one should also do without universes other than hProp.  Of course,
elementary 1-toposes also validate UIP.

If we also omit hProp and propositional resizing, but include
nonrecursive HITs as well as ordinary inductive types, then it ought
to be basically Pi-W-pretopos logic; right?

> This is good: this fragment leaves us in familiar territory.
>
> (2) I don't see univalent type theory as simply the extension of type
> theory with univalence (and hence function and proposition
> extensionality). Before we extend dependent type theory with any
> axiom, we can start to think "univalently".
>
> In particular, the notions of h-level, proposition, contractibility,
> equivalence, the distinction of existence as proposition or structure,
> so as to be able to define e.g. embeddings, surjections, and many
> others correctly, can be formulated and understood before we bring
> univalence.
>
> In this way "univalent type theory" is a different way to understand
> good old type theory. Of course, with univalence we get more, and what
> you are saying, and I don't disagree fundamentally, is that this
> "more" are types of higher h-level and theorems and constructions with
> them (such as the type of categories, if we want to avoid homotopy in
> the discussion).
>
> Although we don't use univalence in our paper, we formulate our
> notions in the light of this new, alternative understanding of type
> theory.
>
> One example, already mentioned in the above answer to Jon, is
> something that kept Cory and I working for an afternoon, but perhaps
> is not adequately emphasized in the paper.
>
> In topos logic, you define (for the dominance of all propositions)
>
>   Lift(X) = { A:X->Omega | (exists(x:X), A x) &
>                            forall(x,y:X), A x -> A y -> x = y }
>
> If we want, in univalent type theory, this to work for types of higher
> h-levels, how should we define this?
>
> The above definition works well and can be kept as it is if X is a
> set. To generalize it to types of higher levels, we need two
> modifications:
>
>   (i)  Change Omega to the universe U.
>   (ii) Reformulate the condition on A as isProp(Sigma(x:X), A x).
>
> When X is a set, the reformulation (i)-(ii) makes no
> difference. However, in the general case, it is (i) and (ii) that give
> the right definition. For instance, with the right definition, we
> always get an embedding X->Lift X, whereas if we had taken the
> original topos-theoretic version of Lift, then Lift S^1 would be a
> singleton and hence wouldn't embed S^1. We would get the wrong notion
> of partial function.
>
> Thus, although we haven't used univalence, we took care of formulating
> the notions so that they are not restricted to the realm of sets, and
> in this sense what we are doing can be considered as univalent type
> theory.
>
> (3) We should have cited Andrej's and Bernhard's references below, and
> we will (and many other things, to reflect the amount of work done
> about this in the context of topos theory). Of course we are aware of
> them, but thanks for mentioning them in this list!
>
> (4) A last point is that, as opposed to most of the work in the topos
> literature for dominances in realizability toposes as in (3), we
> deliberately don't use Markov's principle or countable choice in our
> internal development of computability in univalent type theory
> (Section 3 of the paper). Moreover, we are *not* looking at synthetic
> computability. We are looking at plain computability.
>
> Best,
> Martin
>
>
> On 06/04/17 12:52, Thomas Streicher wrote:
>>> This looks like a very interesting paper, thank you for sharing. I look
>>> forward to reading it in more detail.
>>>
>>> I am curious, does this development use univalence except to establish
>>> functional extensionality and propositional extensionality? The reason I
>>> ask is, I wonder if it is possible to do a similar development of
>>> computability theory in extensional type theory and get analogous
>>> results. Additionally, I am curious whether you have found cases in
>>> which univalence clarifies or sharpens this development, since I'm
>>> trying to keep track of interesting use-cases of univalence.
>>
>> For synthetic domain theory a formulation in extensional type theory
>> has been given in
>>
>> MR1694130 (2000f:68069)
>> Reus, Bernhard; Streicher, Thomas
>> General synthetic domain theory — a logical approach. (English summary)
>> Math. Structures Comput. Sci. 9 (1999), no. 2, 177–223.
>>
>> There is no need whatsoever to use univalence or something like that.
>> The only benefit would be to solve domain equations up to equality
>> which even computer scientists find unnecessary (for good reasons).
>>
>> Andrej Bauer has written on Synthetic Recursion Theory, see
>> math.andrej.com/data/synthetic.pdf.
>>
>> So I tend to the opinion that theer can't be an intrinsic use of
>> Univalence or HITs. But if there is I am curious to learn which one!
>>
>> Thomas
>>
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe
>
> --
> 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.