I am interested in the fact that Id_X : X → (X → U) is an embedding
(in the sense of univalent mathematics), because it gives this:

  The injective types are precisely the retracts of exponential powers
  of universes, where an exponential power of a type D is a type of
  the form A → D for some type A.

Injectivity is defined as (functional) data rather than property
(using Σ rather than ∃).

A type D is called injective if for any embedding j:X→Y, every
function f:X→D extends to a map f':Y→D along j.

This injectivity result depends crucially on univalence (even though
the fact that Id_X is an embedding depends on much weaker hypotheses,
as we've found out in this thread).

It is also crucial that we say that j is an embedding (its fibers are
propositions) rather than merely that j is left-cancellable.

The following elaborates on this, with more comments and more
technical results rendered in Agda.

http://www.cs.bham.ac.uk/~mhe/agda-new/InjectiveTypes.html

We don't postulate anything in this development. Any axiom (UA, K, or
FunExt) is used explicitly as an assumption whenever needed.

The reason I came across injective types was my interest in searchable
and omniscient types. (In a previous research life, I had already come
across injective topological spaces when working on domain theory in
the sense of Dana Scott, and what we do here is partly inherited from
that.) This is also reported in this development: 

http://www.cs.bham.ac.uk/~mhe/agda-new/index.html

Some of this was reported in the past in this list. But there are new 
things, in particular regarding injectivity.

Martin.


On Saturday, 9 December 2017 00:27:16 UTC, Martín Hötzel Escardó wrote:
>
> 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
>
>   
>