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