Does MLTT have "or"?

Does MLTT have "or"?

[Martin Escardo]

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

Re: [HoTT] Does MLTT have "or"?

[Michael Shulman]

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.

Re: [HoTT] Does MLTT have "or"?

[Martin Escardo]

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

Re: [HoTT] Does MLTT have "or"?

[Thomas Streicher]

> (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

Re: Does MLTT have "or"?

[Andrew Polonsky]

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

Re: [HoTT] Re: Does MLTT have "or"?

[Martin Escardo]

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.

Re: [HoTT] Re: Does MLTT have "or"?

[Michael Shulman]

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.

Re: [HoTT] Does MLTT have "or"?

[Martin Escardo]

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

Re: [HoTT] Does MLTT have "or"?

[Thomas Streicher]

> 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

Re: [HoTT] Does MLTT have "or"?

[Martin Escardo]

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

Re: Does MLTT have "or"?

[Andrew Swan]

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

Re: [HoTT] Re: Does MLTT have "or"?

[Martin Escardo]

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.

Re: [HoTT] Does MLTT have "or"?

[Martin Escardo]

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

Re: [HoTT] Does MLTT have "or"?

[Martin Escardo]

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
> 

Re: [HoTT] Does MLTT have "or"?

[Michael Shulman]

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

Re: [HoTT] Does MLTT have "or"?

[stre...]

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

Re: [HoTT] Does MLTT have "or"?

[Michael Shulman]

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