* Does MLTT have "or"? @ 2017-05-02 9:09 Martin Escardo 2017-05-02 19:04 ` [HoTT] " Michael Shulman ` (3 more replies) 0 siblings, 4 replies; 17+ messages in thread From: Martin Escardo @ 2017-05-02 9:09 UTC (permalink / raw) To: HomotopyT...@googlegroups.com Last week in a meeting I had a technical discussion with somebody, who suggested to post the question here. (1) Prove (internally) or disprove (as a meta-theorem, probably with a counter-model) the following in (intensional) Martin-Loef Type Theory: * The poset of subsingletons (or propositions or truth values) has binary joins (or disjunction). (We know it has binary meets and Heyting implication, which amounts to saying it is a Heyting semilattice. Is it a lattice?) (2) The question is whether given any two propositions P and Q we can find a proposition R with P->R and Q->R such that for any proposition R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of P and Q.) (3) Of course, if MLTT had propositional truncations ||-||, then the answer would be R := ||P+Q||. But we can ask this question for MLTT before we postulate propositional truncations as in (1)-(2). (4) What is a model of intensional MLTT with a universe such that ||-|| doesn't exist? More precisely, define, internally in intensional MLTT, hasTruncation(X:U) := Σ(X':U), isProp(X') × (X→X') × Π(P:U), (isProp(P) × (X→P)) → (X'→P). Is there a model, with universes, the falsifies this? Preferably, we want models that falsify this but validate function extensionality (and perhaps also propositional extensionality). Best, Martin ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-02 9:09 Does MLTT have "or"? Martin Escardo @ 2017-05-02 19:04 ` Michael Shulman 2017-05-03 6:47 ` Martin Escardo 2017-05-12 18:10 ` Martin Escardo 2017-05-03 10:55 ` Thomas Streicher ` (2 subsequent siblings) 3 siblings, 2 replies; 17+ messages in thread From: Michael Shulman @ 2017-05-02 19:04 UTC (permalink / raw) To: Martin Escardo; +Cc: HomotopyT...@googlegroups.com Some thoughts: - If in addition to function extensionality and propositional extensionality we assume propositional resizing, then ||-|| is constructible using the standard argument that an elementary topos is a regular category. - A model of MLTT with function extensionality but no universes is given by any locally cartesian closed category (perhaps with coproducts if we have binary sum types). It seems that surely not every lccc with coproducts is a regular category -- though I don't have an example ready to hand, let alone an example that also has universes. On Tue, May 2, 2017 at 2:09 AM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> wrote: > Last week in a meeting I had a technical discussion with somebody, who > suggested to post the question here. > > (1) Prove (internally) or disprove (as a meta-theorem, probably with a > counter-model) the following in (intensional) Martin-Loef Type Theory: > > * The poset of subsingletons (or propositions or truth values) has > binary joins (or disjunction). > > (We know it has binary meets and Heyting implication, which amounts to > saying it is a Heyting semilattice. Is it a lattice?) > > (2) The question is whether given any two propositions P and Q we can > find a proposition R with P->R and Q->R such that for any proposition > R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of > P and Q.) > > (3) Of course, if MLTT had propositional truncations ||-||, then the > answer would be R := ||P+Q||. But we can ask this question for MLTT > before we postulate propositional truncations as in (1)-(2). > > (4) What is a model of intensional MLTT with a universe such that > ||-|| doesn't exist? > > More precisely, define, internally in intensional MLTT, > > hasTruncation(X:U) := Σ(X':U), > isProp(X') > × (X→X') > × Π(P:U), (isProp(P) × (X→P)) → (X'→P). > > Is there a model, with universes, the falsifies this? > > Preferably, we want models that falsify this but validate > function extensionality (and perhaps also propositional > extensionality). > > Best, > 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] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-02 19:04 ` [HoTT] " Michael Shulman @ 2017-05-03 6:47 ` Martin Escardo 2017-05-12 18:10 ` Martin Escardo 1 sibling, 0 replies; 17+ messages in thread From: Martin Escardo @ 2017-05-03 6:47 UTC (permalink / raw) To: Michael Shulman, Martin Escardo; +Cc: HomotopyT...@googlegroups.com On 02/05/17 20:04, Michael Shulman wrote: > Some thoughts: Thanks. Some more remarks: > - If in addition to function extensionality and propositional > extensionality we assume propositional resizing, then ||-|| is > constructible using the standard argument that an elementary topos is > a regular category. We can say more regarding resizing, in the presence of universes, as in my question. If U' is the universe after U with U:U', then the large type hasTruncation'(X:U) := Σ(X':U'), isProp(X') × (X→X') × Π(P:U), (isProp(P) × (X→P)) → (X'→P). is always inhabited in MLTT. It is a proposition for all X:U iff funext and propext hold. Moreover, you can construct such a "large truncation" X' by X' = Π(P:U), isProp(P) → (X → P) → P. Then X' is a proposition for all X' iff funext holds (propext is not involved here). Then, in the presence of funext, X has a small truncation ∥X∥ iff there is a small proposition P:U equivalent to X', and in this case P has the universal property of ∥X∥. Hence the presence of all small propositional truncations *is* a resizing axiom, amounting to say that every large truncation X' of each small X:U is equivalent to some small P:U. > - A model of MLTT with function extensionality but no universes is > given by any locally cartesian closed category (perhaps with > coproducts if we have binary sum types). It seems that surely not > every lccc with coproducts is a regular category -- though I don't > have an example ready to hand, let alone an example that also has > universes. Right. I want an example with universes, and, moreover, an example which will not only fail to have all small truncations but also the truncation of P+Q for small propositions P and Q. You can ask this question when P and Q are type variables or when they are closed type terms. In many cases, a small truncation ∥P+Q∥ exists in all models, by a construction in MLTT. For example, consider α,β:ℕ→2 with isProp(Σ(n:ℕ), α(n)=1), isProp(Σ(n:ℕ), β(n)=1), and take P := Σ(n:ℕ), α(n)=1, Q := Σ(n:ℕ), β(n)=1. Then we can easily construct γ:ℕ→2 from α and β so that the type Σ(n:ℕ), γ(n)=1 has the universal property of ∥P+Q∥. Can you find examples of propositions P and Q such that their disjunction ∥P+Q∥ cannot be shown to exist in intensional MLTT with universes? Of course, we may have Π(P,Q:U), isProp(P) → isProp(Q) → hasTruncation(P×Q) empty in a model without such a counter-example P and Q. Martin > > > On Tue, May 2, 2017 at 2:09 AM, 'Martin Escardo' via Homotopy Type > Theory <HomotopyT...@googlegroups.com> wrote: >> Last week in a meeting I had a technical discussion with somebody, who >> suggested to post the question here. >> >> (1) Prove (internally) or disprove (as a meta-theorem, probably with a >> counter-model) the following in (intensional) Martin-Loef Type Theory: >> >> * The poset of subsingletons (or propositions or truth values) has >> binary joins (or disjunction). >> >> (We know it has binary meets and Heyting implication, which amounts to >> saying it is a Heyting semilattice. Is it a lattice?) >> >> (2) The question is whether given any two propositions P and Q we can >> find a proposition R with P->R and Q->R such that for any proposition >> R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of >> P and Q.) >> >> (3) Of course, if MLTT had propositional truncations ||-||, then the >> answer would be R := ||P+Q||. But we can ask this question for MLTT >> before we postulate propositional truncations as in (1)-(2). >> >> (4) What is a model of intensional MLTT with a universe such that >> ||-|| doesn't exist? >> >> More precisely, define, internally in intensional MLTT, >> >> hasTruncation(X:U) := Σ(X':U), >> isProp(X') >> × (X→X') >> × Π(P:U), (isProp(P) × (X→P)) → (X'→P). >> >> Is there a model, with universes, the falsifies this? >> >> Preferably, we want models that falsify this but validate >> function extensionality (and perhaps also propositional >> extensionality). >> >> Best, >> 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. > -- Martin Escardo http://www.cs.bham.ac.uk/~mhe ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-02 19:04 ` [HoTT] " Michael Shulman 2017-05-03 6:47 ` Martin Escardo @ 2017-05-12 18:10 ` Martin Escardo 2017-05-12 18:41 ` Martin Escardo 2017-05-13 21:46 ` Michael Shulman 1 sibling, 2 replies; 17+ messages in thread From: Martin Escardo @ 2017-05-12 18:10 UTC (permalink / raw) To: Michael Shulman; +Cc: HomotopyT...@googlegroups.com On 02/05/17 20:04, Michael Shulman wrote: > Some thoughts: > > [...] > > - A model of MLTT with function extensionality but no universes is > given by any locally cartesian closed category (perhaps with > coproducts if we have binary sum types). It seems that surely not > every lccc with coproducts is a regular category -- though I don't > have an example ready to hand, let alone an example that also has > universes. If you assume excluded middle (every proposition is empty or pointed), and function extensionality, then, as you know, every type X does have a propositional truncation, namely ¬¬X:=(X->0)->0. The universal map is the evaluation map eta:X->¬¬X. If we have f:X->P for a proposition P, then we get ¬¬f:¬¬X->¬¬P by the functoriality of double-dualization. By excluded middle we have a map ¬¬P->P, which composed with ¬¬f gives a map f':¬¬X->P, which in turn establishes the universality of eta:X->¬¬X among maps of X into propositions (the uniqueness requirement relies on funext). Therefore, indeed, ¬¬X is the propositional truncation of X (or, more precisely, ¬¬X, together with eta:X->¬¬X and the extension procedure f |-> f' and its uniqueness give the propositional truncation of X). (Side-remark. Conversely, if you forget the assumption of excluded middle, but remember the assumption of function extensionality, then the assumption that eta:X->¬¬X is the universal map of X into a proposition, for every X, implies excluded middle. (Exercise.) So, in general, the propositional truncation of X, if it exists, is wildly different from ¬¬X.) The above argument relies on having a universe (first, to formulate excluded middle and funext, and, second, to formulate and prove the universality of eta). *** What is the interaction (if any) of excluded middle with regularity, in your thought above? It seems to me that adding a universe is playing a role. It is different to say externally that all morphisms have images, than to say this internally using a universe (or am I wrong?). A second side-remark is this, which I realized just now while writing this, although I have known the above for several years: We know that the addition of propositional truncations as a rule, with certain stipulated definitional equalities, as in the HoTT book, gives function extensionality. A number of us (including Nicolai and me), asked whether hypothetical propositional truncations (which cannot come with stipulated definitional equalities) also give funext. The above argument shows that hypothetical propositional truncations definitely cannot give function extensionality. For, if this were the case, excluded middle would also imply function extensionality. But we know that this is not the case. Best, Martin ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-12 18:10 ` Martin Escardo @ 2017-05-12 18:41 ` Martin Escardo 2017-05-13 21:46 ` Michael Shulman 1 sibling, 0 replies; 17+ messages in thread From: Martin Escardo @ 2017-05-12 18:41 UTC (permalink / raw) To: Michael Shulman; +Cc: HomotopyT...@googlegroups.com Obviously the second side-remark overlooks the fact that we used function extensionality to show that excluded middle implies the existence of propositional truncations. Apologies. Hence the question of whether hypothetical propositional truncations imply function extensionality remains open (although I very much doubt that they do). Martin On 12/05/17 19:10, Martin Escardo wrote: > On 02/05/17 20:04, Michael Shulman wrote: >> Some thoughts: >> >> [...] >> >> - A model of MLTT with function extensionality but no universes is >> given by any locally cartesian closed category (perhaps with >> coproducts if we have binary sum types). It seems that surely not >> every lccc with coproducts is a regular category -- though I don't >> have an example ready to hand, let alone an example that also has >> universes. > > If you assume excluded middle (every proposition is empty or pointed), > and function extensionality, then, as you know, every type X does have a > propositional truncation, namely ¬¬X:=(X->0)->0. > > The universal map is the evaluation map eta:X->¬¬X. If we have f:X->P > for a proposition P, then we get ¬¬f:¬¬X->¬¬P by the functoriality of > double-dualization. By excluded middle we have a map ¬¬P->P, which > composed with ¬¬f gives a map f':¬¬X->P, which in turn establishes the > universality of eta:X->¬¬X among maps of X into propositions (the > uniqueness requirement relies on funext). Therefore, indeed, ¬¬X is the > propositional truncation of X (or, more precisely, ¬¬X, together with > eta:X->¬¬X and the extension procedure f |-> f' and its uniqueness give > the propositional truncation of X). > > (Side-remark. Conversely, if you forget the assumption of excluded > middle, but remember the assumption of function extensionality, then the > assumption that eta:X->¬¬X is the universal map of X into a proposition, > for every X, implies excluded middle. (Exercise.) So, in general, the > propositional truncation of X, if it exists, is wildly different from ¬¬X.) > > The above argument relies on having a universe (first, to formulate > excluded middle and funext, and, second, to formulate and prove the > universality of eta). > > *** What is the interaction (if any) of excluded middle with regularity, > in your thought above? It seems to me that adding a universe is playing > a role. It is different to say externally that all morphisms have > images, than to say this internally using a universe (or am I wrong?). > > A second side-remark is this, which I realized just now while writing > this, although I have known the above for several years: > > We know that the addition of propositional truncations as a rule, with > certain stipulated definitional equalities, as in the HoTT book, gives > function extensionality. > > A number of us (including Nicolai and me), asked whether hypothetical > propositional truncations (which cannot come with stipulated > definitional equalities) also give funext. > > The above argument shows that hypothetical propositional truncations > definitely cannot give function extensionality. For, if this were the > case, excluded middle would also imply function extensionality. But we > know that this is not the case. > > Best, > Martin > ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-12 18:10 ` Martin Escardo 2017-05-12 18:41 ` Martin Escardo @ 2017-05-13 21:46 ` Michael Shulman 2017-05-14 9:54 ` stre... 2017-05-16 6:20 ` Michael Shulman 1 sibling, 2 replies; 17+ messages in thread From: Michael Shulman @ 2017-05-13 21:46 UTC (permalink / raw) To: Martin Escardo; +Cc: HomotopyT...@googlegroups.com On Fri, May 12, 2017 at 11:10 AM, Martin Escardo <escardo...@googlemail.com> wrote: > The above argument relies on having a universe (first, to formulate > excluded middle and funext, and, second, to formulate and prove the > universality of eta). > > *** What is the interaction (if any) of excluded middle with regularity, > in your thought above? It seems to me that adding a universe is playing > a role. It is different to say externally that all morphisms have > images, than to say this internally using a universe (or am I wrong?). Three replies: 1. I don't think the argument technically relies on having a universe. LEM, funext, and the universality of eta are usually stated internally by quantifying over a universe, but they can also be stated as rules with type judgments as premises, and I believe the proof of universality goes through as a derivation of one rule from others. 2. In general, saying something internally is different from saying it externally, but I think that for images (and more generally for universal properties that are stable under pullback and descent) there is no difference. In such cases saying it internally with a universe is the same as saying it externally for the "universal case", which implies its external truth in all other cases. (You can also say it "internally" without a universe using stack semantics.) 3. A Boolean coherent category automatically has a subobject classifier, namely 1+1. Thus, if it is also cartesian closed, it is automatically a topos. > A second side-remark is this, which I realized just now while writing > this, although I have known the above for several years: > > We know that the addition of propositional truncations as a rule, with > certain stipulated definitional equalities, as in the HoTT book, gives > function extensionality. > > A number of us (including Nicolai and me), asked whether hypothetical > propositional truncations (which cannot come with stipulated > definitional equalities) also give funext. > > The above argument shows that hypothetical propositional truncations > definitely cannot give function extensionality. For, if this were the > case, excluded middle would also imply function extensionality. But we > know that this is not the case. > > Best, > Martin ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-13 21:46 ` Michael Shulman @ 2017-05-14 9:54 ` stre... 2017-05-16 6:20 ` Michael Shulman 1 sibling, 0 replies; 17+ messages in thread From: stre... @ 2017-05-14 9:54 UTC (permalink / raw) To: Michael Shulman; +Cc: Martin Escardo, HomotopyT...@googlegroups.com The question is not one of universal properties but of existence. I wo der whether every posetal lccc has binary sups. Every cartesian closd poset is lccc but need not have binary sups, e.g. the free ccc over 1 generator is lccc but has no binary sums. Thomas ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-13 21:46 ` Michael Shulman 2017-05-14 9:54 ` stre... @ 2017-05-16 6:20 ` Michael Shulman 1 sibling, 0 replies; 17+ messages in thread From: Michael Shulman @ 2017-05-16 6:20 UTC (permalink / raw) To: Martin Escardo; +Cc: HomotopyT...@googlegroups.com On Sat, May 13, 2017 at 2:46 PM, Michael Shulman <shu...@sandiego.edu> wrote: > 3. A Boolean coherent category automatically has a subobject > classifier, namely 1+1. Thus, if it is also cartesian closed, it is > automatically a topos. I should have said, a Boolean *extensive* coherent category. Of course, an arbitrary coherent category may not have all coproducts, and if it has coproducts they may not be disjoint (e.g. the posetal case). >> A second side-remark is this, which I realized just now while writing >> this, although I have known the above for several years: >> >> We know that the addition of propositional truncations as a rule, with >> certain stipulated definitional equalities, as in the HoTT book, gives >> function extensionality. >> >> A number of us (including Nicolai and me), asked whether hypothetical >> propositional truncations (which cannot come with stipulated >> definitional equalities) also give funext. >> >> The above argument shows that hypothetical propositional truncations >> definitely cannot give function extensionality. For, if this were the >> case, excluded middle would also imply function extensionality. But we >> know that this is not the case. >> >> Best, >> Martin ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-02 9:09 Does MLTT have "or"? Martin Escardo 2017-05-02 19:04 ` [HoTT] " Michael Shulman @ 2017-05-03 10:55 ` Thomas Streicher 2017-05-03 14:25 ` Martin Escardo 2017-05-03 12:17 ` Andrew Polonsky 2017-05-06 13:51 ` Andrew Swan 3 siblings, 1 reply; 17+ messages in thread From: Thomas Streicher @ 2017-05-03 10:55 UTC (permalink / raw) To: Martin Escardo; +Cc: HomotopyT...@googlegroups.com > (4) What is a model of intensional MLTT with a universe such that > ||-|| doesn't exist? In my 1992 TCS paper I have constructed an impredicative universe within Asm(K_1) (separated objects of effective topos) which is not reflective. The universe consists of all powers of N together with the initial object. All its elements are empty or contain infinitely many global elements. But or is definable `a la Russel-Prawitz. Thomas ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-03 10:55 ` Thomas Streicher @ 2017-05-03 14:25 ` Martin Escardo 2017-05-03 14:48 ` Thomas Streicher 0 siblings, 1 reply; 17+ messages in thread From: Martin Escardo @ 2017-05-03 14:25 UTC (permalink / raw) To: stre...; +Cc: HomotopyT...@googlegroups.com On 03/05/17 11:55, stre...@mathematik.tu-darmstadt.de wrote: >> (4) What is a model of intensional MLTT with a universe such that >> ||-|| doesn't exist? > > In my 1992 TCS paper I have constructed an impredicative universe > within Asm(K_1) (separated objects of effective topos) which is not > reflective. The universe consists of all powers of N together with the > initial object. All its elements are empty or contain infinitely many > global elements. > > But or is definable `a la Russel-Prawitz. What you are saying is that there is model where general propositional truncations don't exist, but "or" does. Right? How difficult is to get a model where "or" doesn't exist either? Best, Martin ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-03 14:25 ` Martin Escardo @ 2017-05-03 14:48 ` Thomas Streicher 2017-05-03 15:04 ` Martin Escardo 0 siblings, 1 reply; 17+ messages in thread From: Thomas Streicher @ 2017-05-03 14:48 UTC (permalink / raw) To: Martin Escardo; +Cc: HomotopyT...@googlegroups.com > What you are saying is that there is model where general propositional > truncations don't exist, but "or" does. Right? yes > How difficult is to get a model where "or" doesn't exist either? depends on what "or" is! in my model Prop has or by impredicativity but this or doen't coincide with sums on the level of types. Thomas ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Does MLTT have "or"? 2017-05-03 14:48 ` Thomas Streicher @ 2017-05-03 15:04 ` Martin Escardo 0 siblings, 0 replies; 17+ messages in thread From: Martin Escardo @ 2017-05-03 15:04 UTC (permalink / raw) To: stre...; +Cc: HomotopyT...@googlegroups.com On 03/05/17 15:48, stre...@mathematik.tu-darmstadt.de wrote: >> What you are saying is that there is model where general propositional >> truncations don't exist, but "or" does. Right? > > yes > >> How difficult is to get a model where "or" doesn't exist either? > > depends on what "or" is! in my model Prop has or by impredicativity > but this or doen't coincide with sums on the level of types. I specified what "or" is in point (2) of the initial message of this thread: (2) The question is whether given any two propositions P and Q we can find a proposition R with P->R and Q->R such that for any proposition R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of P and Q.) Here "proposition" means "type in which any two points are Id-equal". Martin ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: Does MLTT have "or"? 2017-05-02 9:09 Does MLTT have "or"? Martin Escardo 2017-05-02 19:04 ` [HoTT] " Michael Shulman 2017-05-03 10:55 ` Thomas Streicher @ 2017-05-03 12:17 ` Andrew Polonsky 2017-05-03 12:24 ` [HoTT] " Martin Escardo 2017-05-03 12:24 ` Michael Shulman 2017-05-06 13:51 ` Andrew Swan 3 siblings, 2 replies; 17+ messages in thread From: Andrew Polonsky @ 2017-05-03 12:17 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1935 bytes --] If you don't mind the proposition living in a higher universe, then certainly the impredicative encoding will do: P\/Q := ∏(X:U) isProp(X) -> (P -> X) -> (Q -> X) -> X satisfies P -> P\/Q Q -> P\/Q isProp(R) -> (P->R) -> (Q->R) -> (P\/Q -> R) Best, Andrew On Tuesday, May 2, 2017 at 12:45:41 PM UTC-4, Martin Hotzel Escardo wrote: > > Last week in a meeting I had a technical discussion with somebody, who > suggested to post the question here. > > (1) Prove (internally) or disprove (as a meta-theorem, probably with a > counter-model) the following in (intensional) Martin-Loef Type Theory: > > * The poset of subsingletons (or propositions or truth values) has > binary joins (or disjunction). > > (We know it has binary meets and Heyting implication, which amounts to > saying it is a Heyting semilattice. Is it a lattice?) > > (2) The question is whether given any two propositions P and Q we can > find a proposition R with P->R and Q->R such that for any proposition > R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of > P and Q.) > > (3) Of course, if MLTT had propositional truncations ||-||, then the > answer would be R := ||P+Q||. But we can ask this question for MLTT > before we postulate propositional truncations as in (1)-(2). > > (4) What is a model of intensional MLTT with a universe such that > ||-|| doesn't exist? > > More precisely, define, internally in intensional MLTT, > > hasTruncation(X:U) := Σ(X':U), > isProp(X') > × (X→X') > × Π(P:U), (isProp(P) × (X→P)) → (X'→P). > > Is there a model, with universes, the falsifies this? > > Preferably, we want models that falsify this but validate > function extensionality (and perhaps also propositional > extensionality). > > Best, > Martin > [-- Attachment #1.2: Type: text/html, Size: 2397 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Re: Does MLTT have "or"? 2017-05-03 12:17 ` Andrew Polonsky @ 2017-05-03 12:24 ` Martin Escardo 2017-05-03 12:24 ` Michael Shulman 1 sibling, 0 replies; 17+ messages in thread From: Martin Escardo @ 2017-05-03 12:24 UTC (permalink / raw) To: Homotopy Type Theory On 03/05/17 13:17, andrew....@gmail.com wrote: > If you don't mind the proposition living in a higher universe, then > certainly the impredicative encoding will do: > > P\/Q := ∏(X:U) isProp(X) -> (P -> X) -> (Q -> X) -> X Assuming funext to show that this is indeed a proposition. This is equivalent to the large truncation of P+Q discussed in my previous message. As I said, if a small truncation exists, it is equivalent to the large truncation, which always exists for any type, assuming funext. Martin > > satisfies > > P -> P\/Q > Q -> P\/Q > isProp(R) -> (P->R) -> (Q->R) -> (P\/Q -> R) > > Best, > Andrew > > On Tuesday, May 2, 2017 at 12:45:41 PM UTC-4, Martin Hotzel Escardo wrote: > > Last week in a meeting I had a technical discussion with somebody, who > suggested to post the question here. > > (1) Prove (internally) or disprove (as a meta-theorem, probably with a > counter-model) the following in (intensional) Martin-Loef Type Theory: > > * The poset of subsingletons (or propositions or truth values) has > binary joins (or disjunction). > > (We know it has binary meets and Heyting implication, which amounts to > saying it is a Heyting semilattice. Is it a lattice?) > > (2) The question is whether given any two propositions P and Q we can > find a proposition R with P->R and Q->R such that for any proposition > R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of > P and Q.) > > (3) Of course, if MLTT had propositional truncations ||-||, then the > answer would be R := ||P+Q||. But we can ask this question for MLTT > before we postulate propositional truncations as in (1)-(2). > > (4) What is a model of intensional MLTT with a universe such that > ||-|| doesn't exist? > > More precisely, define, internally in intensional MLTT, > > hasTruncation(X:U) := Σ(X':U), > isProp(X') > × (X→X') > × Π(P:U), (isProp(P) × (X→P)) → (X'→P). > > Is there a model, with universes, the falsifies this? > > Preferably, we want models that falsify this but validate > function extensionality (and perhaps also propositional > extensionality). > > Best, > 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:HomotopyTypeThe...@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Re: Does MLTT have "or"? 2017-05-03 12:17 ` Andrew Polonsky 2017-05-03 12:24 ` [HoTT] " Martin Escardo @ 2017-05-03 12:24 ` Michael Shulman 1 sibling, 0 replies; 17+ messages in thread From: Michael Shulman @ 2017-05-03 12:24 UTC (permalink / raw) To: Andrew Polonsky; +Cc: Homotopy Type Theory Note that the "un-resized" impredicative truncation and disjunction, in addition to living in a larger universe themselves, only have the appropriate universal property with respect to propositions in the *smaller* universe. On Wed, May 3, 2017 at 5:17 AM, Andrew Polonsky <andrew....@gmail.com> wrote: > If you don't mind the proposition living in a higher universe, then > certainly the impredicative encoding will do: > > P\/Q := ∏(X:U) isProp(X) -> (P -> X) -> (Q -> X) -> X > > satisfies > > P -> P\/Q > Q -> P\/Q > isProp(R) -> (P->R) -> (Q->R) -> (P\/Q -> R) > > Best, > Andrew > > > On Tuesday, May 2, 2017 at 12:45:41 PM UTC-4, Martin Hotzel Escardo wrote: >> >> Last week in a meeting I had a technical discussion with somebody, who >> suggested to post the question here. >> >> (1) Prove (internally) or disprove (as a meta-theorem, probably with a >> counter-model) the following in (intensional) Martin-Loef Type Theory: >> >> * The poset of subsingletons (or propositions or truth values) has >> binary joins (or disjunction). >> >> (We know it has binary meets and Heyting implication, which amounts to >> saying it is a Heyting semilattice. Is it a lattice?) >> >> (2) The question is whether given any two propositions P and Q we can >> find a proposition R with P->R and Q->R such that for any proposition >> R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of >> P and Q.) >> >> (3) Of course, if MLTT had propositional truncations ||-||, then the >> answer would be R := ||P+Q||. But we can ask this question for MLTT >> before we postulate propositional truncations as in (1)-(2). >> >> (4) What is a model of intensional MLTT with a universe such that >> ||-|| doesn't exist? >> >> More precisely, define, internally in intensional MLTT, >> >> hasTruncation(X:U) := Σ(X':U), >> isProp(X') >> × (X→X') >> × Π(P:U), (isProp(P) × (X→P)) → (X'→P). >> >> Is there a model, with universes, the falsifies this? >> >> Preferably, we want models that falsify this but validate >> function extensionality (and perhaps also propositional >> extensionality). >> >> Best, >> 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] 17+ messages in thread
* Re: Does MLTT have "or"? 2017-05-02 9:09 Does MLTT have "or"? Martin Escardo ` (2 preceding siblings ...) 2017-05-03 12:17 ` Andrew Polonsky @ 2017-05-06 13:51 ` Andrew Swan 2017-05-07 13:49 ` [HoTT] " Martin Escardo 3 siblings, 1 reply; 17+ messages in thread From: Andrew Swan @ 2017-05-06 13:51 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 6651 bytes --] We consider the category "localisation of setoids." That is we take the objects to be sets equipped with an equivalence relation (X, ~), and morphisms (X, ~) -> (Y, ~) to be functions f: X/~ -> Y/~ such that there exists a function f': X -> Y commuting with f and the quotient maps. In ZFC we can show that this category is equivalent to Set, so we already know it is complete, cocomplete and locally cartesian closed. However, it will be important that we can also do this constructively i.e. without using the equivalence with Set. Note that one can give explicit definitions of limits and colimits as well as dependent products that work constructively. Say that a setoid is trivial if the equivalence classes are all singletons. The full subcategory of trivial setoids is isomorphic to the category of sets (and this time the isomorphism works constructively). Note that image factorisation is different in trivial setoids and setoids. Suppose we have some morphism of trivial setoids f: (X, ~) -> (Y, ~) (since these are trivial setoids this is just any map X -> Y). For the image factorisation in setoids, we take the underlying set of im(f) to be X, but change the equivalence relation, to ~' defined by x ~' x' whenever f(x) = f(x'). On the other hand the image factorisation in trivial setoids is the quotient X/~' together with the trivial equivalence relation. Assuming choice these will be isomorphic. However, the key point is that in general the converse also holds, so by working internally in a model of set theory where AC fails, we can get examples where the image factorisations are not isomorphic (ie where the inclusion of subcategory functor does not preserve image factorisation). On the other hand, the rest of the type theoretic structure is preserved by the inclusion functor. Dependent products, finite limits and disjoint sums are all the same in trivial setoids and setoids. We now assume that we have an inaccessible set, stated using a suitable constructive notion of inaccessible. We define a universe U_1 -> U_0 by taking U_0 to be the set of all small trivial setoids, and an element of U_1 is a small trivial setoid together with one of its elements. Take the equivalence relation on U_1 and U_2 to just be trivial. The small maps f: X -> Y are then those which are both small in the usual sense (fibres are isomorphic to elements of the inaccessible set), and also admit a function f': X -> Y which makes a pullback square with f and the quotient maps. Note that if Y is trivial and f: X -> Y is small then X is also trivial. We can also consider another larger universe V_1 -> V_0 which consists of all small setoids. If we interpret type theory in the above category we can almost, but not quite answer question (4). We work internally in the Lifschitz realizability model like in Chen, Rathjen, Lifschitz realizability for intuitionistic Zermelo–Fraenkel set theory <https://link.springer.com/article/10.1007/s00153-012-0299-2>. In type theory we work over the context consisting of binary sequences a: N -> 2 which are 1 at most once, and we consider the propositions P(a) = forall n. a(2n) = 0 and Q(a) = forall n. a(2n + 1) = 0. Call this context A. Then LLPO is the statement that for all a in A, the proposition P(a) \/ Q(a) is true (when disjunction exists at all). If the disjunction ||P \/ Q|| exists, then we would have maps of the form P + Q -> || P + Q || -> A in the model. If || P + Q || belongs to the universe U, then the map || P + Q || -> A would be small, which would make the setoid || P + Q || trivial, and in particular it has to be just a subset of A. On the other hand, if this is still the disjunction of P and Q when we move up to the larger universe V, then it has to be isomorphic to the "real" image factorisation in setoids, which consists of pairs (i, a) where either i = 0 and P(a) holds or i = 1 and Q(a) holds, together with the equivalence relation that identifies (0, a) and (1, a) when both occur in the set. If this was isomorphic to a monomorphism, then, assuming LLPO, we would have a choice function, that selects for each a in A, a choice of i such that i = 0 and P(a) or i = 1 and Q(a). However this is impossible in Lifschitz realizability. I think it's possible to get a complete answer to question (4) by instead working with the arrow category of setoids, and then interpreting the universe as the inclusion of U into V. Finally, the above was working over a context, A, but I think it's also possible to do the same over the empty context, because I have some unpublished results that imply there is a specific computable sequence a: N -> 2 such that IZF + LLPO + MP proves a has at most one 1, but for any definable set, x, IZF + LLPO + MP cannot prove the statement "x belongs to 2, and either x = 0 and P(a) holds or x = 1 and Q(a) holds". Best, Andrew On Tuesday, 2 May 2017 18:45:41 UTC+2, Martín Hötzel Escardó wrote: > > Last week in a meeting I had a technical discussion with somebody, who > suggested to post the question here. > > (1) Prove (internally) or disprove (as a meta-theorem, probably with a > counter-model) the following in (intensional) Martin-Loef Type Theory: > > * The poset of subsingletons (or propositions or truth values) has > binary joins (or disjunction). > > (We know it has binary meets and Heyting implication, which amounts to > saying it is a Heyting semilattice. Is it a lattice?) > > (2) The question is whether given any two propositions P and Q we can > find a proposition R with P->R and Q->R such that for any proposition > R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of > P and Q.) > > (3) Of course, if MLTT had propositional truncations ||-||, then the > answer would be R := ||P+Q||. But we can ask this question for MLTT > before we postulate propositional truncations as in (1)-(2). > > (4) What is a model of intensional MLTT with a universe such that > ||-|| doesn't exist? > > More precisely, define, internally in intensional MLTT, > > hasTruncation(X:U) := Σ(X':U), > isProp(X') > × (X→X') > × Π(P:U), (isProp(P) × (X→P)) → (X'→P). > > Is there a model, with universes, the falsifies this? > > Preferably, we want models that falsify this but validate > function extensionality (and perhaps also propositional > extensionality). > > Best, > Martin > [-- Attachment #1.2: Type: text/html, Size: 7185 bytes --] ^ permalink raw reply [flat|nested] 17+ messages in thread
* Re: [HoTT] Re: Does MLTT have "or"? 2017-05-06 13:51 ` Andrew Swan @ 2017-05-07 13:49 ` Martin Escardo 0 siblings, 0 replies; 17+ messages in thread From: Martin Escardo @ 2017-05-07 13:49 UTC (permalink / raw) To: Homotopy Type Theory Interesting! Martin On 06/05/17 14:51, Andrew Swan wrote: > We consider the category "localisation of setoids." That is we take the > objects to be sets equipped with an equivalence relation (X, ~), and > morphisms (X, ~) -> (Y, ~) to be functions f: X/~ -> Y/~ such that there > exists a function f': X -> Y commuting with f and the quotient maps. In > ZFC we can show that this category is equivalent to Set, so we already > know it is complete, cocomplete and locally cartesian closed. However, > it will be important that we can also do this constructively i.e. > without using the equivalence with Set. Note that one can give explicit > definitions of limits and colimits as well as dependent products that > work constructively. > > Say that a setoid is trivial if the equivalence classes are all > singletons. The full subcategory of trivial setoids is isomorphic to the > category of sets (and this time the isomorphism works constructively). > > Note that image factorisation is different in trivial setoids and > setoids. Suppose we have some morphism of trivial setoids f: (X, ~) -> > (Y, ~) (since these are trivial setoids this is just any map X -> Y). > For the image factorisation in setoids, we take the underlying set of > im(f) to be X, but change the equivalence relation, to ~' defined by x > ~' x' whenever f(x) = f(x'). On the other hand the image factorisation > in trivial setoids is the quotient X/~' together with the trivial > equivalence relation. Assuming choice these will be isomorphic. However, > the key point is that in general the converse also holds, so by working > internally in a model of set theory where AC fails, we can get examples > where the image factorisations are not isomorphic (ie where the > inclusion of subcategory functor does not preserve image factorisation). > > On the other hand, the rest of the type theoretic structure is preserved > by the inclusion functor. Dependent products, finite limits and disjoint > sums are all the same in trivial setoids and setoids. > > We now assume that we have an inaccessible set, stated using a suitable > constructive notion of inaccessible. We define a universe U_1 -> U_0 by > taking U_0 to be the set of all small trivial setoids, and an element of > U_1 is a small trivial setoid together with one of its elements. Take > the equivalence relation on U_1 and U_2 to just be trivial. The small > maps f: X -> Y are then those which are both small in the usual sense > (fibres are isomorphic to elements of the inaccessible set), and also > admit a function f': X -> Y which makes a pullback square with f and the > quotient maps. Note that if Y is trivial and f: X -> Y is small then X > is also trivial. We can also consider another larger universe V_1 -> V_0 > which consists of all small setoids. > > If we interpret type theory in the above category we can almost, but not > quite answer question (4). We work internally in the Lifschitz > realizability model like in Chen, Rathjen, Lifschitz realizability for > intuitionistic Zermelo–Fraenkel set theory > <https://link.springer.com/article/10.1007/s00153-012-0299-2>. In type > theory we work over the context consisting of binary sequences a: N -> 2 > which are 1 at most once, and we consider the propositions P(a) = forall > n. a(2n) = 0 and Q(a) = forall n. a(2n + 1) = 0. Call this context A. > Then LLPO is the statement that for all a in A, the proposition P(a) \/ > Q(a) is true (when disjunction exists at all). If the disjunction ||P \/ > Q|| exists, then we would have maps of the form P + Q -> || P + Q || -> > A in the model. If || P + Q || belongs to the universe U, then the map > || P + Q || -> A would be small, which would make the setoid || P + Q || > trivial, and in particular it has to be just a subset of A. On the other > hand, if this is still the disjunction of P and Q when we move up to the > larger universe V, then it has to be isomorphic to the "real" image > factorisation in setoids, which consists of pairs (i, a) where either i > = 0 and P(a) holds or i = 1 and Q(a) holds, together with the > equivalence relation that identifies (0, a) and (1, a) when both occur > in the set. If this was isomorphic to a monomorphism, then, assuming > LLPO, we would have a choice function, that selects for each a in A, a > choice of i such that i = 0 and P(a) or i = 1 and Q(a). However this is > impossible in Lifschitz realizability. > > I think it's possible to get a complete answer to question (4) by > instead working with the arrow category of setoids, and then > interpreting the universe as the inclusion of U into V. > > Finally, the above was working over a context, A, but I think it's also > possible to do the same over the empty context, because I have some > unpublished results that imply there is a specific computable sequence > a: N -> 2 such that IZF + LLPO + MP proves a has at most one 1, but for > any definable set, x, IZF + LLPO + MP cannot prove the statement "x > belongs to 2, and either x = 0 and P(a) holds or x = 1 and Q(a) holds". > > > Best, > Andrew > > > On Tuesday, 2 May 2017 18:45:41 UTC+2, Martín Hötzel Escardó wrote: > > Last week in a meeting I had a technical discussion with somebody, who > suggested to post the question here. > > (1) Prove (internally) or disprove (as a meta-theorem, probably with a > counter-model) the following in (intensional) Martin-Loef Type Theory: > > * The poset of subsingletons (or propositions or truth values) has > binary joins (or disjunction). > > (We know it has binary meets and Heyting implication, which amounts to > saying it is a Heyting semilattice. Is it a lattice?) > > (2) The question is whether given any two propositions P and Q we can > find a proposition R with P->R and Q->R such that for any proposition > R' with P->R' and Q->R' we have R->R'. (R is the least upper bound of > P and Q.) > > (3) Of course, if MLTT had propositional truncations ||-||, then the > answer would be R := ||P+Q||. But we can ask this question for MLTT > before we postulate propositional truncations as in (1)-(2). > > (4) What is a model of intensional MLTT with a universe such that > ||-|| doesn't exist? > > More precisely, define, internally in intensional MLTT, > > hasTruncation(X:U) := Σ(X':U), > isProp(X') > × (X→X') > × Π(P:U), (isProp(P) × (X→P)) → (X'→P). > > Is there a model, with universes, the falsifies this? > > Preferably, we want models that falsify this but validate > function extensionality (and perhaps also propositional > extensionality). > > Best, > 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:HomotopyTypeThe...@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 17+ messages in thread
end of thread, other threads:[~2017-05-16 6:20 UTC | newest] Thread overview: 17+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-05-02 9:09 Does MLTT have "or"? Martin Escardo 2017-05-02 19:04 ` [HoTT] " Michael Shulman 2017-05-03 6:47 ` Martin Escardo 2017-05-12 18:10 ` Martin Escardo 2017-05-12 18:41 ` Martin Escardo 2017-05-13 21:46 ` Michael Shulman 2017-05-14 9:54 ` stre... 2017-05-16 6:20 ` Michael Shulman 2017-05-03 10:55 ` Thomas Streicher 2017-05-03 14:25 ` Martin Escardo 2017-05-03 14:48 ` Thomas Streicher 2017-05-03 15:04 ` Martin Escardo 2017-05-03 12:17 ` Andrew Polonsky 2017-05-03 12:24 ` [HoTT] " Martin Escardo 2017-05-03 12:24 ` Michael Shulman 2017-05-06 13:51 ` Andrew Swan 2017-05-07 13:49 ` [HoTT] " Martin Escardo
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).