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?