Re: [HoTT] Yet another characterization of univalence

[Gershom B <gers...@gmail.com>]

On December 18, 2017 at 5:58:22 PM, Martín Hötzel Escardó
(escardo...@gmail.com) wrote:
> >
> 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.
>

Here is a question: given a local operator (Lawvere-Tierny topology)
j, an object D is a sheaf if for any j-dense subobject X >-> Y, every
function f : X -> D extends to a map f’ : Y -> D. Is there a way in
which we can view injective types as sheafs in some appropriate sense?

Regards,
Gershom

On Mon, Dec 18, 2017 at 5:58 PM, Martín Hötzel Escardó
<escardo...@gmail.com> wrote:
> 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
>>
>>
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.