Re: [HoTT] Re: Why do we need judgmental equality?

[Matt Oliveri <atmacen@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2527 bytes --]

You'll have to ask Jon about what "idea" Nuprl's intrinsic untypedness is 
"not an essential part of". I'd say the most important thing about Nuprl is 
dependent refinement typing. In particular, Nuprl is extrinsic dependent 
typing, since the intrinsic type system is trivial. That turns out to be 
very interesting too, but makes the approach less broadly applicable.

I have some outlandish views about Nuprl. I don't consider its PER 
semantics to be a model, in the usual sense of model theory. It's 
proof-theoretic semantics. It's a semantic justification of some proof 
principles. Kind of like a strong normalization proof for ITT. You can 
point out that it's technically a realizability model. But I'd say that's 
because the terms are realizers. *What are they realizing?* That would be a 
model. The model theory of Nuprlish systems is currently virtually 
nonexistent. Somebody ought to fix that. There's a set-theoretic semantics 
(actually two, and they are different... sort of) for an old version of 
Nuprl. That's it, AFAIK.

On Monday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman wrote:
>
> FWIW, I think the only thing I have against NuPRL "in principle" is 
> that it seems to be closely tied to one particular model, which is the 
> opposite of what I want my type theories to achieve.  I say "seems" 
> because then someone says something like Jon's "Nuprl's underlying 
> objects are untyped -- but that is not an essential part of the idea", 
> providing an instance of the problem I have with NuPRL "in practice", 
> which is that every time I think I understand it someone proves me 
> wrong.  (-:O 
>
> Can you explain the difference between "definitional" (whatever that 
> means) and "strict" equality in Andromeda?  Of course there is the 
> technical difference between judgmental equality and the equality 
> type, but that doesn't seem to me to be a "real" difference in the 
> presence of equality reflection, particularly at the purely 
> philosophical level at which a phrase like "equality of sense" has to 
> be interpreted.  As far as I know, even beta-reduction has no 
> privileged status in the Andromeda core -- although I suppose 
> alpha-conversion probably does. 
>

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 3039 bytes --]