[-- 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 --]

[-- 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 --]

[-- 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 --]

[-- 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 --]

[-- 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 --]

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.

[-- 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 --]

[-- 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 --]

[-- 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 --]

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.

[-- 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 --]

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.