Re: [HoTT] Re: Where is the problem with initiality?

[Ambrus Kaposi <kaposi...@gmail.com>]

On Fri, Jun 1, 2018 at 11:27 PM Matt Oliveri <atm...@gmail.com> wrote:
>
> On Friday, June 1, 2018 at 1:45:42 PM UTC-4, Eric Finster wrote:
>>
>> So from an internal perspective, I cannot think of any reason to
>> insist on decidability.
>
> I agree with this. And in particular, I think QIITs can define intrinsic syntax of (fully-annotated) extensional type theroy just fine. Equality reflection would be an extra equality constructor. Isn't that right? What do Thorsten and team think of that? Is it an infelicity of QIITs, perhaps because they're hSet truncated? Or is there a problem with ETT that structuralism doesn't shed light on? Or is ETT maybe not so bad?

Yes, the syntax for extensional type theory can be defined as a QIIT.

For me, the problem with it is that there is no easy way to input
terms in the computer: starting with a string, lexing, parsing it and
getting an untyped term, then typechecking the untyped term. During
bidirectional typechecking, we need that types in the QIIT have
decidable equality. See e.g.
https://bitbucket.org/akaposi/tt-in-tt/src/HEAD/Typecheck.agda
Equality of types is not decidable in ETT, even if we can normalise
terms (use it for programming).

But maybe there are other ways to build terms in this QIIT in a
convenient way (the NuPRL, Andromeda people know this), and then I
also don't see why we would insist on decidability of equality.