Re: [HoTT] Conjecture

[Thomas Streicher <stre...@mathematik.tu-darmstadt.de>]

> 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 ¡X a logical approach. (English summary)
Math. Structures Comput. Sci. 9 (1999), no. 2, 177¡V223.

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