Re: [HoTT] Yet another characterization of univalence

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

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



On Tuesday, 19 December 2017 03:36:51 UTC, Gershom B wrote:
On December 18, 2017 at 5:58:22 PM, Martín Hötzel Escardó 
(escar...@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? 


I don't think so, because we don't have the required uniqueness
of the sheaf condition here.

In general, if a type D is injective, many extensions of any
f:X→D along an embedding j:X→Y exist.

In the file
http://www.cs.bham.ac.uk/~mhe/agda-new/InjectiveTypes.html, 
two canonical extensions are shown to exist, a minimal one f\j
using Σ, and a maximal f/j one using Π. 

In fact they are left and right Kan extensions, in the sense that we
have equivalences

 Nat f (g ∘ j) ≃ Nat f∖j  g

and

 Nat g f/j ≃ Nat (g ∘ j) f

of natural transformations involving the "presheaves" g : Y → U and
f\j, f/j : X → U.

Although these two extensions are canonical in the above sense, they are not unique.

Martin


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