Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
* [HoTT] Proof that something is an embedding without assuming excluded middle?
@ 2018-11-13 20:32 Martín Hötzel Escardó
  2018-11-13 20:36 ` [HoTT] " Martín Hötzel Escardó
  2018-11-13 23:47 ` Jean Joseph
  0 siblings, 2 replies; 12+ messages in thread
From: Martín Hötzel Escardó @ 2018-11-13 20:32 UTC (permalink / raw)
  To: Homotopy Type Theory

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

Let P be a subsingleton and 𝓤 be a universe, and consider the
product map

  Π : (P → 𝓤) → 𝓤
         A     ↦ Π (p:P), A(p).

Is this an embedding? (In the sense of having subsingleton
fibers.)

It is easy to see that this is the case if P=𝟘 or P=𝟙 (empty or
singleton type).

But the reasons are fundamentally different:

(0) If P=𝟘, the domain of Π is equivalent to 𝟙, and Π amounts to
    the map 𝟙 → 𝓤 with constant value 𝟙.

    In general, a function 𝟙 → X into a type X is *not* an
    embedding. Such a function is an embedding iff it maps the
    point of 𝟙 to a point x:X such that the type x=x is a
    singleton.

    And indeed for X:=𝓤 we have that the type 𝟙=𝟙 is a singleton.

(1) If P=𝟙, the domain of Π is equivalent to 𝓤, and Π amounts to
    the identity map 𝓤 → 𝓤, which, being an equivalence, is an
    embedding.

Question. Is there a uniform proof that Π as above for P a
subsingleton is an embedding, without considering the case
distinction (P=𝟘)+(P=𝟙)?

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 12+ messages in thread

