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

[Matt Oliveri <atmacen@gmail.com>]

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

Let's say that "objects" are untyped, and "elements" are typed, by 
definition. These are semantic entities. Nuprl's (closed) terms are untyped 
in that you are allowed to think of them as objects. You can also think of 
them as elements. This is not the same. I'd like to distance Nuprl, based 
on PERs, from set theory. In set theory, objects are given their final 
meaning by the universe, and sets are types only in the most boring 
possible sense that you gather up objects and call them elements. In Nuprl, 
terms obtain their computational meaning as objects, but their mathematical 
meaning as elements. Interpreted as PERs, Nuprl's types let you ask whether 
two objects implement the same element. Equality of elements is not 
equality of objects, and the way you think about objects and elements is 
different. A variable has a declared type, and it denotes an arbitrary 
element of that type. It is meaningless to think of it as an object (unless 
the declared type is a subtype of the type of objects).

You are right that you don't need to explain elements in terms of objects. 
That doesn't necessarily make it a bad idea.

Each PER indicates how its elements are implemented by objects. There's no 
requirement that an object will have a unique type. Each type can be 
thought of as an abstract view of certain objects.

Constructions in Nuprl are heavily based on types, as in any strong type 
system. You wouldn't bother with a strong type system if you weren't going 
to do that. You can construct elements using the usual sorts of rules. 
Because Nuprl also has objects, you also have the option of constructing 
objects and then proving they implement elements of one or more types. If 
you've never felt at all constrained by a strong type system, great; you 
don't have to do that. But for many people, the intrinsically untyped 
approach is sometimes helpful. An element is an element; it doesn't matter 
whether it's an element by construction, or a verified object. I see this 
as a tremendous benefit for strongly typed programming.

On Monday, February 11, 2019 at 1:17:25 PM UTC-5, Thorsten Altenkirch wrote:
>
> I have got something else against NuPRL. It explains Type Theory via 
> untyped objects which are then typed. In  my view there is no reason why we 
> need to explain typed things via untyped objects. When we talk about 
> mathematical objects we think about typed entities, and the formalism of 
> type theory should reflect this. It is not that we find an untyped object 
> on the street and then try to find out which type it has. We are thinking 
> of a type first and then we construct an element. 
>
> Thorsten
>
>

-- 
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: 3366 bytes --]