[HoTT] Proof that something is an embedding without assuming excluded middle?mailto:homotopytypetheory@googlegroups.com2019-07-18T12:21:43ZMartín Hötzel Escardóescardo.martin@gmail.com[HoTT] Proof that something is an embedding without assuming excluded middle?2018-11-13T20:32:26Zurn:uuid:0f4bd653-305d-307f-54a2-76dbdce930ca
```[-- 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.

[-- Attachment #1.2: Type: text/html, Size: 1972 bytes --]
```
Martín Hötzel Escardóescardo.martin@gmail.com[HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-13T20:36:35Zurn:uuid:675a8666-fc3b-b23f-03ef-1bd0a562e6af
```[-- 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.

[-- Attachment #1.2: Type: text/html, Size: 2295 bytes --]
```
Jean Josephjsjean00@gmail.com[HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-13T23:47:42Zurn:uuid:5a3984d7-09d2-44b0-2995-70a7a755b722
```[-- 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.

[-- Attachment #1.2: Type: text/html, Size: 2901 bytes --]
```
Martín Hötzel Escardóescardo.martin@gmail.com[HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-14T10:23:40Zurn:uuid:d0f0a1a8-0895-3883-baf8-8fafb7ba7a48
```[-- 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.

[-- Attachment #1.2: Type: text/html, Size: 4337 bytes --]
```
Paolo Capriottip.capriotti@gmail.com[HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-14T11:07:52Zurn:uuid:dd343ce0-d589-0648-6592-8eb29e9faf39
```[-- 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.

[-- Attachment #1.2: Type: text/html, Size: 3038 bytes --]
```
Michael Shulmanshulman@sandiego.eduRe: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-14T15:52:46Zurn:uuid:f4f01b07-1683-dc1c-91d8-c06dd9be3ff8
```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.
```
Martín Hötzel Escardóescardo.martin@gmail.com[HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-14T19:00:34Zurn:uuid:18e73dc7-67e9-0cab-d6be-c6bd673fd882
```[-- 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.

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.

[-- Attachment #1.2: Type: text/html, Size: 3621 bytes --]
```
Martín Hötzel Escardóescardo.martin@gmail.comRe: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-15T11:05:46Zurn:uuid:febb4582-8f9a-db7d-7d7d-e031e308f2a3
```[-- 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

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.

[-- Attachment #1.2: Type: text/html, Size: 6676 bytes --]
```
Martín Hötzel Escardóescardo.martin@gmail.comRe: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-15T19:23:23Zurn:uuid:c08cc364-e976-9d3b-f263-71a2b4927285
```[-- 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

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.

[-- Attachment #1.2: Type: text/html, Size: 1486 bytes --]
```
Michael Shulmanshulman@sandiego.eduRe: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-15T19:30:09Zurn:uuid:090b0248-64b6-07bb-87e7-92864bc05dbb
```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.
```
Martín Hötzel Escardóescardo.martin@gmail.comRe: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-15T22:26:45Zurn:uuid:a77e9260-7896-6d0a-2540-56b467a817d4
```[-- 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.

[-- Attachment #1.2: Type: text/html, Size: 2373 bytes --]
```
Michael Shulmanshulman@sandiego.eduRe: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?2018-11-15T23:38:30Zurn:uuid:c3ae1e7b-3f7d-ca12-b9e1-919c11272b1d
```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.