Re: Does MLTT have "or"?

[Andrew Swan <wakeli...@gmail.com>]

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