Re: [HoTT] Conjecture

[Martin Escardo <escardo...@googlemail.com>]

Dear Thomas,

Sorry it took so long to answer, but I needed to find time to be able
to write my reaction to your remarks.

(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.)

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