Re: [HoTT] Yet another characterization of univalence

["Martín Hötzel Escardó" <"escardo..."@gmail.com>]

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

On Friday, 1 December 2017 14:53:25 UTC, Martín Hötzel Escardó wrote:
>
>
>  OK. Here is a further weakening of the hypotheses. It suffices to have
> funext (again) and that the map
>
>     idtofun{B}{C} : A=B → (A→B)
>
> is left-cancellable (that is, idtofun p = idtofun q → p=q).
>
> Univalence gives that this is an embedding, which is stronger than
> saying that it is left-cancellable. And also K gives that this is an
> embedding.
>
>
I've written this down here in Agda 
:  http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html

(updating a 2015 development)

  * This is self-contained (doesn't use any library).
  * A main feature is that instead of J (or pattern maching on refl), this 
uses the Yoneda machinery everywhere instead (regretably with just one 
exception (I'd be grateful for suggestions of how to get rid of this use of 
J)).

A syntactical novelty is a new notation for universes in Agda closer to the 
notation in the HoTT book for informal mathematics in type theory. This 
could be further improved by making it built-in in Agda (as explained in 
the imported NonStandardUniverseNotation.lagda), but probably it is good 
enough without any modification to Agda.

Martin

  

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