Quotients

[Andrej Bauer]

I am writing up the chapter on real numbers and I have a question
about quotients.

Suppose A is a type and E is an equivalence relation on A
(prop-valued). Can a sequence f : N -> A/E be lifted to N -> A?

I believe this is not the case, but would like to make sure. Even
though A/E is constructed as a hit with a single constructor i : A ->
A/E, this does *not* imply that every element in A/E is of the form
i(x).

Is this correct?

With kind regards,

Andrej

[Peter LeFanu Lumsdaine]

Yes.  If N-sequence lifted, then in particular, individual elements would lift.  Look at the topos model of (covariant, Reedy, simplicial) presheaves on (L —> M <— R).  In this, look at the object A = (1 —> 1 + 1 <— 1), with the coproduct inclusions as maps, and the equivalence relation on it declaring any two elements to be equal.  Then the set quotient is (1 —> 1 <— 1), which has a global element (and so a constant global N-sequence); but A itself has no global element, so no global N-sequence.

[Guillaume Brunerie]

I think you have to interpret Andrej’s question as being (-1)-truncated.
Individual elements of A/E merely lift to elements of A, because you
can apply the elimination rule of A/E : for the point constructor you
get what you want and the path constructor is taken care of by the
(-1)-truncation.
But I think that an infinite sequence of elements of A/E do not even
merely lift to A because intuitively you would have to apply the
elimination rule an infinite number of times which is not possible.

I don’t have a counter-example but presumably it should not be too
hard to find one.

Guillaume

2013/3/9 Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>:

> --
> You received this message because you are subscribed to the Google Groups
> "IAS Univalent Foundations" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to univalent-founda...@googlegroups.com.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at
> http://groups.google.com/group/univalent-foundations?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[Peter LeFanu Lumsdaine]

On Sat, Mar 9, 2013 at 3:23 PM, Guillaume Brunerie <guillaume...@gmail.com> wrote:

I think you have to interpret Andrej’s question as being (-1)-truncated.
Individual elements of A/E merely lift to elements of A, because you
can apply the elimination rule of A/E : for the point constructor you
get what you want and the path constructor is taken care of by the
(-1)-truncation.
But I think that an infinite sequence of elements of A/E do not even
merely lift to A because intuitively you would have to apply the
elimination rule an infinite number of times which is not possible.

I don’t have a counter-example but presumably it should not be too
hard to find one.

Ah, OK — yes, that makes sense.  In that case, this is equivalent to countable h-prop choice; that is,

“if A_n is a family of types, and for each n, there merely exists some element of A_n, then there merely exists some function f : forall n, A_n.”

(To see how this version implies Andrej’s statement, take a sequence f : N —> A/E, and for each n let A_n be { x : A & i(x) = f(n) }; conversely, assuming Andrej’s statement, recover this version by taking A = { n : N & A_n }, taking E to identify (n,x) with (m,y) just if m = n; and taking the sequence in A/E where f(n) witnesses the fact that there merely exists some inhabitant of A_n.)

Looking again for traditional topos-theoretic counterexamples, countable choice always holds in presheaf models; to make it fail, one has to move to sheaf models in which a countable sequence of covers can fail to have a common refinement.  So for instance it fails in sheaves over the reals, and this is not too hard to show.  But do we have an extension of any such sheaf model to the type theory yet?  Or can we alternatively find a non-topos-theoretic counterexample by using non-h-set types?

–p.

[Michael Shulman]

I agree, individual elements merely lift, while sequences lifting is countable choice. (Isn't this issue the reason for defining the reals as an HIT?)

We do have arbitrary sheaf models as long as you don't also want strict univalence. Simplicial presheaves with a left exact localization of the injective model structure are a type-theoretic model category and satisfy the hypotheses of the HIT semantic construction. But in general they only have 'universes' that are homotopy-a-la-tarski.

[Vladimir Voevodsky]

On Mar 9, 2013, at 8:20 PM, Michael Shulman wrote:

I agree, individual elements merely lift, while sequences lifting is countable choice. (Isn't this issue the reason for defining the reals as an HIT?)

We do have arbitrary sheaf models as long as you don't also want strict univalence. Simplicial presheaves with a left exact localization of the injective model structure are a type-theoretic model category and satisfy the hypotheses of the HIT semantic construction. But in general they only have 'universes' that are homotopy-a-la-tarski.

What is "homotopy-a-la-tarski" ? V.

[Michael Shulman]

I mean there is a 'universe' type U and a coercion El from terms of type U to types, plus operations on U like

Pi : forall a:U, (El a -> U) -> U

but El only respects these operations up to equivalence, e.g. we have

El(Pi a b) \simeq forall x:El a, El (b x)

rather than a definitional equality as is more usual and convenient. I think this is what we get directly from an infty-categorical object classifier: the universal type family El is a fibration of fibrant objects that represents the universal morphism in the infty-category, so that every k-small morphism is a homotopy pullback of it. In particular, the fibrations like ' forall x:El a, El (b x) ' are k-small, allowing us to choose some morphism Pi which classifies them up to homotopy.

[Dan Licata]

On Mar10, Michael Shulman wrote:
> I mean there is a 'universe' type U and a coercion El from terms of type U
> to types, plus operations on U like
>
> Pi : forall a:U, (El a -> U) -> U
>
> but El only respects these operations up to equivalence, e.g. we have
>
> El(Pi a b) \simeq forall x:El a, El (b x)
>
> rather than a definitional equality as is more usual and convenient.

On the other hand, if you think of the big universe as the Martin-Lof
logical framework level, then an equivalence and not a definitional
equality is what you would expect: In this style, pi-sets are introduced
by a constructor

lambda : (forall x:El a -> El (b x)) -> El (Pi a b)

and eliminated by pattern-matching on lambda. From this you can define

app : El (Pi a b) -> (forall x:El a -> El (b x))

and, modulo having a big identity type with function extensionality for
"forall", you should be able to prove that the two are mutually inverse.
So you'd get an equivalence, but not a definitional equality.

-Dan

[Vladimir Voevodsky]

On Mar 10, 2013, at 1:29 PM, Michael Shulman wrote:

I mean there is a 'universe' type U and a coercion El from terms of type U to types, plus operations on U like

Pi : forall a:U, (El a -> U) -> U

but El only respects these operations up to equivalence, e.g. we have

El(Pi a b) \simeq forall x:El a, El (b x)

rather than a definitional equality as is more usual and convenient. I think this is what we get directly from an infty-categorical object classifier: the universal type family El is a fibration of fibrant objects that represents the universal morphism in the infty-category, so that every k-small morphism is a homotopy pullback of it. In particular, the fibrations like ' forall x:El a, El (b x) ' are k-small, allowing us to choose some morphism Pi which classifies them up to homotopy.

From what you wrote it only follows that they are k-small up to homotopy. V.

[Peter LeFanu Lumsdaine]

By the way, does anyone know if/where this definition (i.e. a universe closed under operations that have the right universal properties, but don’t necessarily agree definitionally with the actual type-constructors of the theory) has previously been considered in the literature?  As Dan points out, it arises very naturally from purely type-theoretic motivations, not just homotopy-theoretic — but I remember looking around for it at some point, and couldn’t find it.  But it seems like it should surely exist somewhere!

–p.

--

[Joachim Kock]

Without being too sure about the definition of universe in
type theory, I think this is the kind of universes constructed
in Section 6 of [Gepner-Kock, Univalence in locally cartesian
closed infinity-categories, arXiv:1208.1749].

> On 10/03/2013 21:28 , Vladimir Voevodsky wrote:
>
> From what you wrote it only follows that they are k-small up to
> homotopy. V.

'k-small' should be taken to mean 'relatively k-compact'.

Cheers,
Joachim.

[Guillaume Brunerie]

On 2013/3/10 Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:
> By the way, does anyone know if/where this definition (i.e. a universe
> closed under operations that have the right universal properties, but don’t
> necessarily agree definitionally with the actual type-constructors of the
> theory) has previously been considered in the literature? As Dan points
> out, it arises very naturally from purely type-theoretic motivations, not
> just homotopy-theoretic — but I remember looking around for it at some
> point, and couldn’t find it. But it seems like it should surely exist
> somewhere!

In Martin Hofmann’s "Syntax and Semantics of Dependent Types" this is
taken as the definition of a universe (section 2.1.6).
He says that we could assert a definitional equality of types instead,
but that there are various disadvantages, in particular that in many
models the definitional equality of types is not valid under the
canonical interpretation of Pi.

Guillaume

[Michael Shulman]

On Mar 10, 2013 6:35 PM, "Joachim Kock" <ko...@mat.uab.cat> wrote:
>> From what you wrote it only follows that they are k-small up to
>> homotopy. V.
>
> 'k-small' should be taken to mean 'relatively k-compact'.

Indeed -- the point is that smallness is in the infty-categorical sense.

[Vladimir Voevodsky]

On Mar 10, 2013, at 9:11 PM, Peter LeFanu Lumsdaine wrote:

> By the way, does anyone know if/where this definition (i.e. a universe closed under operations that have the right universal properties, but don’t necessarily agree definitionally with the actual type-constructors of the theory) has previously been considered in the literature? As Dan points out, it arises very naturally from purely type-theoretic motivations, not just homotopy-theoretic — but I remember looking around for it at some point, and couldn’t find it. But it seems like it should surely exist somewhere!
>
> –p.
>

BTW if having such universes would be sufficient for constructing a model it would justify the resizing rules.

V.

[Michael Shulman]

On Sun, Mar 10, 2013 at 7:03 PM, Guillaume Brunerie
<guillaume...@gmail.com> wrote:
> In Martin Hofmann’s "Syntax and Semantics of Dependent Types" this is
> taken as the definition of a universe (section 2.1.6).
> He says that we could assert a definitional equality of types instead,
> but that there are various disadvantages, in particular that in many
> models the definitional equality of types is not valid under the
> canonical interpretation of Pi.

Nice! I did not realize that.

Maybe this really is a useful direction to go in, then.