* Conjecture @ 2017-03-27 21:57 Martin Escardo 2017-03-29 21:08 ` [HoTT] Conjecture Nicolai Kraus 2017-04-03 0:35 ` Conjecture Daniel R. Grayson 0 siblings, 2 replies; 22+ messages in thread From: Martin Escardo @ 2017-03-27 21:57 UTC (permalink / raw) To: HomotopyT...@googlegroups.com This is a question I would like to see eventually answered. I posed it a few years ago in a conference (and privately among some of you), but I would like to have it here in this list for the record. Definition. A modulus of constancy for a function f:X->Y is a function (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli of constancy, but if Y is a set then it can have at most one.) We know that if Y is a set and f comes with a modulus of constancy, then f factors through |-|: X -> ||Y||, meaning that we can exhibit an f':||X||->Y with f'|x| = f(x). Conjecture. If for all types X and Y and all functions f:X->Y equipped with a modulus of constancy we can exhibit f':||X||->Y with f'|x| = f(x), then all types are sets. For this conjecture, I assume function extensionality and propositional extensionality, but not (general) univalence. But feel free to play with the assumptions. Martin ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-03-27 21:57 Conjecture Martin Escardo @ 2017-03-29 21:08 ` Nicolai Kraus 2017-03-29 22:05 ` Martin Escardo 2017-04-03 0:35 ` Conjecture Daniel R. Grayson 1 sibling, 1 reply; 22+ messages in thread From: Nicolai Kraus @ 2017-03-29 21:08 UTC (permalink / raw) To: Martin Escardo, HomotopyT...@googlegroups.com Hi Martin, I also would like to know the answer to this conjecture. I am not sure whether I expect that it holds in the quite minimalistic setting that you suggested (but of course we know that the premise of the conjecture is inconsistent in "full HoTT" by Mike's argument). Here is a small thought. Let's allow the innocent-looking HIT which we can write as {-}, known as "generalised circle" or "pseudo truncation" or "1-step truncation", where {X} has constructors [-] : X -> {X} and c : (x y : X) -> [x] = [y]. Then, from the premise of your conjecture, it follows that every {X} has split support, which looks a bit suspicious. I don't know whether you can get anything out of this idea (especially without univalence). But it would certainly be enough to show that every such {X} is a set, since then in particular {1} aka S^1 would be a set, and consequently every type. Nicolai On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote: > This is a question I would like to see eventually answered. > > I posed it a few years ago in a conference (and privately among some of > you), but I would like to have it here in this list for the record. > > Definition. A modulus of constancy for a function f:X->Y is a function > (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli > of constancy, but if Y is a set then it can have at most one.) > > We know that if Y is a set and f comes with a modulus of constancy, then > f factors through |-|: X -> ||Y||, meaning that we can exhibit an > f':||X||->Y with f'|x| = f(x). > > Conjecture. If for all types X and Y and all functions f:X->Y equipped > with a modulus of constancy we can exhibit f':||X||->Y with f'|x| = > f(x), then all types are sets. > > For this conjecture, I assume function extensionality and propositional > extensionality, but not (general) univalence. But feel free to play with > the assumptions. > > Martin > ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-03-29 21:08 ` [HoTT] Conjecture Nicolai Kraus @ 2017-03-29 22:05 ` Martin Escardo 2017-03-30 10:59 ` Michael Shulman 2017-03-30 22:49 ` Nicolai Kraus 0 siblings, 2 replies; 22+ messages in thread From: Martin Escardo @ 2017-03-29 22:05 UTC (permalink / raw) To: HomotopyT...@googlegroups.com Thanks, Nicolai. I don't have anything to add to your remarks. But here is an example where the factorization of constant functions is possible and gives something interesting/useful, whose formulation doesn't refer to constant functions or factorizations. (This is part of joint work with Cory Knapp.) For a type X, define its type of partial elements to be LX := Sigma(P:U), isProp P * (P->X). If X is a set, then LX is a directed-complete partially ordered set (with a minimal element). This claim is proved using the factorization of constant functions through the propositional truncation of their domains, where the codomains are sets, as follows. The order is defined (in the obvious way) by (P:U,-,f:P->X) <= (Q:U,-,g:Q->X) := Sigma(t:P->Q), Pi(p:P), f(p)=g(t(p)). (Where you use the blanks "-" and the assumption that X is a set to show that this is a partial order.) Now, given a directed family (P_i,-,f_i:P_i->X), we want to construct its least upper bound. Its extent of definition is the proposition ||Sigma_i, P_i||, and the question is how we define f:||Sigma_i, P_i||->X. We know how to define f':(Sigma_i, P_i)->X from the f_i's (by the universal property of Sigma). But X is not a proposition, and hence we can't add ||-|| to f' to get f using the universal property of ||-||. But we can show that f' is constant from the assumption of directedness, and then get the desired f:||Sigma_i, P_i||->X by the factorization property, using the assumption that X is a set. Then the remaining details are routine. What if X is not a set? Then we won't get a partial order, but still we may wish to ask whether the resulting category-like structure has filtered colimits in a suitable sense. But when trying to do this, we stumble on the fact that the factorization used in the above construction won't be available in general when X is not a set. So, in addition to the conjecture, I would also like to know (independently of the above example), *precisely when* the factorization through ||-|| is possible for a function with a given modulus of constancy. (I've come across of a number of examples where such factorizations of constant functions proved useful. Perhaps others have too? I'd like to know.) Best, Martin On 29/03/17 22:08, Nicolai Kraus wrote: > Hi Martin, I also would like to know the answer to this conjecture. > I am not sure whether I expect that it holds in the quite minimalistic > setting that you suggested (but of course we know that the premise of > the conjecture is inconsistent in "full HoTT" by Mike's argument). > > Here is a small thought. Let's allow the innocent-looking HIT which we > can write as {-}, known as "generalised circle" or "pseudo truncation" > or "1-step truncation", where {X} has constructors > [-] : X -> {X} and c : (x y : X) -> [x] = [y]. > Then, from the premise of your conjecture, it follows that every {X} > has split support, which looks a bit suspicious. I don't know whether > you can get anything out of this idea (especially without univalence). > But it would certainly be enough to show that every such {X} is a set, > since then in particular {1} aka S^1 would be a set, and consequently > every type. > > Nicolai > > > On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote: >> This is a question I would like to see eventually answered. >> >> I posed it a few years ago in a conference (and privately among some of >> you), but I would like to have it here in this list for the record. >> >> Definition. A modulus of constancy for a function f:X->Y is a function >> (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli >> of constancy, but if Y is a set then it can have at most one.) >> >> We know that if Y is a set and f comes with a modulus of constancy, then >> f factors through |-|: X -> ||Y||, meaning that we can exhibit an >> f':||X||->Y with f'|x| = f(x). >> >> Conjecture. If for all types X and Y and all functions f:X->Y equipped >> with a modulus of constancy we can exhibit f':||X||->Y with f'|x| = >> f(x), then all types are sets. >> >> For this conjecture, I assume function extensionality and propositional >> extensionality, but not (general) univalence. But feel free to play with >> the assumptions. >> >> Martin >> > ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-03-29 22:05 ` Martin Escardo @ 2017-03-30 10:59 ` Michael Shulman 2017-03-30 19:22 ` Egbert Rijke 2017-03-30 22:49 ` Nicolai Kraus 1 sibling, 1 reply; 22+ messages in thread From: Michael Shulman @ 2017-03-30 10:59 UTC (permalink / raw) To: Martin Escardo; +Cc: HomotopyT...@googlegroups.com Note that Nicolai (http://www.cs.nott.ac.uk/~psznk/docs/pseudotruncations.pdf), Floris (arXiv:1512.02274), and Egbert (arXiv:1701.07538) have all recently given (different) constructions of ||-|| in terms of a sequential colimit of nonrecursive HITs. Each of those constructions gives an answer to "precisely when the factorization through ||-|| is possible". On Wed, Mar 29, 2017 at 6:05 PM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> wrote: > Thanks, Nicolai. I don't have anything to add to your remarks. > > But here is an example where the factorization of constant functions > is possible and gives something interesting/useful, whose formulation > doesn't refer to constant functions or factorizations. > > (This is part of joint work with Cory Knapp.) > > For a type X, define its type of partial elements to be > > LX := Sigma(P:U), isProp P * (P->X). > > If X is a set, then LX is a directed-complete partially ordered set > (with a minimal element). > > This claim is proved using the factorization of constant functions > through the propositional truncation of their domains, where the > codomains are sets, as follows. > > The order is defined (in the obvious way) by > > (P:U,-,f:P->X) <= (Q:U,-,g:Q->X) > > := Sigma(t:P->Q), Pi(p:P), f(p)=g(t(p)). > > (Where you use the blanks "-" and the assumption that X is a set to > show that this is a partial order.) > > Now, given a directed family (P_i,-,f_i:P_i->X), we want to construct > its least upper bound. > > Its extent of definition is the proposition ||Sigma_i, P_i||, and the > question is how we define > > f:||Sigma_i, P_i||->X. > > We know how to define > > f':(Sigma_i, P_i)->X > > from the f_i's (by the universal property of Sigma). But X is not a > proposition, and hence we can't add ||-|| to f' to get f using the > universal property of ||-||. > > But we can show that f' is constant from the assumption of > directedness, and then get the desired f:||Sigma_i, P_i||->X by the > factorization property, using the assumption that X is a set. Then the > remaining details are routine. > > What if X is not a set? Then we won't get a partial order, but still > we may wish to ask whether the resulting category-like structure has > filtered colimits in a suitable sense. But when trying to do this, we > stumble on the fact that the factorization used in the above > construction won't be available in general when X is not a set. > > So, in addition to the conjecture, I would also like to know > (independently of the above example), *precisely when* the > factorization through ||-|| is possible for a function with a given > modulus of constancy. > > (I've come across of a number of examples where such factorizations of > constant functions proved useful. Perhaps others have too? I'd like to > know.) > > Best, > Martin > > > > On 29/03/17 22:08, Nicolai Kraus wrote: >> Hi Martin, I also would like to know the answer to this conjecture. >> I am not sure whether I expect that it holds in the quite minimalistic >> setting that you suggested (but of course we know that the premise of >> the conjecture is inconsistent in "full HoTT" by Mike's argument). >> >> Here is a small thought. Let's allow the innocent-looking HIT which we >> can write as {-}, known as "generalised circle" or "pseudo truncation" >> or "1-step truncation", where {X} has constructors >> [-] : X -> {X} and c : (x y : X) -> [x] = [y]. >> Then, from the premise of your conjecture, it follows that every {X} >> has split support, which looks a bit suspicious. I don't know whether >> you can get anything out of this idea (especially without univalence). >> But it would certainly be enough to show that every such {X} is a set, >> since then in particular {1} aka S^1 would be a set, and consequently >> every type. >> >> Nicolai >> >> >> On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote: >>> This is a question I would like to see eventually answered. >>> >>> I posed it a few years ago in a conference (and privately among some of >>> you), but I would like to have it here in this list for the record. >>> >>> Definition. A modulus of constancy for a function f:X->Y is a function >>> (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli >>> of constancy, but if Y is a set then it can have at most one.) >>> >>> We know that if Y is a set and f comes with a modulus of constancy, then >>> f factors through |-|: X -> ||Y||, meaning that we can exhibit an >>> f':||X||->Y with f'|x| = f(x). >>> >>> Conjecture. If for all types X and Y and all functions f:X->Y equipped >>> with a modulus of constancy we can exhibit f':||X||->Y with f'|x| = >>> f(x), then all types are sets. >>> >>> For this conjecture, I assume function extensionality and propositional >>> extensionality, but not (general) univalence. But feel free to play with >>> the assumptions. >>> >>> Martin >>> >> > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-03-30 10:59 ` Michael Shulman @ 2017-03-30 19:22 ` Egbert Rijke 2017-03-30 23:02 ` Nicolai Kraus 0 siblings, 1 reply; 22+ messages in thread From: Egbert Rijke @ 2017-03-30 19:22 UTC (permalink / raw) To: Michael Shulman; +Cc: Martin Escardo, HomotopyT...@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 6583 bytes --] There seems to be a coherence condition missing in the conjecture: it would be natural to say that the precomposition map (||X|| -> Y) -> ({X} -> Y), or equivalently the canonical map (||X|| -> Y) -> (Sigma (f : X -> Y). Pi (x,y:X). fx = fy) has a section (or even is an equivalence), but in that case we would also have to assume that the homotopy Pi (x,y :X). fx = fy is compatible with the action on paths of the map ||X|| -> Y. Is it intentional that this coherence is missing from the conjecture? Best, Egbert On Thu, Mar 30, 2017 at 6:59 AM, Michael Shulman <shu...@sandiego.edu> wrote: > Note that Nicolai > (http://www.cs.nott.ac.uk/~psznk/docs/pseudotruncations.pdf), Floris > (arXiv:1512.02274), and Egbert (arXiv:1701.07538) have all recently > given (different) constructions of ||-|| in terms of a sequential > colimit of nonrecursive HITs. Each of those constructions gives an > answer to "precisely when the factorization through ||-|| is > possible". > > On Wed, Mar 29, 2017 at 6:05 PM, 'Martin Escardo' via Homotopy Type > Theory <HomotopyT...@googlegroups.com> wrote: > > Thanks, Nicolai. I don't have anything to add to your remarks. > > > > But here is an example where the factorization of constant functions > > is possible and gives something interesting/useful, whose formulation > > doesn't refer to constant functions or factorizations. > > > > (This is part of joint work with Cory Knapp.) > > > > For a type X, define its type of partial elements to be > > > > LX := Sigma(P:U), isProp P * (P->X). > > > > If X is a set, then LX is a directed-complete partially ordered set > > (with a minimal element). > > > > This claim is proved using the factorization of constant functions > > through the propositional truncation of their domains, where the > > codomains are sets, as follows. > > > > The order is defined (in the obvious way) by > > > > (P:U,-,f:P->X) <= (Q:U,-,g:Q->X) > > > > := Sigma(t:P->Q), Pi(p:P), f(p)=g(t(p)). > > > > (Where you use the blanks "-" and the assumption that X is a set to > > show that this is a partial order.) > > > > Now, given a directed family (P_i,-,f_i:P_i->X), we want to construct > > its least upper bound. > > > > Its extent of definition is the proposition ||Sigma_i, P_i||, and the > > question is how we define > > > > f:||Sigma_i, P_i||->X. > > > > We know how to define > > > > f':(Sigma_i, P_i)->X > > > > from the f_i's (by the universal property of Sigma). But X is not a > > proposition, and hence we can't add ||-|| to f' to get f using the > > universal property of ||-||. > > > > But we can show that f' is constant from the assumption of > > directedness, and then get the desired f:||Sigma_i, P_i||->X by the > > factorization property, using the assumption that X is a set. Then the > > remaining details are routine. > > > > What if X is not a set? Then we won't get a partial order, but still > > we may wish to ask whether the resulting category-like structure has > > filtered colimits in a suitable sense. But when trying to do this, we > > stumble on the fact that the factorization used in the above > > construction won't be available in general when X is not a set. > > > > So, in addition to the conjecture, I would also like to know > > (independently of the above example), *precisely when* the > > factorization through ||-|| is possible for a function with a given > > modulus of constancy. > > > > (I've come across of a number of examples where such factorizations of > > constant functions proved useful. Perhaps others have too? I'd like to > > know.) > > > > Best, > > Martin > > > > > > > > On 29/03/17 22:08, Nicolai Kraus wrote: > >> Hi Martin, I also would like to know the answer to this conjecture. > >> I am not sure whether I expect that it holds in the quite minimalistic > >> setting that you suggested (but of course we know that the premise of > >> the conjecture is inconsistent in "full HoTT" by Mike's argument). > >> > >> Here is a small thought. Let's allow the innocent-looking HIT which we > >> can write as {-}, known as "generalised circle" or "pseudo truncation" > >> or "1-step truncation", where {X} has constructors > >> [-] : X -> {X} and c : (x y : X) -> [x] = [y]. > >> Then, from the premise of your conjecture, it follows that every {X} > >> has split support, which looks a bit suspicious. I don't know whether > >> you can get anything out of this idea (especially without univalence). > >> But it would certainly be enough to show that every such {X} is a set, > >> since then in particular {1} aka S^1 would be a set, and consequently > >> every type. > >> > >> Nicolai > >> > >> > >> On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote: > >>> This is a question I would like to see eventually answered. > >>> > >>> I posed it a few years ago in a conference (and privately among some of > >>> you), but I would like to have it here in this list for the record. > >>> > >>> Definition. A modulus of constancy for a function f:X->Y is a function > >>> (x,y:X)->f(x)=f(y). (Such a function can have zero, one or more moduli > >>> of constancy, but if Y is a set then it can have at most one.) > >>> > >>> We know that if Y is a set and f comes with a modulus of constancy, > then > >>> f factors through |-|: X -> ||Y||, meaning that we can exhibit an > >>> f':||X||->Y with f'|x| = f(x). > >>> > >>> Conjecture. If for all types X and Y and all functions f:X->Y equipped > >>> with a modulus of constancy we can exhibit f':||X||->Y with f'|x| = > >>> f(x), then all types are sets. > >>> > >>> For this conjecture, I assume function extensionality and propositional > >>> extensionality, but not (general) univalence. But feel free to play > with > >>> the assumptions. > >>> > >>> Martin > >>> > >> > > > > -- > > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- egbertrijke.com [-- Attachment #2: Type: text/html, Size: 8752 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-03-30 19:22 ` Egbert Rijke @ 2017-03-30 23:02 ` Nicolai Kraus 0 siblings, 0 replies; 22+ messages in thread From: Nicolai Kraus @ 2017-03-30 23:02 UTC (permalink / raw) To: Egbert Rijke, Michael Shulman Cc: Martin Escardo, HomotopyT...@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 8417 bytes --] Egbert, this map becomes an equivalence if you add a tower of coherences to the codomain (by arXiv:1411.2682), I don't see a simple single coherence that you can reasonably add - what do you have in mind? What do you mean by "the homotopy is compatible with the action on paths"? Nicolai On 30/03/17 20:22, Egbert Rijke wrote: > There seems to be a coherence condition missing in the conjecture: it > would be natural to say that the precomposition map > > (||X|| -> Y) -> ({X} -> Y), > > or equivalently the canonical map > > (||X|| -> Y) -> (Sigma (f : X -> Y). Pi (x,y:X). fx = fy) > > has a section (or even is an equivalence), but in that case we would > also have to assume that the homotopy Pi (x,y :X). fx = fy is > compatible with the action on paths of the map ||X|| -> Y. > > Is it intentional that this coherence is missing from the conjecture? > > Best, > Egbert > > On Thu, Mar 30, 2017 at 6:59 AM, Michael Shulman <shu...@sandiego.edu > <mailto:shu...@sandiego.edu>> wrote: > > Note that Nicolai > (http://www.cs.nott.ac.uk/~psznk/docs/pseudotruncations.pdf > <http://www.cs.nott.ac.uk/%7Epsznk/docs/pseudotruncations.pdf>), > Floris > (arXiv:1512.02274), and Egbert (arXiv:1701.07538) have all recently > given (different) constructions of ||-|| in terms of a sequential > colimit of nonrecursive HITs. Each of those constructions gives an > answer to "precisely when the factorization through ||-|| is > possible". > > On Wed, Mar 29, 2017 at 6:05 PM, 'Martin Escardo' via Homotopy Type > Theory <HomotopyT...@googlegroups.com > <mailto:HomotopyT...@googlegroups.com>> wrote: > > Thanks, Nicolai. I don't have anything to add to your remarks. > > > > But here is an example where the factorization of constant functions > > is possible and gives something interesting/useful, whose > formulation > > doesn't refer to constant functions or factorizations. > > > > (This is part of joint work with Cory Knapp.) > > > > For a type X, define its type of partial elements to be > > > > LX := Sigma(P:U), isProp P * (P->X). > > > > If X is a set, then LX is a directed-complete partially ordered set > > (with a minimal element). > > > > This claim is proved using the factorization of constant functions > > through the propositional truncation of their domains, where the > > codomains are sets, as follows. > > > > The order is defined (in the obvious way) by > > > > (P:U,-,f:P->X) <= (Q:U,-,g:Q->X) > > > > := Sigma(t:P->Q), Pi(p:P), f(p)=g(t(p)). > > > > (Where you use the blanks "-" and the assumption that X is a set to > > show that this is a partial order.) > > > > Now, given a directed family (P_i,-,f_i:P_i->X), we want to > construct > > its least upper bound. > > > > Its extent of definition is the proposition ||Sigma_i, P_i||, > and the > > question is how we define > > > > f:||Sigma_i, P_i||->X. > > > > We know how to define > > > > f':(Sigma_i, P_i)->X > > > > from the f_i's (by the universal property of Sigma). But X is not a > > proposition, and hence we can't add ||-|| to f' to get f using the > > universal property of ||-||. > > > > But we can show that f' is constant from the assumption of > > directedness, and then get the desired f:||Sigma_i, P_i||->X by the > > factorization property, using the assumption that X is a set. > Then the > > remaining details are routine. > > > > What if X is not a set? Then we won't get a partial order, but still > > we may wish to ask whether the resulting category-like structure has > > filtered colimits in a suitable sense. But when trying to do > this, we > > stumble on the fact that the factorization used in the above > > construction won't be available in general when X is not a set. > > > > So, in addition to the conjecture, I would also like to know > > (independently of the above example), *precisely when* the > > factorization through ||-|| is possible for a function with a given > > modulus of constancy. > > > > (I've come across of a number of examples where such > factorizations of > > constant functions proved useful. Perhaps others have too? I'd > like to > > know.) > > > > Best, > > Martin > > > > > > > > On 29/03/17 22:08, Nicolai Kraus wrote: > >> Hi Martin, I also would like to know the answer to this conjecture. > >> I am not sure whether I expect that it holds in the quite > minimalistic > >> setting that you suggested (but of course we know that the > premise of > >> the conjecture is inconsistent in "full HoTT" by Mike's argument). > >> > >> Here is a small thought. Let's allow the innocent-looking HIT > which we > >> can write as {-}, known as "generalised circle" or "pseudo > truncation" > >> or "1-step truncation", where {X} has constructors > >> [-] : X -> {X} and c : (x y : X) -> [x] = [y]. > >> Then, from the premise of your conjecture, it follows that > every {X} > >> has split support, which looks a bit suspicious. I don't know > whether > >> you can get anything out of this idea (especially without > univalence). > >> But it would certainly be enough to show that every such {X} is > a set, > >> since then in particular {1} aka S^1 would be a set, and > consequently > >> every type. > >> > >> Nicolai > >> > >> > >> On 27/03/17 22:57, 'Martin Escardo' via Homotopy Type Theory wrote: > >>> This is a question I would like to see eventually answered. > >>> > >>> I posed it a few years ago in a conference (and privately > among some of > >>> you), but I would like to have it here in this list for the > record. > >>> > >>> Definition. A modulus of constancy for a function f:X->Y is a > function > >>> (x,y:X)->f(x)=f(y). (Such a function can have zero, one or > more moduli > >>> of constancy, but if Y is a set then it can have at most one.) > >>> > >>> We know that if Y is a set and f comes with a modulus of > constancy, then > >>> f factors through |-|: X -> ||Y||, meaning that we can exhibit an > >>> f':||X||->Y with f'|x| = f(x). > >>> > >>> Conjecture. If for all types X and Y and all functions f:X->Y > equipped > >>> with a modulus of constancy we can exhibit f':||X||->Y with > f'|x| = > >>> f(x), then all types are sets. > >>> > >>> For this conjecture, I assume function extensionality and > propositional > >>> extensionality, but not (general) univalence. But feel free to > play with > >>> the assumptions. > >>> > >>> Martin > >>> > >> > > > > -- > > You received this message because you are subscribed to the > Google Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from > it, send an email to > HomotopyTypeThe...@googlegroups.com > <mailto:HomotopyTypeTheo...@googlegroups.com>. > > For more options, visit https://groups.google.com/d/optout > <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 HomotopyTypeThe...@googlegroups.com > <mailto:HomotopyTypeTheo...@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout > <https://groups.google.com/d/optout>. > > > > > -- > egbertrijke.com <https://egbertrijke.com/> > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeThe...@googlegroups.com > <mailto:HomotopyTypeThe...@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 14193 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-03-29 22:05 ` Martin Escardo 2017-03-30 10:59 ` Michael Shulman @ 2017-03-30 22:49 ` Nicolai Kraus 2017-03-31 16:09 ` Martin Escardo 1 sibling, 1 reply; 22+ messages in thread From: Nicolai Kraus @ 2017-03-30 22:49 UTC (permalink / raw) To: Martin Escardo, HomotopyT...@googlegroups.com Interesting construction by Cory and you! And I think I can help you with the factorisation that you asked for, as follows: On 29/03/17 23:05, 'Martin Escardo' via Homotopy Type Theory wrote: > Now, given a directed family (P_i,-,f_i:P_i->X), we want to construct > its least upper bound. > > Its extent of definition is the proposition ||Sigma_i, P_i||, and the > question is how we define > > f:||Sigma_i, P_i||->X. > > We know how to define > > f':(Sigma_i, P_i)->X > > [...] > > What if X is not a set? (I assume that it is i : Nat in the above.) We can construct the proof of constancy for f' by only going "steps of length 1", i.e. we do it only using the equality proofs of the form f'(i,_) = f'(i+1,_). This constancy proof is coherent up to whichever level you want. By arXiv:1411.2682 Thm 10.5, this means that you can replace the condition "X is a set" by "X is 1-truncated" or "X is 17-truncated" or any finite number you want (this uses funext, but nothing else). With a different strategy, we can do better and drop all assumptions on X. Given this family (P_i, -, f_i), we can define the HIT R with constructors r : (i : Nat) -> P_i -> R s : (i : Nat) -> (p : P_i) -> (r i p) = (r (i+1) (t i p) (where t i : P_i -> P_{i+1} comes from the proof that the family is directed). Now, we can show that R is a proposition. (One way is this: To show R -> isContr(R), we can assume that we are given (r i p : R), and we can prove that this is a centre of contraction.) R is equivalent to ||Sigma_i, P_i||, and it's easy to construct R -> X. Best, Nicolai ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-03-30 22:49 ` Nicolai Kraus @ 2017-03-31 16:09 ` Martin Escardo 2017-04-05 19:37 ` Martin Escardo 0 siblings, 1 reply; 22+ messages in thread From: Martin Escardo @ 2017-03-31 16:09 UTC (permalink / raw) To: HomotopyT...@googlegroups.com On 30/03/17 23:49, Nicolai Kraus wrote: > Interesting construction by Cory and you! And I think I can help > you with the factorisation that you asked for, as follows: Thanks for this, Nicolai. Cory and I a battling against the clock to get our submission ready for a conference. I'll continue the discussion after that. Best, Martin ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-03-31 16:09 ` Martin Escardo @ 2017-04-05 19:37 ` Martin Escardo 2017-04-06 0:23 ` Jon Sterling 0 siblings, 1 reply; 22+ messages in thread From: Martin Escardo @ 2017-04-05 19:37 UTC (permalink / raw) To: HomotopyT...@googlegroups.com On 31/03/17 17:09, 'Martin Escardo' via Homotopy Type Theory wrote: > > > On 30/03/17 23:49, Nicolai Kraus wrote: >> Interesting construction by Cory and you! And I think I can help >> you with the factorisation that you asked for, as follows: > > Thanks for this, Nicolai. > > Cory and I a battling against the clock to get our submission ready for > a conference. I'll continue the discussion after that. I may as well give a link to the paper now that we have finished and submitted it, which is about partial functions in univalent type theory: http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf The conjecture in the initial message of this thread goes well beyond this, and is even unrelated. But I am still very interested in the conjecture independently of any use of it. Martin ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-04-05 19:37 ` Martin Escardo @ 2017-04-06 0:23 ` Jon Sterling 2017-04-06 5:55 ` Martin Escardo 2017-04-06 11:52 ` Thomas Streicher 0 siblings, 2 replies; 22+ messages in thread From: Jon Sterling @ 2017-04-06 0:23 UTC (permalink / raw) To: HomotopyTypeTheory Martin, This looks like a very interesting paper, thank you for sharing. I look forward to reading it in more detail. I am curious, does this development use univalence except to establish functional extensionality and propositional extensionality? The reason I ask is, I wonder if it is possible to do a similar development of computability theory in extensional type theory and get analogous results. Additionally, I am curious whether you have found cases in which univalence clarifies or sharpens this development, since I'm trying to keep track of interesting use-cases of univalence. Best, Jon On Wed, Apr 5, 2017, at 12:37 PM, 'Martin Escardo' via Homotopy Type Theory wrote: > > > On 31/03/17 17:09, 'Martin Escardo' via Homotopy Type Theory wrote: > > > > > > On 30/03/17 23:49, Nicolai Kraus wrote: > >> Interesting construction by Cory and you! And I think I can help > >> you with the factorisation that you asked for, as follows: > > > > Thanks for this, Nicolai. > > > > Cory and I a battling against the clock to get our submission ready for > > a conference. I'll continue the discussion after that. > > I may as well give a link to the paper now that we have finished and > submitted it, which is about partial functions in univalent type theory: > http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf > > The conjecture in the initial message of this thread goes well beyond > this, and is even unrelated. But I am still very interested in the > conjecture independently of any use of it. > > Martin > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-04-06 0:23 ` Jon Sterling @ 2017-04-06 5:55 ` Martin Escardo 2017-04-06 12:40 ` Vladimir Voevodsky 2017-04-06 11:52 ` Thomas Streicher 1 sibling, 1 reply; 22+ messages in thread From: Martin Escardo @ 2017-04-06 5:55 UTC (permalink / raw) To: Jon Sterling, HomotopyT... On 06/04/17 01:23, Jon Sterling wrote: > I am curious, does this development use univalence except to establish > functional extensionality and propositional extensionality? The reason I > ask is, I wonder if it is possible to do a similar development of > computability theory in extensional type theory and get analogous > results. Additionally, I am curious whether you have found cases in > which univalence clarifies or sharpens this development, since I'm > trying to keep track of interesting use-cases of univalence. Currently the only place that uses univalence is the equivalence of (X->Y) with the type of single-valued relations X->Y->U. (This was proved by Egbert in his mater thesis.) But another point, compared with previous developments in topos logic an extensional type theory, is that a number of things work as they should for types more general than sets by replacing subobject-classifier-valued functions by universe-valued functions. An example is this: Consider the lifing in its representation with subsingletons L(X) = (Sigma(A:X->U), isProp(Sigma(x:X), A(x))). If we replaced U by Prop in this definition, this wouldn't work well for types that are not sets. For example, if X is the circle, any function into a set, and hence any function into Prop, is constant, and so L(X) would be contractible. However, with the definition as it is, with U, we always have that X is embedded into L(X), even if X is not a set. The same phenomenon applies to the equivalence of (X->Y) with the type of single-valued relations X->Y->U discussed above, but this additionally requires univalence. Martin ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-04-06 5:55 ` Martin Escardo @ 2017-04-06 12:40 ` Vladimir Voevodsky 2017-04-06 13:50 ` Martin Escardo 0 siblings, 1 reply; 22+ messages in thread From: Vladimir Voevodsky @ 2017-04-06 12:40 UTC (permalink / raw) To: Martin Escardo; +Cc: Prof. Vladimir Voevodsky, Jon Sterling, HomotopyT... [-- Attachment #1: Type: text/plain, Size: 2283 bytes --] I looks like like you would also need the resizing rule to place hProp into a lower universe. Is it so? Vladimir. > On Apr 6, 2017, at 1:55 AM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> wrote: > > > > On 06/04/17 01:23, Jon Sterling wrote: >> I am curious, does this development use univalence except to establish >> functional extensionality and propositional extensionality? The reason I >> ask is, I wonder if it is possible to do a similar development of >> computability theory in extensional type theory and get analogous >> results. Additionally, I am curious whether you have found cases in >> which univalence clarifies or sharpens this development, since I'm >> trying to keep track of interesting use-cases of univalence. > > Currently the only place that uses univalence is the equivalence of > (X->Y) with the type of single-valued relations X->Y->U. (This was > proved by Egbert in his mater thesis.) > > But another point, compared with previous developments in topos logic > an extensional type theory, is that a number of things work as they > should for types more general than sets by replacing > subobject-classifier-valued functions by universe-valued functions. > > An example is this: Consider the lifing in its representation with > subsingletons > > L(X) = (Sigma(A:X->U), isProp(Sigma(x:X), A(x))). > > If we replaced U by Prop in this definition, this wouldn't work well > for types that are not sets. > > For example, if X is the circle, any function into a set, and hence > any function into Prop, is constant, and so L(X) would be > contractible. > > However, with the definition as it is, with U, we always have that X > is embedded into L(X), even if X is not a set. > > The same phenomenon applies to the equivalence of (X->Y) with the type > of single-valued relations X->Y->U discussed above, but this > additionally requires univalence. > > Martin > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Message signed with OpenPGP --] [-- Type: application/pgp-signature, Size: 507 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-04-06 12:40 ` Vladimir Voevodsky @ 2017-04-06 13:50 ` Martin Escardo [not found] ` <81c0782f-9287-4111-a4f1-01cb9c87c7e8@cs.bham.ac.uk> 0 siblings, 1 reply; 22+ messages in thread From: Martin Escardo @ 2017-04-06 13:50 UTC (permalink / raw) To: Vladimir Voevodsky, Martin Escardo; +Cc: Jon Sterling, HomotopyT... On 06/04/17 13:40, Vladimir Voevodsky wrote: > I looks like like you would also need the resizing rule to place > hProp into a lower universe. Is it so? I think that this is most natural way. But, to convince myself that often resizing is not needed, I wrote in Agda examples of similar "monads" T (e.g. the propositional truncation defined by ||X|| : (P : U) -> isProp P -> (X -> P) -> P) with universe juggling, by decorating the occurrences of U with indices. Although TX will live in the next universe, and hence so will the unit and the multiplication, and the monad laws (can be written down and) hold. Here I show the types only, where "i" is the level of the propositions you are considering: T : {i j : Level} → U j → U (j ⊔ lsuc i) η : {i j : Level} {X : U j} → X → T {i} {j} X T-extend : {i j k : Level} {X : U j} {Y : U k} → (X → T {i} {k} Y) → (T {i} {j} X → T {i} {k} Y) kleisli-law₀ : {i j : Level} {X : U j} → T-extend η ≡ id kleisli-law₁ : {i j k : Level} {X : U j} {Y : U k} (f : X → T {i} {k} Y) → T-extend f ∘ η ≡ f kleisli-law₂ : {i j k l : Level} {X : U j} {Y : U k} {Z : U l} (f : X → T {i} {k} Y) (g : Y → T {i} {l} Z) → T-extend(T-extend g ∘ f) ≡ (T-extend g) ∘ (T-extend f) μ : {i j : Level} {X : U j} → T {i} {j ⊔ lsuc i} (T {i} {j} X) → T {i} {j} X T-functor : {i j k : Level} {X : U j} {Y : U k} → (X → Y) → (T {i} {j} X → T {i} {k} Y) This works for the above example, and for lifting too. (Of course all this universe subscripting is ugly.) But I would prefer that somebody proved that propositional resizing (is consistent and) doesn't destroy normalization (e.g. in cubical type theory), and just use resizing. Or just keep my fingers crossed and work with propositional resizing. :-) Martin > > Vladimir. > >> On Apr 6, 2017, at 1:55 AM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> wrote: >> >> >> >> On 06/04/17 01:23, Jon Sterling wrote: >>> I am curious, does this development use univalence except to establish >>> functional extensionality and propositional extensionality? The reason I >>> ask is, I wonder if it is possible to do a similar development of >>> computability theory in extensional type theory and get analogous >>> results. Additionally, I am curious whether you have found cases in >>> which univalence clarifies or sharpens this development, since I'm >>> trying to keep track of interesting use-cases of univalence. >> >> Currently the only place that uses univalence is the equivalence of >> (X->Y) with the type of single-valued relations X->Y->U. (This was >> proved by Egbert in his mater thesis.) >> >> But another point, compared with previous developments in topos logic >> an extensional type theory, is that a number of things work as they >> should for types more general than sets by replacing >> subobject-classifier-valued functions by universe-valued functions. >> >> An example is this: Consider the lifing in its representation with >> subsingletons >> >> L(X) = (Sigma(A:X->U), isProp(Sigma(x:X), A(x))). >> >> If we replaced U by Prop in this definition, this wouldn't work well >> for types that are not sets. >> >> For example, if X is the circle, any function into a set, and hence >> any function into Prop, is constant, and so L(X) would be >> contractible. >> >> However, with the definition as it is, with U, we always have that X >> is embedded into L(X), even if X is not a set. >> >> The same phenomenon applies to the equivalence of (X->Y) with the type >> of single-valued relations X->Y->U discussed above, but this >> additionally requires univalence. >> >> Martin >> >> -- >> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > ^ permalink raw reply [flat|nested] 22+ messages in thread
[parent not found: <81c0782f-9287-4111-a4f1-01cb9c87c7e8@cs.bham.ac.uk>]
* Re: [HoTT] Conjecture [not found] ` <81c0782f-9287-4111-a4f1-01cb9c87c7e8@cs.bham.ac.uk> @ 2017-04-06 16:09 ` Martin Escardo 0 siblings, 0 replies; 22+ messages in thread From: Martin Escardo @ 2017-04-06 16:09 UTC (permalink / raw) To: Martin Escardo; +Cc: HomotopyT... Another remark about size is that if the propositions in your dominance are in the first universe, then all universes except the first one are closed under lifting, and hence we way as well just work from the second universe onwards as an alternative to resizing. Martin On 06/04/17 17:08, Martin Escardo wrote: > Another remark about size is that if the propositions in your dominance > are in the first universe, then all universes except the first one are > closed under lifting, and hence we way as well just work from the second > universe onwards as an alternative to resizing. Martin > > On 06/04/17 14:50, 'Martin Escardo' via Homotopy Type Theory wrote: >> >> >> On 06/04/17 13:40, Vladimir Voevodsky wrote: >>> I looks like like you would also need the resizing rule to place >>> hProp into a lower universe. Is it so? >> >> I think that this is most natural way. >> >> But, to convince myself that often resizing is not needed, I wrote in >> Agda examples of similar "monads" T (e.g. the propositional truncation >> defined by ||X|| : (P : U) -> isProp P -> (X -> P) -> P) with universe >> juggling, by decorating the occurrences of U with indices. Although TX >> will live in the next universe, and hence so will the unit and the >> multiplication, and the monad laws (can be written down and) hold. >> >> Here I show the types only, where "i" is the level of the propositions >> you are considering: >> >> T : {i j : Level} → U j → U (j ⊔ lsuc i) >> >> η : {i j : Level} {X : U j} → X → T {i} {j} X >> >> T-extend : {i j k : Level} {X : U j} {Y : U k} >> → (X → T {i} {k} Y) → (T {i} {j} X → T {i} {k} Y) >> >> kleisli-law₀ : {i j : Level} {X : U j} >> → T-extend η ≡ id >> >> kleisli-law₁ : {i j k : Level} {X : U j} {Y : U k} >> (f : X → T {i} {k} Y) >> → T-extend f ∘ η ≡ f >> >> kleisli-law₂ : {i j k l : Level} {X : U j} {Y : U k} {Z : U l} >> (f : X → T {i} {k} Y) >> (g : Y → T {i} {l} Z) >> → T-extend(T-extend g ∘ f) ≡ (T-extend g) ∘ (T-extend f) >> >> μ : {i j : Level} {X : U j} >> → T {i} {j ⊔ lsuc i} (T {i} {j} X) → T {i} {j} X >> >> T-functor : {i j k : Level} {X : U j} {Y : U k} >> → (X → Y) → (T {i} {j} X → T {i} {k} Y) >> >> This works for the above example, and for lifting too. >> >> (Of course all this universe subscripting is ugly.) >> >> But I would prefer that somebody proved that propositional resizing >> (is consistent and) doesn't destroy normalization (e.g. in cubical >> type theory), and just use resizing. Or just keep my fingers crossed >> and work with propositional resizing. :-) >> >> Martin >> >>> >>> Vladimir. >>> >>>> On Apr 6, 2017, at 1:55 AM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> wrote: >>>> >>>> >>>> >>>> On 06/04/17 01:23, Jon Sterling wrote: >>>>> I am curious, does this development use univalence except to establish >>>>> functional extensionality and propositional extensionality? The reason I >>>>> ask is, I wonder if it is possible to do a similar development of >>>>> computability theory in extensional type theory and get analogous >>>>> results. Additionally, I am curious whether you have found cases in >>>>> which univalence clarifies or sharpens this development, since I'm >>>>> trying to keep track of interesting use-cases of univalence. >>>> >>>> Currently the only place that uses univalence is the equivalence of >>>> (X->Y) with the type of single-valued relations X->Y->U. (This was >>>> proved by Egbert in his mater thesis.) >>>> >>>> But another point, compared with previous developments in topos logic >>>> an extensional type theory, is that a number of things work as they >>>> should for types more general than sets by replacing >>>> subobject-classifier-valued functions by universe-valued functions. >>>> >>>> An example is this: Consider the lifing in its representation with >>>> subsingletons >>>> >>>> L(X) = (Sigma(A:X->U), isProp(Sigma(x:X), A(x))). >>>> >>>> If we replaced U by Prop in this definition, this wouldn't work well >>>> for types that are not sets. >>>> >>>> For example, if X is the circle, any function into a set, and hence >>>> any function into Prop, is constant, and so L(X) would be >>>> contractible. >>>> >>>> However, with the definition as it is, with U, we always have that X >>>> is embedded into L(X), even if X is not a set. >>>> >>>> The same phenomenon applies to the equivalence of (X->Y) with the type >>>> of single-valued relations X->Y->U discussed above, but this >>>> additionally requires univalence. >>>> >>>> Martin >>>> >>>> -- >>>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. >>>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com. >>>> For more options, visit https://groups.google.com/d/optout. >>> >> > ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-04-06 0:23 ` Jon Sterling 2017-04-06 5:55 ` Martin Escardo @ 2017-04-06 11:52 ` Thomas Streicher 2017-04-07 9:49 ` Martin Escardo 1 sibling, 1 reply; 22+ messages in thread From: Thomas Streicher @ 2017-04-06 11:52 UTC (permalink / raw) To: Jon Sterling; +Cc: HomotopyT... > This looks like a very interesting paper, thank you for sharing. I look > forward to reading it in more detail. > > I am curious, does this development use univalence except to establish > functional extensionality and propositional extensionality? The reason I > ask is, I wonder if it is possible to do a similar development of > computability theory in extensional type theory and get analogous > results. Additionally, I am curious whether you have found cases in > which univalence clarifies or sharpens this development, since I'm > trying to keep track of interesting use-cases of univalence. For synthetic domain theory a formulation in extensional type theory has been given in MR1694130 (2000f:68069) Reus, Bernhard; Streicher, Thomas General synthetic domain theory ¡X a logical approach. (English summary) Math. Structures Comput. Sci. 9 (1999), no. 2, 177¡V223. There is no need whatsoever to use univalence or something like that. The only benefit would be to solve domain equations up to equality which even computer scientists find unnecessary (for good reasons). Andrej Bauer has written on Synthetic Recursion Theory, see math.andrej.com/data/synthetic.pdf. So I tend to the opinion that theer can't be an intrinsic use of Univalence or HITs. But if there is I am curious to learn which one! Thomas ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-04-06 11:52 ` Thomas Streicher @ 2017-04-07 9:49 ` Martin Escardo 2017-04-07 17:11 ` Michael Shulman 0 siblings, 1 reply; 22+ messages in thread From: Martin Escardo @ 2017-04-07 9:49 UTC (permalink / raw) To: Thomas Streicher, Jon Sterling; +Cc: HomotopyT... Dear Thomas, Sorry it took so long to answer, but I needed to find time to be able to write my reaction to your remarks. (1) Indeed, I do like to think of the fragment of univalent type theory consisting of function extensionality + proposition extensionality + propositional truncation as essentially the same thing as topos logic, provided we have propositional resizing. (But, as discussed, much can be done without propositional resizing (but not all), and one way of looking at HIT's is as a mechanism to avoid resizing.) This is good: this fragment leaves us in familiar territory. (2) I don't see univalent type theory as simply the extension of type theory with univalence (and hence function and proposition extensionality). Before we extend dependent type theory with any axiom, we can start to think "univalently". In particular, the notions of h-level, proposition, contractibility, equivalence, the distinction of existence as proposition or structure, so as to be able to define e.g. embeddings, surjections, and many others correctly, can be formulated and understood before we bring univalence. In this way "univalent type theory" is a different way to understand good old type theory. Of course, with univalence we get more, and what you are saying, and I don't disagree fundamentally, is that this "more" are types of higher h-level and theorems and constructions with them (such as the type of categories, if we want to avoid homotopy in the discussion). Although we don't use univalence in our paper, we formulate our notions in the light of this new, alternative understanding of type theory. One example, already mentioned in the above answer to Jon, is something that kept Cory and I working for an afternoon, but perhaps is not adequately emphasized in the paper. In topos logic, you define (for the dominance of all propositions) Lift(X) = { A:X->Omega | (exists(x:X), A x) & forall(x,y:X), A x -> A y -> x = y } If we want, in univalent type theory, this to work for types of higher h-levels, how should we define this? The above definition works well and can be kept as it is if X is a set. To generalize it to types of higher levels, we need two modifications: (i) Change Omega to the universe U. (ii) Reformulate the condition on A as isProp(Sigma(x:X), A x). When X is a set, the reformulation (i)-(ii) makes no difference. However, in the general case, it is (i) and (ii) that give the right definition. For instance, with the right definition, we always get an embedding X->Lift X, whereas if we had taken the original topos-theoretic version of Lift, then Lift S^1 would be a singleton and hence wouldn't embed S^1. We would get the wrong notion of partial function. Thus, although we haven't used univalence, we took care of formulating the notions so that they are not restricted to the realm of sets, and in this sense what we are doing can be considered as univalent type theory. (3) We should have cited Andrej's and Bernhard's references below, and we will (and many other things, to reflect the amount of work done about this in the context of topos theory). Of course we are aware of them, but thanks for mentioning them in this list! (4) A last point is that, as opposed to most of the work in the topos literature for dominances in realizability toposes as in (3), we deliberately don't use Markov's principle or countable choice in our internal development of computability in univalent type theory (Section 3 of the paper). Moreover, we are *not* looking at synthetic computability. We are looking at plain computability. Best, Martin On 06/04/17 12:52, Thomas Streicher wrote: >> This looks like a very interesting paper, thank you for sharing. I look >> forward to reading it in more detail. >> >> I am curious, does this development use univalence except to establish >> functional extensionality and propositional extensionality? The reason I >> ask is, I wonder if it is possible to do a similar development of >> computability theory in extensional type theory and get analogous >> results. Additionally, I am curious whether you have found cases in >> which univalence clarifies or sharpens this development, since I'm >> trying to keep track of interesting use-cases of univalence. > > For synthetic domain theory a formulation in extensional type theory > has been given in > > MR1694130 (2000f:68069) > Reus, Bernhard; Streicher, Thomas > General synthetic domain theory — a logical approach. (English summary) > Math. Structures Comput. Sci. 9 (1999), no. 2, 177–223. > > There is no need whatsoever to use univalence or something like that. > The only benefit would be to solve domain equations up to equality > which even computer scientists find unnecessary (for good reasons). > > Andrej Bauer has written on Synthetic Recursion Theory, see > math.andrej.com/data/synthetic.pdf. > > So I tend to the opinion that theer can't be an intrinsic use of > Univalence or HITs. But if there is I am curious to learn which one! > > Thomas > -- Martin Escardo http://www.cs.bham.ac.uk/~mhe ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-04-07 9:49 ` Martin Escardo @ 2017-04-07 17:11 ` Michael Shulman 2017-04-07 18:10 ` Martin Escardo 0 siblings, 1 reply; 22+ messages in thread From: Michael Shulman @ 2017-04-07 17:11 UTC (permalink / raw) To: Martin Escardo; +Cc: HomotopyT...@googlegroups.com On Fri, Apr 7, 2017 at 2:49 AM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> wrote: > (1) Indeed, I do like to think of the fragment of univalent type > theory consisting of function extensionality + proposition > extensionality + propositional truncation as essentially the same > thing as topos logic, provided we have propositional resizing. (But, > as discussed, much can be done without propositional resizing (but not > all), and one way of looking at HIT's is as a mechanism to avoid > resizing.) I would say that to really be talking about (elementary) topos logic, one should also do without universes other than hProp. Of course, elementary 1-toposes also validate UIP. If we also omit hProp and propositional resizing, but include nonrecursive HITs as well as ordinary inductive types, then it ought to be basically Pi-W-pretopos logic; right? > This is good: this fragment leaves us in familiar territory. > > (2) I don't see univalent type theory as simply the extension of type > theory with univalence (and hence function and proposition > extensionality). Before we extend dependent type theory with any > axiom, we can start to think "univalently". > > In particular, the notions of h-level, proposition, contractibility, > equivalence, the distinction of existence as proposition or structure, > so as to be able to define e.g. embeddings, surjections, and many > others correctly, can be formulated and understood before we bring > univalence. > > In this way "univalent type theory" is a different way to understand > good old type theory. Of course, with univalence we get more, and what > you are saying, and I don't disagree fundamentally, is that this > "more" are types of higher h-level and theorems and constructions with > them (such as the type of categories, if we want to avoid homotopy in > the discussion). > > Although we don't use univalence in our paper, we formulate our > notions in the light of this new, alternative understanding of type > theory. > > One example, already mentioned in the above answer to Jon, is > something that kept Cory and I working for an afternoon, but perhaps > is not adequately emphasized in the paper. > > In topos logic, you define (for the dominance of all propositions) > > Lift(X) = { A:X->Omega | (exists(x:X), A x) & > forall(x,y:X), A x -> A y -> x = y } > > If we want, in univalent type theory, this to work for types of higher > h-levels, how should we define this? > > The above definition works well and can be kept as it is if X is a > set. To generalize it to types of higher levels, we need two > modifications: > > (i) Change Omega to the universe U. > (ii) Reformulate the condition on A as isProp(Sigma(x:X), A x). > > When X is a set, the reformulation (i)-(ii) makes no > difference. However, in the general case, it is (i) and (ii) that give > the right definition. For instance, with the right definition, we > always get an embedding X->Lift X, whereas if we had taken the > original topos-theoretic version of Lift, then Lift S^1 would be a > singleton and hence wouldn't embed S^1. We would get the wrong notion > of partial function. > > Thus, although we haven't used univalence, we took care of formulating > the notions so that they are not restricted to the realm of sets, and > in this sense what we are doing can be considered as univalent type > theory. > > (3) We should have cited Andrej's and Bernhard's references below, and > we will (and many other things, to reflect the amount of work done > about this in the context of topos theory). Of course we are aware of > them, but thanks for mentioning them in this list! > > (4) A last point is that, as opposed to most of the work in the topos > literature for dominances in realizability toposes as in (3), we > deliberately don't use Markov's principle or countable choice in our > internal development of computability in univalent type theory > (Section 3 of the paper). Moreover, we are *not* looking at synthetic > computability. We are looking at plain computability. > > Best, > Martin > > > On 06/04/17 12:52, Thomas Streicher wrote: >>> This looks like a very interesting paper, thank you for sharing. I look >>> forward to reading it in more detail. >>> >>> I am curious, does this development use univalence except to establish >>> functional extensionality and propositional extensionality? The reason I >>> ask is, I wonder if it is possible to do a similar development of >>> computability theory in extensional type theory and get analogous >>> results. Additionally, I am curious whether you have found cases in >>> which univalence clarifies or sharpens this development, since I'm >>> trying to keep track of interesting use-cases of univalence. >> >> For synthetic domain theory a formulation in extensional type theory >> has been given in >> >> MR1694130 (2000f:68069) >> Reus, Bernhard; Streicher, Thomas >> General synthetic domain theory — a logical approach. (English summary) >> Math. Structures Comput. Sci. 9 (1999), no. 2, 177–223. >> >> There is no need whatsoever to use univalence or something like that. >> The only benefit would be to solve domain equations up to equality >> which even computer scientists find unnecessary (for good reasons). >> >> Andrej Bauer has written on Synthetic Recursion Theory, see >> math.andrej.com/data/synthetic.pdf. >> >> So I tend to the opinion that theer can't be an intrinsic use of >> Univalence or HITs. But if there is I am curious to learn which one! >> >> Thomas >> > > -- > Martin Escardo > http://www.cs.bham.ac.uk/~mhe > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Conjecture 2017-04-07 17:11 ` Michael Shulman @ 2017-04-07 18:10 ` Martin Escardo 0 siblings, 0 replies; 22+ messages in thread From: Martin Escardo @ 2017-04-07 18:10 UTC (permalink / raw) To: Michael Shulman; +Cc: HomotopyT...@googlegroups.com On 07/04/17 18:11, Michael Shulman wrote: > On Fri, Apr 7, 2017 at 2:49 AM, 'Martin Escardo' via Homotopy Type > Theory <HomotopyT...@googlegroups.com> wrote: >> (1) Indeed, I do like to think of the fragment of univalent type >> theory consisting of function extensionality + proposition >> extensionality + propositional truncation as essentially the same >> thing as topos logic, provided we have propositional resizing. (But, >> as discussed, much can be done without propositional resizing (but not >> all), and one way of looking at HIT's is as a mechanism to avoid >> resizing.) > > I would say that to really be talking about (elementary) topos logic, > one should also do without universes other than hProp. Of course, > elementary 1-toposes also validate UIP. Agreed. (But you can consider elementary toposes with a universe object, and a number of people have worked on that independently of any connection with dependent type theory.) > If we also omit hProp and propositional resizing, but include > nonrecursive HITs as well as ordinary inductive types, then it ought > to be basically Pi-W-pretopos logic; right? I'd let the experts on these details to answer this. I noticed the following mistake immediately after I send my message this morning, and this is a good opportunity to rectify it: >> In topos logic, you define (for the dominance of all propositions) >> >> Lift(X) = { A:X->Omega | (exists(x:X), A x) & >> forall(x,y:X), A x -> A y -> x = y } >> Lift(X) = { A:X->Omega | forall(x,y:X), A x -> A y -> x = y } If anybody noticed, they probably knew I meant that, and, if they didn't notice, they probably understood that. There are other possibilities, of course. :-) Martin ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Conjecture 2017-03-27 21:57 Conjecture Martin Escardo 2017-03-29 21:08 ` [HoTT] Conjecture Nicolai Kraus @ 2017-04-03 0:35 ` Daniel R. Grayson 2017-04-03 2:20 ` [HoTT] Conjecture Favonia 2017-04-03 9:56 ` Nicolai Kraus 1 sibling, 2 replies; 22+ messages in thread From: Daniel R. Grayson @ 2017-04-03 0:35 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 647 bytes --] Here's a fact related to the current discussion, which I have formalized today. I would appreciate knowing whether it's already known. It gives a criterion for factoring through the propositional truncation when the target is of h-level 3. Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3} (f : X -> Y) (c : ∏ x x', f x = f x') : (∏ x, c x x = idpath (f x)) -> (∏ x x' x'', c x x'' = c x x' @ c x' x'') -> ∥ X ∥ -> Y. You may find it in WellOrderedSets.v <https://github.com/DanGrayson/UniMath/blob/well-ordering-2/UniMath/Combinatorics/WellOrderedSets.v> on one of my branches. [-- Attachment #1.2: Type: text/html, Size: 1221 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Re: Conjecture 2017-04-03 0:35 ` Conjecture Daniel R. Grayson @ 2017-04-03 2:20 ` Favonia 2017-04-03 9:56 ` Nicolai Kraus 1 sibling, 0 replies; 22+ messages in thread From: Favonia @ 2017-04-03 2:20 UTC (permalink / raw) To: Daniel R. Grayson, Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 1380 bytes --] Yes, this has been known from Nicolai's work on truncation (e.g. "The General Universal Property"). I just learned that this has been mechanized in Agda by Nils as well. http://www.cse.chalmers.se/~nad/listings/equality/H-level.Truncation.html#18216 By the way, the condition (∏ x, c x x = idpath (f x)) is provable from transitivity. -Favonia On Sun, Apr 2, 2017 at 8:35 PM Daniel R. Grayson < danielrich...@gmail.com> wrote: Here's a fact related to the current discussion, which I have formalized today. I would appreciate knowing whether it's already known. It gives a criterion for factoring through the propositional truncation when the target is of h-level 3. Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3} (f : X -> Y) (c : ∏ x x', f x = f x') : (∏ x, c x x = idpath (f x)) -> (∏ x x' x'', c x x'' = c x x' @ c x' x'') -> ∥ X ∥ -> Y. You may find it in WellOrderedSets.v <https://github.com/DanGrayson/UniMath/blob/well-ordering-2/UniMath/Combinatorics/WellOrderedSets.v> on one of my branches. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 3285 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Re: Conjecture 2017-04-03 0:35 ` Conjecture Daniel R. Grayson 2017-04-03 2:20 ` [HoTT] Conjecture Favonia @ 2017-04-03 9:56 ` Nicolai Kraus 2017-04-03 11:50 ` Daniel R. Grayson 1 sibling, 1 reply; 22+ messages in thread From: Nicolai Kraus @ 2017-04-03 9:56 UTC (permalink / raw) To: Daniel R. Grayson, Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 1918 bytes --] Dan, this is one instance of my "general universal property of the propositional truncation", arXiv:1411.2682. In that paper I show that, if you fix a number n, then for a type Y of h-level n, the function type ||X|| -> Y is equivalent to the Sigma-type with the following components: (1) a function X -> Y (2) the condition that (1) is weakly constant (3) a coherence condition for (2) (4) a coherence condition for (3) ... (n) a coherence condition for (n-1) This can be presented as a natural transformation between semi-simplicial types. What you have formalized is the case n=3 (one direction). (In my presentation, I don't use the component "c x x = idpath (f x)" because it can be inferred, and if you go higher than 3, this component would make additional coherence conditions necessary.) Nicolai On 03/04/17 01:35, Daniel R. Grayson wrote: > Here's a fact related to the current discussion, which I have > formalized today. I would appreciate knowing > whether it's already known. It gives a criterion for factoring > through the propositional truncation > when the target is of h-level 3. > > Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3} > (f : X -> Y) (c : ∏ x x', f x = f x') : > (∏ x, c x x = idpath (f x)) -> > (∏ x x' x'', c x x'' = c x x' @ c x' x'') -> > ∥ X ∥ -> Y. > > You may find it in WellOrderedSets.v > <https://github.com/DanGrayson/UniMath/blob/well-ordering-2/UniMath/Combinatorics/WellOrderedSets.v> on > one of my branches. > > > -- > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send > an email to HomotopyTypeThe...@googlegroups.com > <mailto:HomotopyTypeThe...@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 3410 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Re: Conjecture 2017-04-03 9:56 ` Nicolai Kraus @ 2017-04-03 11:50 ` Daniel R. Grayson 0 siblings, 0 replies; 22+ messages in thread From: Daniel R. Grayson @ 2017-04-03 11:50 UTC (permalink / raw) To: Homotopy Type Theory; +Cc: danielrich... [-- Attachment #1.1: Type: text/plain, Size: 1739 bytes --] Thanks, Nicolai and Favonia. It's a nice result, Nicolai! On Monday, April 3, 2017 at 5:56:36 AM UTC-4, Nicolai Kraus wrote: > > Dan, this is one instance of my "general universal property of the > propositional truncation", arXiv:1411.2682. > In that paper I show that, if you fix a number n, then for a type Y of > h-level n, the function type > ||X|| -> Y > is equivalent to the Sigma-type with the following components: > (1) a function X -> Y > (2) the condition that (1) is weakly constant > (3) a coherence condition for (2) > (4) a coherence condition for (3) > ... > (n) a coherence condition for (n-1) > > This can be presented as a natural transformation between semi-simplicial > types. > What you have formalized is the case n=3 (one direction). > (In my presentation, I don't use the component "c x x = idpath (f x)" > because it can be inferred, > and if you go higher than 3, this component would make additional > coherence conditions necessary.) > Nicolai > > On 03/04/17 01:35, Daniel R. Grayson wrote: > > Here's a fact related to the current discussion, which I have formalized > today. I would appreciate knowing > whether it's already known. It gives a criterion for factoring through > the propositional truncation > when the target is of h-level 3. > > Definition squash_to_HLevel_3 {X : UU} {Y : HLevel 3} > (f : X -> Y) (c : ∏ x x', f x = f x') : > (∏ x, c x x = idpath (f x)) -> > (∏ x x' x'', c x x'' = c x x' @ c x' x'') -> > ∥ X ∥ -> Y. > > You may find it in WellOrderedSets.v > <https://github.com/DanGrayson/UniMath/blob/well-ordering-2/UniMath/Combinatorics/WellOrderedSets.v> on > one of my branches. > > [-- Attachment #1.2: Type: text/html, Size: 3459 bytes --] ^ permalink raw reply [flat|nested] 22+ messages in thread
end of thread, other threads:[~2017-04-07 18:10 UTC | newest] Thread overview: 22+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-03-27 21:57 Conjecture Martin Escardo 2017-03-29 21:08 ` [HoTT] Conjecture Nicolai Kraus 2017-03-29 22:05 ` Martin Escardo 2017-03-30 10:59 ` Michael Shulman 2017-03-30 19:22 ` Egbert Rijke 2017-03-30 23:02 ` Nicolai Kraus 2017-03-30 22:49 ` Nicolai Kraus 2017-03-31 16:09 ` Martin Escardo 2017-04-05 19:37 ` Martin Escardo 2017-04-06 0:23 ` Jon Sterling 2017-04-06 5:55 ` Martin Escardo 2017-04-06 12:40 ` Vladimir Voevodsky 2017-04-06 13:50 ` Martin Escardo [not found] ` <81c0782f-9287-4111-a4f1-01cb9c87c7e8@cs.bham.ac.uk> 2017-04-06 16:09 ` Martin Escardo 2017-04-06 11:52 ` Thomas Streicher 2017-04-07 9:49 ` Martin Escardo 2017-04-07 17:11 ` Michael Shulman 2017-04-07 18:10 ` Martin Escardo 2017-04-03 0:35 ` Conjecture Daniel R. Grayson 2017-04-03 2:20 ` [HoTT] Conjecture Favonia 2017-04-03 9:56 ` Nicolai Kraus 2017-04-03 11:50 ` Daniel R. Grayson
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).