* [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-13 20:32 [HoTT] Proof that something is an embedding without assuming excluded middle? Martín Hötzel Escardó
@ 2018-11-13 20:36 ` " Martín Hötzel Escardó
  2018-11-13 23:47 ` Jean Joseph
  1 sibling, 0 replies; 12+ messages in thread
From: Martín Hötzel Escardó @ 2018-11-13 20:36 UTC (permalink / raw)
  To: Homotopy Type Theory

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

NB. Of course this map is left-cancellable. But this is weaker than being 
an embedding. M.

On Tuesday, 13 November 2018 20:32:22 UTC, Martín Hötzel Escardó wrote:
>
> Let P be a subsingleton and 𝓤 be a universe, and consider the
> product map
>
>   Π : (P → 𝓤) → 𝓤
>          A     ↦ Π (p:P), A(p).
>
> Is this an embedding? (In the sense of having subsingleton
> fibers.)
>
> It is easy to see that this is the case if P=𝟘 or P=𝟙 (empty or
> singleton type).
>
> But the reasons are fundamentally different:
>
> (0) If P=𝟘, the domain of Π is equivalent to 𝟙, and Π amounts to
>     the map 𝟙 → 𝓤 with constant value 𝟙.
>
>     In general, a function 𝟙 → X into a type X is *not* an
>     embedding. Such a function is an embedding iff it maps the
>     point of 𝟙 to a point x:X such that the type x=x is a
>     singleton.
>
>     And indeed for X:=𝓤 we have that the type 𝟙=𝟙 is a singleton.
>
> (1) If P=𝟙, the domain of Π is equivalent to 𝓤, and Π amounts to
>     the identity map 𝓤 → 𝓤, which, being an equivalence, is an
>     embedding.
>
> Question. Is there a uniform proof that Π as above for P a
> subsingleton is an embedding, without considering the case
> distinction (P=𝟘)+(P=𝟙)?
>
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 12+ messages in thread

* [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-13 20:32 [HoTT] Proof that something is an embedding without assuming excluded middle? Martín Hötzel Escardó
  2018-11-13 20:36 ` [HoTT] " Martín Hötzel Escardó
@ 2018-11-13 23:47 ` Jean Joseph
  2018-11-14 10:23   ` Martín Hötzel Escardó
  1 sibling, 1 reply; 12+ messages in thread
From: Jean Joseph @ 2018-11-13 23:47 UTC (permalink / raw)
  To: Homotopy Type Theory

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

I think to show this is an embedding may imply the law of double negation. 
For any proposition Q, let P = {0 : Z | Q}. Let A be defined as for all p : 
P, A(p) = 0 : P, and let B be defined as for all p : P, B(p) = not not (0 : 
P). To show that Pi (p : P), A(p) = Pi (p : P), B(p), you can define the 
following isomorphism (?): for any f : Pi (p : P), A(p), define g : Pi (p : 
P), B(p) by picking p : P, then f(p) : A(p), so Q is true. Hence, not not Q 
is true, meaning it has an element, so g(p) is that element. We then can 
conclude A = B. By function extensionality, that's equivalent to for all p 
: P, A (p) = B (p), which gives Q = not not Q. 

Jean

On Tuesday, November 13, 2018 at 3:32:22 PM UTC-5, Martín Hötzel Escardó 
wrote:
>
> Let P be a subsingleton and 𝓤 be a universe, and consider the
> product map
>
>   Π : (P → 𝓤) → 𝓤
>          A     ↦ Π (p:P), A(p).
>
> Is this an embedding? (In the sense of having subsingleton
> fibers.)
>
> It is easy to see that this is the case if P=𝟘 or P=𝟙 (empty or
> singleton type).
>
> But the reasons are fundamentally different:
>
> (0) If P=𝟘, the domain of Π is equivalent to 𝟙, and Π amounts to
>     the map 𝟙 → 𝓤 with constant value 𝟙.
>
>     In general, a function 𝟙 → X into a type X is *not* an
>     embedding. Such a function is an embedding iff it maps the
>     point of 𝟙 to a point x:X such that the type x=x is a
>     singleton.
>
>     And indeed for X:=𝓤 we have that the type 𝟙=𝟙 is a singleton.
>
> (1) If P=𝟙, the domain of Π is equivalent to 𝓤, and Π amounts to
>     the identity map 𝓤 → 𝓤, which, being an equivalence, is an
>     embedding.
>
> Question. Is there a uniform proof that Π as above for P a
> subsingleton is an embedding, without considering the case
> distinction (P=𝟘)+(P=𝟙)?
>
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 12+ messages in thread

* [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-13 23:47 ` Jean Joseph
@ 2018-11-14 10:23   ` Martín Hötzel Escardó
  2018-11-14 11:07     ` Paolo Capriotti
  0 siblings, 1 reply; 12+ messages in thread
From: Martín Hötzel Escardó @ 2018-11-14 10:23 UTC (permalink / raw)
  To: Homotopy Type Theory

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

It seems to me that you are trying to show that if the map is
left-cancellable then excluded middle holds. However, as I said, the
map is left-cancellable. Moreover, it is a section with retraction
X ↦ λp.X:

        Π : (P → 𝓤) → 𝓤
               A          ↦ Π(p:P), A(p)    (section)
            λ(p:P).X  ↤ X                    (retraction)

because if p:P is given then A is constant with value (equivalent
to) ΠA.

For sets, sections (and more generally left-cancellable maps) are
necessarily embeddings. However, for general types this need not be
the case. See the paper https://arxiv.org/abs/1507.03634 by Mike
Shulman, and in particular Theorem 3.10, which gives a criterion for a
section being an embedding.

(I think the problem with your proof attempt is that you forgot to
give the other direction of the "isomorphism", which would require
double negation elimination.)

Best,
Martin

On Tuesday, 13 November 2018 23:47:40 UTC, Jean Joseph wrote:
>
> I think to show this is an embedding may imply the law of double negation. 
> For any proposition Q, let P = {0 : Z | Q}. Let A be defined as for all p : 
> P, A(p) = 0 : P, and let B be defined as for all p : P, B(p) = not not (0 : 
> P). To show that Pi (p : P), A(p) = Pi (p : P), B(p), you can define the 
> following isomorphism (?): for any f : Pi (p : P), A(p), define g : Pi (p : 
> P), B(p) by picking p : P, then f(p) : A(p), so Q is true. Hence, not not Q 
> is true, meaning it has an element, so g(p) is that element. We then can 
> conclude A = B. By function extensionality, that's equivalent to for all p 
> : P, A (p) = B (p), which gives Q = not not Q. 
>
> Jean
>
> On Tuesday, November 13, 2018 at 3:32:22 PM UTC-5, Martín Hötzel Escardó 
> wrote:
>>
>> Let P be a subsingleton and 𝓤 be a universe, and consider the
>> product map
>>
>>   Π : (P → 𝓤) → 𝓤
>>          A     ↦ Π (p:P), A(p).
>>
>> Is this an embedding? (In the sense of having subsingleton
>> fibers.)
>>
>> It is easy to see that this is the case if P=𝟘 or P=𝟙 (empty or
>> singleton type).
>>
>> But the reasons are fundamentally different:
>>
>> (0) If P=𝟘, the domain of Π is equivalent to 𝟙, and Π amounts to
>>     the map 𝟙 → 𝓤 with constant value 𝟙.
>>
>>     In general, a function 𝟙 → X into a type X is *not* an
>>     embedding. Such a function is an embedding iff it maps the
>>     point of 𝟙 to a point x:X such that the type x=x is a
>>     singleton.
>>
>>     And indeed for X:=𝓤 we have that the type 𝟙=𝟙 is a singleton.
>>
>> (1) If P=𝟙, the domain of Π is equivalent to 𝓤, and Π amounts to
>>     the identity map 𝓤 → 𝓤, which, being an equivalence, is an
>>     embedding.
>>
>> Question. Is there a uniform proof that Π as above for P a
>> subsingleton is an embedding, without considering the case
>> distinction (P=𝟘)+(P=𝟙)?
>>
>> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 12+ messages in thread

* [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-14 10:23   ` Martín Hötzel Escardó
@ 2018-11-14 11:07     ` Paolo Capriotti
  2018-11-14 15:52       ` Michael Shulman
  2018-11-14 19:00       ` Martín Hötzel Escardó
  0 siblings, 2 replies; 12+ messages in thread
From: Paolo Capriotti @ 2018-11-14 11:07 UTC (permalink / raw)
  To: Homotopy Type Theory

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

On Tue, 13 Nov 2018, at 8:32 PM, Martín Hötzel Escardó wrote:
> Let P be a subsingleton and 𝓤 be a universe, and consider the
> product map
>
>   Π : (P → 𝓤) → 𝓤
>          A     ↦ Π (p:P), A(p).
>
> Is this an embedding? (In the sense of having subsingleton
> fibers.)
>
> It is easy to see that this is the case if P=𝟘 or P=𝟙 (empty or
> singleton type).
>
> But the reasons are fundamentally different:
>
> (0) If P=𝟘, the domain of Π is equivalent to 𝟙, and Π amounts to
>     the map 𝟙 → 𝓤 with constant value 𝟙.
>
>     In general, a function 𝟙 → X into a type X is *not* an
>     embedding. Such a function is an embedding iff it maps the
>     point of 𝟙 to a point x:X such that the type x=x is a
>     singleton.
>
>     And indeed for X:=𝓤 we have that the type 𝟙=𝟙 is a singleton.
>
> (1) If P=𝟙, the domain of Π is equivalent to 𝓤, and Π amounts to
>     the identity map 𝓤 → 𝓤, which, being an equivalence, is an
>     embedding.
>
> Question. Is there a uniform proof that Π as above for P a
> subsingleton is an embedding, without considering the case
> distinction (P=𝟘)+(P=𝟙)?

I think one can show that ap Π is an equivalence by giving an inverse. 
Given X, Y : P → 𝓤, first note that the equality type X = Y is equivalent 
by function extensionality to (u : P) → X u = Y u. Since one can prove 
easily that (u : P) → X u = Π X, it follows that X = Y is equivalent to P → 
Π X = Π Y. Hence we get a map ω : Π X = Π Y → X = Y. To show that it is 
indeed an inverse of ap Π, start with some α : Π X = Π Y. By following the 
construction above, we get that ap Π (ω α) maps a function h : Π X to λ u . 
α (λ v . tr^X [u,v] (h u)) u, where [u,v] : u = v is given by the fact that 
P is a proposition. Now, within the assumption u : P, the λ expression in 
brackets is equal to h itself, hence ap Π (ω α) = α. The other composition 
is easier, since it can just be checked on reflexivity.

Best,
Paolo

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 12+ messages in thread

* Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-14 11:07     ` Paolo Capriotti
@ 2018-11-14 15:52       ` Michael Shulman
  2018-11-15 11:05         ` Martín Hötzel Escardó
  2018-11-14 19:00       ` Martín Hötzel Escardó
  1 sibling, 1 reply; 12+ messages in thread
From: Michael Shulman @ 2018-11-14 15:52 UTC (permalink / raw)
  To: Paolo Capriotti; +Cc: HomotopyTypeTheory

Here's a sketch of a more conceptual argument.  Both 𝓤 and P → 𝓤 are
the object-types of (oo-)categories, and Π is the object-map of a
right adjoint functor whose counit is an equivalence.  Thus, by a
standard argument, it is fully faithful, and hence also fully faithful
on equivalences (which, by univalence, are the equalities).  Of course
we can't define the whole oo-categories in Book HoTT, but I think this
is one of those arguments that only needs the 1- or 2-dimensional
structure.
On Wed, Nov 14, 2018 at 3:07 AM Paolo Capriotti <p.capriotti@gmail.com> wrote:
>
> On Tue, 13 Nov 2018, at 8:32 PM, Martín Hötzel Escardó wrote:
> > Let P be a subsingleton and 𝓤 be a universe, and consider the
> > product map
> >
> >   Π : (P → 𝓤) → 𝓤
> >          A     ↦ Π (p:P), A(p).
> >
> > Is this an embedding? (In the sense of having subsingleton
> > fibers.)
> >
> > It is easy to see that this is the case if P=𝟘 or P=𝟙 (empty or
> > singleton type).
> >
> > But the reasons are fundamentally different:
> >
> > (0) If P=𝟘, the domain of Π is equivalent to 𝟙, and Π amounts to
> >     the map 𝟙 → 𝓤 with constant value 𝟙.
> >
> >     In general, a function 𝟙 → X into a type X is *not* an
> >     embedding. Such a function is an embedding iff it maps the
> >     point of 𝟙 to a point x:X such that the type x=x is a
> >     singleton.
> >
> >     And indeed for X:=𝓤 we have that the type 𝟙=𝟙 is a singleton.
> >
> > (1) If P=𝟙, the domain of Π is equivalent to 𝓤, and Π amounts to
> >     the identity map 𝓤 → 𝓤, which, being an equivalence, is an
> >     embedding.
> >
> > Question. Is there a uniform proof that Π as above for P a
> > subsingleton is an embedding, without considering the case
> > distinction (P=𝟘)+(P=𝟙)?
>
> I think one can show that ap Π is an equivalence by giving an inverse. Given X, Y : P → 𝓤, first note that the equality type X = Y is equivalent by function extensionality to (u : P) → X u = Y u. Since one can prove easily that (u : P) → X u = Π X, it follows that X = Y is equivalent to P → Π X = Π Y. Hence we get a map ω : Π X = Π Y → X = Y. To show that it is indeed an inverse of ap Π, start with some α : Π X = Π Y. By following the construction above, we get that ap Π (ω α) maps a function h : Π X to λ u . α (λ v . tr^X [u,v] (h u)) u, where [u,v] : u = v is given by the fact that P is a proposition. Now, within the assumption u : P, the λ expression in brackets is equal to h itself, hence ap Π (ω α) = α. The other composition is easier, since it can just be checked on reflexivity.
>
> Best,
> Paolo
>
> --
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 12+ messages in thread

* [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-14 11:07     ` Paolo Capriotti
  2018-11-14 15:52       ` Michael Shulman
@ 2018-11-14 19:00       ` Martín Hötzel Escardó
  1 sibling, 0 replies; 12+ messages in thread
From: Martín Hötzel Escardó @ 2018-11-14 19:00 UTC (permalink / raw)
  To: Homotopy Type Theory

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

Thanks, Paolo. 

Independently, Mike Shulman had sent me another solution based on modal 
operators off-list. But these two solutions are essentially the same. 

I am glad the answer to the question is positive. 

Maybe I'll explain later why I am interested in this question. 

Best, 
Martin 

On Wednesday, 14 November 2018 11:07:50 UTC, Paolo Capriotti wrote:
>
> On Tue, 13 Nov 2018, at 8:32 PM, Martín Hötzel Escardó wrote:
> > Let P be a subsingleton and 𝓤 be a universe, and consider the
> > product map
> >
> >   Π : (P → 𝓤) → 𝓤
> >          A     ↦ Π (p:P), A(p).
> >
> > Is this an embedding? (In the sense of having subsingleton
> > fibers.)
> >
> > It is easy to see that this is the case if P=𝟘 or P=𝟙 (empty or
> > singleton type).
> >
> > But the reasons are fundamentally different:
> >
> > (0) If P=𝟘, the domain of Π is equivalent to 𝟙, and Π amounts to
> >     the map 𝟙 → 𝓤 with constant value 𝟙.
> >
> >     In general, a function 𝟙 → X into a type X is *not* an
> >     embedding. Such a function is an embedding iff it maps the
> >     point of 𝟙 to a point x:X such that the type x=x is a
> >     singleton.
> >
> >     And indeed for X:=𝓤 we have that the type 𝟙=𝟙 is a singleton.
> >
> > (1) If P=𝟙, the domain of Π is equivalent to 𝓤, and Π amounts to
> >     the identity map 𝓤 → 𝓤, which, being an equivalence, is an
> >     embedding.
> >
> > Question. Is there a uniform proof that Π as above for P a
> > subsingleton is an embedding, without considering the case
> > distinction (P=𝟘)+(P=𝟙)?
>
> I think one can show that ap Π is an equivalence by giving an inverse. 
> Given X, Y : P → 𝓤, first note that the equality type X = Y is equivalent 
> by function extensionality to (u : P) → X u = Y u. Since one can prove 
> easily that (u : P) → X u = Π X, it follows that X = Y is equivalent to P → 
> Π X = Π Y. Hence we get a map ω : Π X = Π Y → X = Y. To show that it is 
> indeed an inverse of ap Π, start with some α : Π X = Π Y. By following the 
> construction above, we get that ap Π (ω α) maps a function h : Π X to λ u . 
> α (λ v . tr^X [u,v] (h u)) u, where [u,v] : u = v is given by the fact that 
> P is a proposition. Now, within the assumption u : P, the λ expression in 
> brackets is equal to h itself, hence ap Π (ω α) = α. The other composition 
> is easier, since it can just be checked on reflexivity.
>
> Best,
> Paolo
>
>

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 12+ messages in thread

* Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-14 15:52       ` Michael Shulman
@ 2018-11-15 11:05         ` Martín Hötzel Escardó
  2018-11-15 19:23           ` Martín Hötzel Escardó
  0 siblings, 1 reply; 12+ messages in thread
From: Martín Hötzel Escardó @ 2018-11-15 11:05 UTC (permalink / raw)
  To: Homotopy Type Theory

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

Here is my take on the independent proofs by Mike and Paolo. My aim in
this version is to avoid calculations as much as possible.

We want to show that the following map s is an embedding:

 s : (P → 𝓤) → 𝓤
 s = Π

Our strategy will be to exhibit s as a composition of an equivalence
followed by something that is clearly an embedding:

  (P → 𝓤) ≃  M ↪ 𝓤

We take M := Σ (X : 𝓤), is-equiv (κ X),
where the function κ X : X → (P → X) is defined by κ x p = x.

The map M ↪ 𝓤 is simply the first projection. It is an embedding
because "being an equivalence" is a proposition.

The equivalence (P → 𝓤) ≃ M is easy. Given A : P → 𝓤 we take X to be
the type s A, with a short argument to show that the map κ(s A) is an
equivalence. Conversely, given X : 𝓤 such that κ X is an equivalence,
we take A to be the constant family (p ↦ X). It is direct and short to
check that this does give an inverse (using function extensionality and 
univalence).

By construction, the map s is the composition of the equivalence
followed by the projection.

Because equivalences are embeddings, and compositions of embeddings
are embeddings, it follows that s is an embedding.

I coded this in Agda here:
http://www.cs.bham.ac.uk/~mhe/agda-new/UF-InjectiveTypes.html#17057

Thanks for your input!

Martin


On Wednesday, 14 November 2018 15:52:45 UTC, Michael Shulman wrote:
>
> Here's a sketch of a more conceptual argument.  Both 𝓤 and P → 𝓤 are 
> the object-types of (oo-)categories, and Π is the object-map of a 
> right adjoint functor whose counit is an equivalence.  Thus, by a 
> standard argument, it is fully faithful, and hence also fully faithful 
> on equivalences (which, by univalence, are the equalities).  Of course 
> we can't define the whole oo-categories in Book HoTT, but I think this 
> is one of those arguments that only needs the 1- or 2-dimensional 
> structure. 
> On Wed, Nov 14, 2018 at 3:07 AM Paolo Capriotti <p.cap...@gmail.com 
> <javascript:>> wrote: 
> > 
> > On Tue, 13 Nov 2018, at 8:32 PM, Martín Hötzel Escardó wrote: 
> > > Let P be a subsingleton and 𝓤 be a universe, and consider the 
> > > product map 
> > > 
> > >   Π : (P → 𝓤) → 𝓤 
> > >          A     ↦ Π (p:P), A(p). 
> > > 
> > > Is this an embedding? (In the sense of having subsingleton 
> > > fibers.) 
> > > 
> > > It is easy to see that this is the case if P=𝟘 or P=𝟙 (empty or 
> > > singleton type). 
> > > 
> > > But the reasons are fundamentally different: 
> > > 
> > > (0) If P=𝟘, the domain of Π is equivalent to 𝟙, and Π amounts to 
> > >     the map 𝟙 → 𝓤 with constant value 𝟙. 
> > > 
> > >     In general, a function 𝟙 → X into a type X is *not* an 
> > >     embedding. Such a function is an embedding iff it maps the 
> > >     point of 𝟙 to a point x:X such that the type x=x is a 
> > >     singleton. 
> > > 
> > >     And indeed for X:=𝓤 we have that the type 𝟙=𝟙 is a singleton. 
> > > 
> > > (1) If P=𝟙, the domain of Π is equivalent to 𝓤, and Π amounts to 
> > >     the identity map 𝓤 → 𝓤, which, being an equivalence, is an 
> > >     embedding. 
> > > 
> > > Question. Is there a uniform proof that Π as above for P a 
> > > subsingleton is an embedding, without considering the case 
> > > distinction (P=𝟘)+(P=𝟙)? 
> > 
> > I think one can show that ap Π is an equivalence by giving an inverse. 
> Given X, Y : P → 𝓤, first note that the equality type X = Y is equivalent 
> by function extensionality to (u : P) → X u = Y u. Since one can prove 
> easily that (u : P) → X u = Π X, it follows that X = Y is equivalent to P → 
> Π X = Π Y. Hence we get a map ω : Π X = Π Y → X = Y. To show that it is 
> indeed an inverse of ap Π, start with some α : Π X = Π Y. By following the 
> construction above, we get that ap Π (ω α) maps a function h : Π X to λ u . 
> α (λ v . tr^X [u,v] (h u)) u, where [u,v] : u = v is given by the fact that 
> P is a proposition. Now, within the assumption u : P, the λ expression in 
> brackets is equal to h itself, hence ap Π (ω α) = α. The other composition 
> is easier, since it can just be checked on reflexivity. 
> > 
> > Best, 
> > Paolo 
> > 
> > -- 
> > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com <javascript:>. 
>
> > For more options, visit https://groups.google.com/d/optout. 
>

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 12+ messages in thread

* Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-15 11:05         ` Martín Hötzel Escardó
@ 2018-11-15 19:23           ` Martín Hötzel Escardó
  2018-11-15 19:29             ` Michael Shulman
  0 siblings, 1 reply; 12+ messages in thread
From: Martín Hötzel Escardó @ 2018-11-15 19:23 UTC (permalink / raw)
  To: Homotopy Type Theory

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



On Thursday, 15 November 2018 11:05:42 UTC, Martín Hötzel Escardó wrote:
>
>
>   (P → 𝓤) ≃  M
>
> We take M := Σ (X : 𝓤), is-equiv (κ X),
> where the function κ X : X → (P → X) is defined by κ x p = x
>

I think something interesting is happening here. We have the "open" 
modality  
P → (-), and the sub-universe M of modal types coincides with the modal
reflection  P → 𝓤 of the universe 𝓤. In particular, this means that the 
sub-universe of modal types is itself a modal type. Has this kind of thing 
been
observed before, for this modality and possibly the classes of modalities 
already considered in the literature?

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 12+ messages in thread

* Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-15 19:23           ` Martín Hötzel Escardó
@ 2018-11-15 19:29             ` Michael Shulman
  2018-11-15 22:26               ` Martín Hötzel Escardó
  0 siblings, 1 reply; 12+ messages in thread
From: Michael Shulman @ 2018-11-15 19:29 UTC (permalink / raw)
  To: Martin Hotzel Escardo; +Cc: HomotopyTypeTheory

Modulo some details about accessibility, the sub-universe of modal
types is a modal type if and only if the modality is left exact.  This
is theorem 3.10 of RSS https://arxiv.org/abs/1706.07526.

However, this sub-universe coinciding with the modal reflection of the
whole universe seems to be something very special about open
modalities.
On Thu, Nov 15, 2018 at 11:23 AM Martín Hötzel Escardó
<escardo.martin@gmail.com> wrote:
>
>
>
> On Thursday, 15 November 2018 11:05:42 UTC, Martín Hötzel Escardó wrote:
>>
>>
>>   (P → 𝓤) ≃  M
>>
>> We take M := Σ (X : 𝓤), is-equiv (κ X),
>> where the function κ X : X → (P → X) is defined by κ x p = x
>
>
> I think something interesting is happening here. We have the "open" modality
> P → (-), and the sub-universe M of modal types coincides with the modal
> reflection  P → 𝓤 of the universe 𝓤. In particular, this means that the
> sub-universe of modal types is itself a modal type. Has this kind of thing been
> observed before, for this modality and possibly the classes of modalities
> already considered in the literature?
>
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 12+ messages in thread

* Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-15 19:29             ` Michael Shulman
@ 2018-11-15 22:26               ` Martín Hötzel Escardó
  2018-11-15 23:38                 ` Michael Shulman
  0 siblings, 1 reply; 12+ messages in thread
From: Martín Hötzel Escardó @ 2018-11-15 22:26 UTC (permalink / raw)
  To: Homotopy Type Theory

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



On Thursday, 15 November 2018 19:30:08 UTC, Michael Shulman wrote:
>
> However, this sub-universe coinciding with the modal reflection of the 
> whole universe seems to be something very special about open 
> modalities. 
>

We may consider the dual question of whether Σ is an embedding:

 s : (P → 𝓤) → 𝓤
 s = Σ

This is again a section of the same retraction r : 𝓤 → (P → 𝓤) defined
by

 r X p = X.

This time we have that the idempotent s ∘ r satisfies

 s (r X) = P × X

definitionally.

So consider the projection κ : (X : 𝓤) → s (r X) → X
and the sub-universe determined by this co-modal operator P × (-):

 C := Σ \(X : 𝓤) → is-equiv (κ X)

Then again we have a definitional factorization of s as

 (P → 𝓤) ≃ C ↪ 𝓤,

where the embedding is the projection, showing that s = Σ is an
embedding too, and that M ≃ C, even though the fixed points of P → (-)
and P × (-) are quite different if e.g. P = 𝟘.

So the subuniverse of P × (-) - co-modal types coincides with the
P → (-) - modal reflection of the universe.

(I coded this in Agda to be sure this is not an evening mirage,
available at the same place. The proof was produced by copy and paste
of the previous one, with very few modifications.)

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 12+ messages in thread

* Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?
  2018-11-15 22:26               ` Martín Hötzel Escardó
@ 2018-11-15 23:38                 ` Michael Shulman
  0 siblings, 0 replies; 12+ messages in thread
From: Michael Shulman @ 2018-11-15 23:38 UTC (permalink / raw)
  To: Martin Hotzel Escardo; +Cc: HomotopyTypeTheory

I remember noticing before that the P x (-) co-modal types coincide
with the P -> (-) modal ones.  In topos-theoretic language, these
common sub-universes are the slice category E/P, which is related to E
by an essential geometric embedding, hence an adjoint triple i_! -|
i^* -| i_* in which both i_! and i_* are fully faithful.  The left
adjoint i_! embeds E/P as the P x (-) co-modal types, while the right
adjoint i_* embeds it as the P -> (-) modal ones.
On Thu, Nov 15, 2018 at 2:26 PM Martín Hötzel Escardó
<escardo.martin@gmail.com> wrote:
>
>
>
> On Thursday, 15 November 2018 19:30:08 UTC, Michael Shulman wrote:
>>
>> However, this sub-universe coinciding with the modal reflection of the
>> whole universe seems to be something very special about open
>> modalities.
>
>
> We may consider the dual question of whether Σ is an embedding:
>
>  s : (P → 𝓤) → 𝓤
>  s = Σ
>
> This is again a section of the same retraction r : 𝓤 → (P → 𝓤) defined
> by
>
>  r X p = X.
>
> This time we have that the idempotent s ∘ r satisfies
>
>  s (r X) = P × X
>
> definitionally.
>
> So consider the projection κ : (X : 𝓤) → s (r X) → X
> and the sub-universe determined by this co-modal operator P × (-):
>
>  C := Σ \(X : 𝓤) → is-equiv (κ X)
>
> Then again we have a definitional factorization of s as
>
>  (P → 𝓤) ≃ C ↪ 𝓤,
>
> where the embedding is the projection, showing that s = Σ is an
> embedding too, and that M ≃ C, even though the fixed points of P → (-)
> and P × (-) are quite different if e.g. P = 𝟘.
>
> So the subuniverse of P × (-) - co-modal types coincides with the
> P → (-) - modal reflection of the universe.
>
> (I coded this in Agda to be sure this is not an evening mirage,
> available at the same place. The proof was produced by copy and paste
> of the previous one, with very few modifications.)
>
> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 12+ messages in thread

end of thread, back to index

Thread overview: 12+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-11-13 20:32 [HoTT] Proof that something is an embedding without assuming excluded middle? Martín Hötzel Escardó
2018-11-13 20:36 ` [HoTT] " Martín Hötzel Escardó
2018-11-13 23:47 ` Jean Joseph
2018-11-14 10:23   ` Martín Hötzel Escardó
2018-11-14 11:07     ` Paolo Capriotti
2018-11-14 15:52       ` Michael Shulman
2018-11-15 11:05         ` Martín Hötzel Escardó
2018-11-15 19:23           ` Martín Hötzel Escardó
2018-11-15 19:29             ` Michael Shulman
2018-11-15 22:26               ` Martín Hötzel Escardó
2018-11-15 23:38                 ` Michael Shulman
2018-11-14 19:00       ` Martín Hötzel Escardó

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox