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

[Martin Escardo <escardo...@googlemail.com>]

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.