Re: [HoTT] Conjecture

[Jon Sterling <j...@jonmsterling.com>]

Martin,

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.

Best,
Jon


On Wed, Apr 5, 2017, at 12:37 PM, 'Martin Escardo' via Homotopy Type
Theory wrote:
> 
> 
> On 31/03/17 17:09, 'Martin Escardo' via Homotopy Type Theory wrote:
> > 
> > 
> > On 30/03/17 23:49, Nicolai Kraus wrote:
> >> Interesting construction by Cory and you! And I think I can help
> >> you with the factorisation that you asked for, as follows:
> > 
> > Thanks for this, Nicolai.
> > 
> > Cory and I a battling against the clock to get our submission ready for
> > a conference. I'll continue the discussion after that.
> 
> I may as well give a link to the paper now that we have finished and
> submitted it, which is about partial functions in univalent type theory:
> http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf
> 
> The conjecture in the initial message of this thread goes well beyond
> this, and is even unrelated. But I am still very interested in the
> conjecture independently of any use of it.
> 
> Martin
> 
> -- 
> 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.