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

["Anders Mörtberg" <andersmortberg@gmail.com>]

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

Note that judgmental equality is not only a convenience, but it also 
affects what is provable in your type theory. Consider the interval HIT, it 
is contractible and hence equivalent to Unit. But it also lets you prove 
function extensionallity which you definitely don't get from the Unit type.

--
Anders

On Tuesday, February 5, 2019 at 6:00:24 PM UTC-5, Matt Oliveri wrote:
>
> The type checking rules are nonlinear (reuses metavariables). For example, 
> for function application, the type of the argument needs to "equal" the 
> domain of the function. What equality is that? It gets called judgmental 
> equality. It's there in some sense even if it's just syntactic equality. 
> But it seems really really hard to have judgmental equality be just 
> syntactic equality, in a dependent type system. It would also be unnatural, 
> from a computational perspective; the judgmental equations are saying 
> something about the computational behavior of the system.
>
> On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote:
>>
>> In section 1.1 of the HoTT book it says "In type theory there is also a 
>> need for an equality judgment." Currently it seems to me like one could, in 
>> principle, replace substitution along judgmental equality with explicit 
>> transports if one added a few sensible rules to the type theory. Is there a 
>> fundamental reason why the equality judgment is still necessary?
>>
>> Thanks,
>> Felix Rech
>>
>

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