3 views

Skip to first unread message

Mar 4, 2014, 11:58:01 AM3/4/14

to homotopyt...@googlegroups.com

Hi,

I managed, after much hackery, to prove in Coq that functional extensionality is downward closed (that is, if functional extensionality is true in U_i, then it is true in U_j for all j <= i). (I suspect an Agda proof would be much less hacky.) Is univalence downward closed? That is, if U_{i + 1} is univalent, is U_i also necessarily univalent? (Apologies if this is answered somewhere in The Book.) My intuition is that this is not the case, because even though we know that paths in U_{i+1} are just equivalences, we don't know that these paths lie entirely in U_i. But I'm not sure how to make this intuition more rigorous.

Thanks,

Jason

Mar 4, 2014, 12:11:15 PM3/4/14

to Jason Gross, homotopyt...@googlegroups.com

Your intuition agrees with mine. In the simplicial set model, for

instance, we could let U_{i+1} be an ordinary univalent universe and

U_i be a discrete simplicial set on some of its vertices.

> --

> 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/groups/opt_out.

instance, we could let U_{i+1} be an ordinary univalent universe and

U_i be a discrete simplicial set on some of its vertices.

> 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/groups/opt_out.

Mar 4, 2014, 12:26:57 PM3/4/14

to Michael Shulman, Jason Gross, homotopyt...@googlegroups.com

This is my intuition as well, but it’s not totally clear to me that it couldn’t depend on some of the subtleties in the rules taken for universes.

If one has universes à la Tarski — the coercion between elements-of-universes and type is explicit — and the cumulativity between universes is an explicit embedding, then certainly the simplicial model shows that one could have a discrete universe inside a univalent one, or vice versa.

But if some of those coercions are made invisible, it’s less clear to me whether the simplicial model will still work. I’d likewise suspect this is still consistent even with Coq-style judgementally-cumulative universes, but there are at least some non-trivial details to check, I think?

–p.

Mar 4, 2014, 4:14:19 PM3/4/14

to Jason Gross, Prof. Vladimir Aleksandrovich Voevodsky, homotopyt...@googlegroups.com

On Mar 4, 2014, at 11:58 AM, Jason Gross <jason...@gmail.com> wrote:

Hi,I managed, after much hackery, to prove in Coq that functional extensionality is downward closed (that is, if functional extensionality is true in U_i, then it is true in U_j for all j <= i). (I suspect an Agda proof would be much less hacky.) Is univalence downward closed? That is, if U_{i + 1} is univalent, is U_i also necessarily univalent?

Of course not. Nothing prevents one to build a model of a system with two (or any number of) universes U0 U1 where U0 : U1 and U0 is a subset of U1 and U1 is univalent while U0 is not. Or, for that matter, where U0 is univalent and U1 is not.

V.

(Apologies if this is answered somewhere in The Book.) My intuition is that this is not the case, because even though we know that paths in U_{i+1} are just equivalences, we don't know that these paths lie entirely in U_i. But I'm not sure how to make this intuition more rigorous.Thanks,Jason

Mar 5, 2014, 3:44:27 AM3/5/14

to Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

> Of course not. Nothing prevents one to build a model of a system with two (or any number of) universes U0 U1 where U0 : U1 and U0 is a subset of U1 and U1 is univalent while U0 is not. Or, for that matter, where U0 is univalent and U1 is not.

Could you, please, explain that. I do see the following problem.
If we have on U1 a notion of equality as isomorphism then this induces

the same notion of equality on U0. That's what we get when we

construct universes the way I and Andr'e suggested (namely from nested

Grothendieck universes).

I guess, you think of a combined intensional/extensional type theory

as suggested by sSet. But then intensional is a particular case of

extensional since the former is obtained from the latter by restricting

to Kan complexes/fibrations. This is quite opposite to what one

usually does namely quotienting/restricting the intensional model to

an extensional one.

Thomas

Mar 5, 2014, 11:51:41 AM3/5/14

to Thomas Streicher, Prof. Vladimir Aleksandrovich Voevodsky, Jason Gross, homotopyt...@googlegroups.com

I am not sure what surprises you. Clearly there is a model in which all universes are sets (discrete simplicial sets). Then there is a univalent model. Then one can mix the two.

V.

V.

Mar 5, 2014, 1:08:08 PM3/5/14

to Vladimir Voevodsky, Thomas Streicher, homotopyt...@googlegroups.com

Perhaps the question is what the relation is, if any, between Id_{U_n} A B and Id_{U_{n+1}} A B, for A : U_n, B : U_n. We have at least the following:

- lift_id : Id_{U_n} A B -> Id_{U_{n+1}} A B
- If U_n is univalent, then we get the composition Id_{U_{n+1}} A B -> Equiv A B -> Id_{U_n} A B (the first by path induction and the section by univalence). I believe this function is an equivalence (with inverse lift_id), because both functions send refl to refl. (This implies that if U_n is univalent, then U_{n+1} cannot satisfy UIP. Is this correct?)

There is the question of whether or not having U_{n+1} be univalent is sufficient to make lift_id an equivalence. The consensus on this thread seems to be that it is not. In some ways, this seems strange, because if U_{n+1} is univalent, then Id_{U_{n+1}} A B is equivalent to a type living in the same universe as Id_{U_n} A B, i.e., Id_{U_{n+1}} lives in a larger universe than it "needs" to, and so it seems natural to conjecture that it can be lowered. Furthermore, Equiv A B does satisfy an equivalence induction principle, so if you do not keep the universes fixed in your head, it is easy to forget that the equivalence induction principle it satisfies talks about functions taking things in U_{n+1}.

-Jason

Mar 5, 2014, 2:19:46 PM3/5/14

to Jason Gross, Vladimir Voevodsky, Thomas Streicher, homotopyt...@googlegroups.com

On Wed, Mar 5, 2014 at 10:08 AM, Jason Gross <jason...@gmail.com> wrote:

> lift_id : Id_{U_n} A B -> Id_{U_{n+1}} A B

> If U_n is univalent, then we get the composition Id_{U_{n+1}} A B -> Equiv A

> B -> Id_{U_n} A B (the first by path induction and the section by

> univalence). I believe this function is an equivalence (with inverse

> lift_id), because both functions send refl to refl. (This implies that if

> U_n is univalent, then U_{n+1} cannot satisfy UIP. Is this correct?)

That looks right to me. It shouldn't be hard to verify it in Coq or Agda.
> lift_id : Id_{U_n} A B -> Id_{U_{n+1}} A B

> If U_n is univalent, then we get the composition Id_{U_{n+1}} A B -> Equiv A

> B -> Id_{U_n} A B (the first by path induction and the section by

> univalence). I believe this function is an equivalence (with inverse

> lift_id), because both functions send refl to refl. (This implies that if

> U_n is univalent, then U_{n+1} cannot satisfy UIP. Is this correct?)

Of course, this doesn't imply that U_{n+1} is itself univalent;

univalence could fail for types in U_{n+1} that aren't in U_n. For

instance, in the groupoid model, the univalent groupoid of sets is

contained in the non-univalent groupoid of groupoids.

> There is the question of whether or not having U_{n+1} be univalent is

> sufficient to make lift_id an equivalence. The consensus on this thread

> seems to be that it is not. In some ways, this seems strange, because if

> U_{n+1} is univalent, then Id_{U_{n+1}} A B is equivalent to a type living

> in the same universe as Id_{U_n} A B, i.e., Id_{U_{n+1}} lives in a larger

> universe than it "needs" to, and so it seems natural to conjecture that it

> can be lowered.

thing in U_n it is equivalent to should be Id_{U_n} A B.

It may also be worth pointing out that with (non-higher)

induction-recursion, one can construct a universe that is a set (and

in particular, not univalent) inside any given universe. (Of course,

we haven't shown yet that IR is consistent with univalence.)

Mike

Mar 5, 2014, 3:36:36 PM3/5/14

to Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

> I am not sure what surprises you. Clearly there is a model in which all universes are sets (discrete simplicial sets). Then there is a univalent model. Then one can mix the two.

Equality on discrete simplicial sets is finer than the one on Kan
complexes. So is is not a subuniverse.

Thomas

Mar 5, 2014, 4:46:48 PM3/5/14

to Jason Gross, Vladimir Voevodsky, Thomas Streicher, homotopyt...@googlegroups.com

On Wed, Mar 5, 2014 at 1:08 PM, Jason Gross <jason...@gmail.com> wrote:

Perhaps the question is what the relation is, if any, between Id_{U_n} A B and Id_{U_{n+1}} A B, for A : U_n, B : U_n. We have at least the following:

- lift_id : Id_{U_n} A B -> Id_{U_{n+1}} A B
- If U_n is univalent, then we get the composition Id_{U_{n+1}} A B -> Equiv A B -> Id_{U_n} A B (the first by path induction and the section by univalence). I believe this function is an equivalence (with inverse lift_id), because both functions send refl to refl. (This implies that if U_n is univalent, then U_{n+1} cannot satisfy UIP. Is this correct?)

I don’t see why this function — call it [lower_id] — is an equivalence? I see how refl-preservation implies that [lower_id] and [lift_id] express Id_{U_{n}} (equivalently, Equiv A B) as a retract of Ud_{U_{n+1}}. But I’m not seeing how to show that they’re inverse the other way round as well.

On the other hand, I can’t think of a counter-model to it — that is, a model where U_n is univalent, but where the map U_n -> U_{n+1} is not an equivalence on Id-types.

There is the question of whether or not having U_{n+1} be univalent is sufficient to make lift_id an equivalence. The consensus on this thread seems to be that it is not. In some ways, this seems strange, because if U_{n+1} is univalent, then Id_{U_{n+1}} A B is equivalent to a type living in the same universe as Id_{U_n} A B, i.e., Id_{U_{n+1}} lives in a larger universe than it "needs" to, and so it seems natural to conjecture that it can be lowered. Furthermore, Equiv A B does satisfy an equivalence induction principle, so if you do not keep the universes fixed in your head, it is easy to forget that the equivalence induction principle it satisfies talks about functions taking things in U_{n+1}.

Yes, this is an interesting subtlety. The model with U_n discrete and U_{n+1} univalent gives some intuition for it, I think: the elimination principle of Equiv A B will hold only for goal predicates where at least one of A, B is generalised over U_{n+1} — in other words, only for predicates that are varying continuously/naturally in A, B, as opposed to predicates defined just over A,B:U_n, which may be disconcinuous/unnatural.

–p.

Mar 5, 2014, 5:05:42 PM3/5/14

to Thomas Streicher, Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

What definition of subuniverse do you have in mind (either as a categorical definition, or rules of syntax) that forbids the smaller universe having a finer equality?

If the rules one takes for universes are as follows (or weaker), then I’m confident that the simplicial model (as presented in Chris’, Vladimir’s and my paper arXiv:1211.2851) allows one to take a non-univalent U_0 living as a sub-universe of a univalent U_1:

(1) Both universes are “à la Tarski”: there is a predicate A:U_i |— El_i(A) Type

(2) The universes are equipped with operations mirroring all constructors on types, commuting definitionally with El_i, e.g.

A,B:U_i |— A +_i B : U_i

A,B:U_i |— El_i (A +_i B) = El_i(A) + El_i(B)

(3) There is a map j : U_0 -> U_1, commuting definitionally with both El and the type-constructor operations, i.e.

A : U_0 |— j(A) : U_1

A : U_0 |— El_1(j(A)) = El_0(A)

A,B : U_0 |— j(A +_0 B) = j(A) +_1 j(B)

–p.

Mar 5, 2014, 5:28:40 PM3/5/14

to Jason Gross, Prof. Vladimir Aleksandrovich Voevodsky, Thomas Streicher, homotopyt...@googlegroups.com

On Mar 5, 2014, at 1:08 PM, Jason Gross <jason...@gmail.com> wrote:

Perhaps the question is what the relation is, if any, between Id_{U_n} A B and Id_{U_{n+1}} A B, for A : U_n, B : U_n. We have at least the following:

- lift_id : Id_{U_n} A B -> Id_{U_{n+1}} A B
- If U_n is univalent, then we get the composition Id_{U_{n+1}} A B -> Equiv A B -> Id_{U_n} A B (the first by path induction and the section by univalence). I believe this function is an equivalence (with inverse lift_id), because both functions send refl to refl. (This implies that if U_n is univalent, then U_{n+1} cannot satisfy UIP. Is this correct?)
There is the question of whether or not having U_{n+1} be univalent is sufficient to make lift_id an equivalence. The consensus on this thread seems to be that it is not. In some ways, this seems strange, because if U_{n+1} is univalent, then Id_{U_{n+1}} A B is equivalent to a type living in the same universe as Id_{U_n} A B, i.e., Id_{U_{n+1}} lives in a larger universe than it "needs" to, and so it seems natural to conjecture that it can be lowered. Furthermore, Equiv A B does satisfy an equivalence induction principle, so if you do not keep the universes fixed in your head, it is easy to forget that the equivalence induction principle it satisfies talks about functions taking things in U_{n+1}.

Right. The reason the induction principle does not imply that equivalences give identities in U_n is that not every family over U_n can be extended to as family over U_{n+1}.

V.

Mar 5, 2014, 5:36:33 PM3/5/14

to Michael Shulman, Prof. Vladimir Aleksandrovich Voevodsky, Jason Gross, Thomas Streicher, homotopyt...@googlegroups.com

On Mar 5, 2014, at 2:19 PM, Michael Shulman <shu...@sandiego.edu> wrote:

> On Wed, Mar 5, 2014 at 10:08 AM, Jason Gross <jason...@gmail.com> wrote:

>> lift_id : Id_{U_n} A B -> Id_{U_{n+1}} A B

>> If U_n is univalent, then we get the composition Id_{U_{n+1}} A B -> Equiv A

>> B -> Id_{U_n} A B (the first by path induction and the section by

>> univalence). I believe this function is an equivalence (with inverse

>> lift_id), because both functions send refl to refl. (This implies that if

>> U_n is univalent, then U_{n+1} cannot satisfy UIP. Is this correct?)

>

> That looks right to me. It shouldn't be hard to verify it in Coq or Agda.

>

> Of course, this doesn't imply that U_{n+1} is itself univalent;

> univalence could fail for types in U_{n+1} that aren't in U_n. For

> instance, in the groupoid model, the univalent groupoid of sets is

> contained in the non-univalent groupoid of groupoids.

V.

Mar 5, 2014, 5:43:50 PM3/5/14

to Thomas Streicher, Prof. Vladimir Aleksandrovich Voevodsky, Jason Gross, homotopyt...@googlegroups.com

V.

Mar 5, 2014, 6:11:15 PM3/5/14

to Peter LeFanu Lumsdaine, Vladimir Voevodsky, Thomas Streicher, homotopyt...@googlegroups.com

On Wed, Mar 5, 2014 at 4:46 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:

On Wed, Mar 5, 2014 at 1:08 PM, Jason Gross <jason...@gmail.com> wrote:

Perhaps the question is what the relation is, if any, between Id_{U_n} A B and Id_{U_{n+1}} A B, for A : U_n, B : U_n. We have at least the following:

- lift_id : Id_{U_n} A B -> Id_{U_{n+1}} A B
I don’t see why this function — call it [lower_id] — is an equivalence? I see how refl-preservation implies that [lower_id] and [lift_id] express Id_{U_{n}} (equivalently, Equiv A B) as a retract of Ud_{U_{n+1}}. But I’m not seeing how to show that they’re inverse the other way round as well.

Indeed, I think you're right; I was thinking that path induction would do the trick, but I see now that [lower_id] is not well-defined across the induction on its argument.

-Jason

Mar 5, 2014, 7:25:24 PM3/5/14

to Jason Gross, Peter LeFanu Lumsdaine, Vladimir Voevodsky, Thomas Streicher, homotopyt...@googlegroups.com

And apparently I fell into the same trap.

We do have Equiv A B -> Id_{U_{n+1}} A B, which is a sort of "weak

univalence" property for U_{n+1} at A and B.

We do have Equiv A B -> Id_{U_{n+1}} A B, which is a sort of "weak

univalence" property for U_{n+1} at A and B.

Mar 6, 2014, 9:46:27 AM3/6/14

to Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

> I suppose I was not precise enough. I should not have said that U0

> is a subset in U1 just that there is a function U0 to U1 compatible

> with the El constructor

My reading was the following as in my very old book.
> is a subset in U1 just that there is a function U0 to U1 compatible

> with the El constructor

Let p0 : E0 -> U0 and p1 : E1 -> U1 be universes. Then the first is a

subuniverse of the second iff

1) there is a mono m : U0 >-> U1 such that m^*p1 \cong p0

2) the terminal projection U0 -> 1 appears as pullback of p1

If, as you suggest, in 1) m need not be a mono but can be an arbitrary

map then it's, od course, possible.

Thomas

Mar 6, 2014, 11:36:36 AM3/6/14

to Michael Shulman, Jason Gross, Vladimir Voevodsky, Thomas Streicher, homotopyt...@googlegroups.com

Ah! And I think I have a counterexample, where those maps aren’t an equivalence.

Let (x0:X) be any pointed type, and (U, El) be a universe (with rules as I set out a couple of emails ago). Then X x U is again a universe, admitting all the same constructors as U: take

El(x,A) = El(A),

(x,A) +_U (y,B) = (x0, A +_U B),

and so on; that is, constructor operations on (X x U) are constantly x0 on the first component, and mirror those of U on the second component.

Now if U is univalent, and X has non-trivial pi0 (e.g. X=S1), then U -> (X x U) gives a univalent universe sitting inside a non-univalent one (again, with the rules as I set out earlier).

Slightly more generally, given any cumulative pair of universes U0 -> U1, we can consider U0 -> A x U1; this shows we can additionally have the smaller universe represented by an element of the larger one.

–p.

Mar 6, 2014, 12:00:38 PM3/6/14

to Peter LeFanu Lumsdaine, Jason Gross, Vladimir Voevodsky, Thomas Streicher, homotopyt...@googlegroups.com

On Thu, Mar 6, 2014 at 8:36 AM, Peter LeFanu Lumsdaine

<p.l.lu...@gmail.com> wrote:

> Now if U is univalent, and X has non-trivial pi0 (e.g. X=S1), then U -> (X x

> U) gives a univalent universe sitting inside a non-univalent one (again,

> with the rules as I set out earlier).

Very nice! More specifically, not only is X × U not univalent, it's
<p.l.lu...@gmail.com> wrote:

> Now if U is univalent, and X has non-trivial pi0 (e.g. X=S1), then U -> (X x

> U) gives a univalent universe sitting inside a non-univalent one (again,

> with the rules as I set out earlier).

not even "univalent on the image of U", as was the case for the

example in the groupoid model that I mentioned.

Mar 6, 2014, 12:06:58 PM3/6/14

to Thomas Streicher, Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

Part of the confusion may be that there are two different notions of "mono".

On the one hand there is the *internal* type-theoretic notion of

"homotopy" monomorphism, i.e. a map f : A -> B which induces an

equivalence on path spaces, i.e. whose (homotopy) fibers are mere

propositions. Certainly if U0 sits monically inside U1 in this sense,

then univalence of U1 implies univalence of U0.

On the other hand, in a set-theoretic model such as simplicial sets,

there is the notion of monomorphism in the 1-category (e.g. of

simplicial sets). This is essentially unrelated: a map of simplicial

sets can be a mono without being a homotopy mono, and vice versa. We

do probably want to ask that any inclusion of universes is mono in

this sense, at least if we want to think about Russell-style

universes, since otherwise two types that are not judgmentally equal

in one universe could become so in a higher universe. But nothing

prevents us from having a non-univalent U0 which sits inside a

univalent U1 by a mono of this sort.

On the one hand there is the *internal* type-theoretic notion of

"homotopy" monomorphism, i.e. a map f : A -> B which induces an

equivalence on path spaces, i.e. whose (homotopy) fibers are mere

propositions. Certainly if U0 sits monically inside U1 in this sense,

then univalence of U1 implies univalence of U0.

On the other hand, in a set-theoretic model such as simplicial sets,

there is the notion of monomorphism in the 1-category (e.g. of

simplicial sets). This is essentially unrelated: a map of simplicial

sets can be a mono without being a homotopy mono, and vice versa. We

do probably want to ask that any inclusion of universes is mono in

this sense, at least if we want to think about Russell-style

universes, since otherwise two types that are not judgmentally equal

in one universe could become so in a higher universe. But nothing

prevents us from having a non-univalent U0 which sits inside a

univalent U1 by a mono of this sort.

Mar 6, 2014, 12:12:31 PM3/6/14

to Thomas Streicher, Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

In the example Vladimir mentioned above, though — the discrete simplicial set of Kan complexes into the full universe of them Kan complexes — I think the map will be a mono, and hence a sub-universe in your sense. The *propositional* equality of U0 is finer than that of U1, but the *judgemental* equality is the same, so in the external, categorical sense, it’s a mono.

Precisely, what I have in mind is the following situation — or rather, either of two variants, one using well-ordered fibrations and the other using displayed fibrations. Please excuse the rather excruciating detail — but the construction has been sketched several times in this thread now and people have slightly disagreed over what they expect it to show, so it seems worth carefully spelling out details to dispel ambiguity. The two variants are on the one hand to give a version compatible with the paper, and on the other hand, to emphasise as usual that the well-orderings aren’t really involved with the substance of the model.

Version 1. Work in the simplicial model as set up in Vladimir, Chris’ and my paper.

α < β are inacessible cardinals;

(U1)_n = { Kan fibrations over Δ[n], with well-ordered fibers of size < β } / {order-preserving isomorphism}

(U0)_n = { well-ordered Kan complexes of size < α } / {order-preserving isomorphism}

Now pick arbitrary well-orderings on the sets U0, U1.

Now U0, U1 are well-ordered Kan complexes, carrying evident well-ordered fibrations p0, p1. There is a natural mono m : U0 -> U1, sending an equivalence class [X] in U0_n to the equivalence class [X x Δ[n] -> Δ[n] ] in U1_n; and m^p1 is order-preserving-isomorphic to p0, i.e. judgementally equal in the sense of the ambient contextual category. And U0 is well-ordered Kan complex of size <α, so occurs as a fiber of p1.

Version 2. As an alternative way of getting strictly associative pullbacks, instead work in the comprehension category whose base is the category of Kan complexes, and in which a type over X is a “displayed fibration”: that is, a functor Y : E(X)^op -> Sets [where E(X) is the category of elements of X], whose total space ΣY -> X is a fibration over X. Or, if you prefer to stick with contextual categories, work in the “contextual core” of this comprehension category: an object is a sequence (A0,A1,…) where A0 is a displayed fibration over 1 and A_{n+1} is a displayed fibration over the total space of A_n.

Now, take α < β inaccessible cardinals; and set

(U1)_n = { displayed fibrations over Δ[n], with fibers of size <β }

(U0)_n = { Kan complexes of size <α }

Again, these are both Kan complexes; they carry obvious displayed fibrations; there’s a mono m : U0 -> U1 (sending a Kan complex X to the constant functor with value X), commuting with these fibrations under pullback; and U0 can be exhibited as a pullback of U1.

So, in either version, we have a pair of universes U0 -> U1, satisfying the rules I set out a couple of emails ago, and also a sub-universe in Thomas’s sense, with U0 discrete and U1 univalent.

–p.

Mar 6, 2014, 1:56:16 PM3/6/14

to Peter LeFanu Lumsdaine, Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

Admittedly, I confused myself w.r.t. the two notions of mono. In my

mail I actually meant the external one, i.e. mono in simplicial sets.

Then clearly the universe U0 of small discrete simplical sets is

included into the universe U1 of small Kan complexes. That's nice, of

course.

But, on the other hand we also would like to have that type forming

operations in U0 coincide with type forming operations in U1. This

seems to hold for dependent sums and products but not for Id-types.

This preservation of type forming operations was not mentioned in my

definition because in extensional type theory type formers are given

by universal properties. E.g. (fibrewise) diagonals are the same in

the smaller and the bigger universe. But the factorisations of the

diagonals are different as in Valdimir's example.

Thomas

mail I actually meant the external one, i.e. mono in simplicial sets.

Then clearly the universe U0 of small discrete simplical sets is

included into the universe U1 of small Kan complexes. That's nice, of

course.

But, on the other hand we also would like to have that type forming

operations in U0 coincide with type forming operations in U1. This

seems to hold for dependent sums and products but not for Id-types.

This preservation of type forming operations was not mentioned in my

definition because in extensional type theory type formers are given

by universal properties. E.g. (fibrewise) diagonals are the same in

the smaller and the bigger universe. But the factorisations of the

diagonals are different as in Valdimir's example.

Thomas

Mar 6, 2014, 2:15:40 PM3/6/14

to Thomas Streicher, Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

On Thu, Mar 6, 2014 at 1:56 PM, Thomas Streicher <stre...@mathematik.tu-darmstadt.de> wrote:

But, on the other hand we also would like to have that type forming

operations in U0 coincide with type forming operations in U1. This

seems to hold for dependent sums and products but not for Id-types.

Considered in the usual way as a type-forming operation on each universe (i.e. analogous to how dependent sums and products are considered), Id-types will still coincide, if I'm not mistaken. That is, in the model I gave above, the operations

Id_0 : forall (A:U0), El_0 A -> El_0 A -> U0

Id_1 : forall (A:U1), El_1 A -> El_1 A -> U1

will satisfy, for A:U0 and x,y:El_0(A),

Id_1 (m A) x y = m ( Id_0 A x y ).

The Id-types that do not coincide are the Id-types *of* the universes themselves:

(Id U0) : U0 -> U0 -> (some universe in which U0 lives, or "Type")

(Id U1) : U1 -> U1 -> (some universe in which U1 lives, or "Type")

But these are distinct from the type-forming operations on the universes.

-p.

Mar 6, 2014, 3:54:40 PM3/6/14

to Peter LeFanu Lumsdaine, Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

I disagree. Take 2 = 1+1 which is in both universes.

Id_U0(2,2) contains one element whereas Id_U1(2,2) consist of isos of

2 and there is more than one.

Isn't it?

Thomas

Id_U0(2,2) contains one element whereas Id_U1(2,2) consist of isos of

2 and there is more than one.

Isn't it?

Thomas

Mar 6, 2014, 4:00:22 PM3/6/14

to Thomas Streicher, Peter LeFanu Lumsdaine, Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

On Thu, Mar 6, 2014 at 12:54 PM, Thomas Streicher

<stre...@mathematik.tu-darmstadt.de> wrote:

> I disagree. Take 2 = 1+1 which is in both universes.

> Id_U0(2,2) contains one element whereas Id_U1(2,2) consist of isos of

> 2 and there is more than one.

But Peter just said that that isn't what we're talking about:
<stre...@mathematik.tu-darmstadt.de> wrote:

> I disagree. Take 2 = 1+1 which is in both universes.

> Id_U0(2,2) contains one element whereas Id_U1(2,2) consist of isos of

> 2 and there is more than one.

Mar 6, 2014, 9:24:27 PM3/6/14

to Michael Shulman, Jason Gross, Vladimir Voevodsky, Thomas Streicher, homotopyt...@googlegroups.com

Indeed, yes. In fact, in the case where X is connected, X × U will if I’m not mistaken be “merely univalent”, in that for A,B:U, if El(A) <~> El(B) then there merely exists some equality between X and Y. So this gives a weak univalence-like principle which does not imply univalence itself (or at least, not for the same universe).

–p.

Mar 6, 2014, 10:51:05 PM3/6/14

to Peter LeFanu Lumsdaine, homotopyt...@googlegroups.com

Someone should record all of this somewhere, maybe at

http://ncatlab.org/homotopytypetheory/show/univalence+axiom .

On Thu, Mar 6, 2014 at 6:24 PM, Peter LeFanu Lumsdaine

http://ncatlab.org/homotopytypetheory/show/univalence+axiom .

On Thu, Mar 6, 2014 at 6:24 PM, Peter LeFanu Lumsdaine

<p.l.lu...@gmail.com> wrote:

> On Thu, Mar 6, 2014 at 12:00 PM, Michael Shulman <shu...@sandiego.edu>

> wrote:

>>

>> On Thu, Mar 6, 2014 at 8:36 AM, Peter LeFanu Lumsdaine

>> <p.l.lu...@gmail.com> wrote:

>> > Now if U is univalent, and X has non-trivial pi0 (e.g. X=S1), then U ->

>> > (X x

>> > U) gives a univalent universe sitting inside a non-univalent one (again,

>> > with the rules as I set out earlier).

>>

>> Very nice! More specifically, not only is X × U not univalent, it's

>> not even "univalent on the image of U", as was the case for the

>> example in the groupoid model that I mentioned.

>

>

> Indeed, yes. In fact, in the case where X is connected, X × U will if I’m

> not mistaken be “merely univalent”, in that for A,B:U, if El(A) <~> El(B)

> then there merely exists some equality between X and Y. So this gives a

> weak univalence-like principle which does not imply univalence itself (or at

> least, not for the same universe).

>

> –p.

>

> On Thu, Mar 6, 2014 at 12:00 PM, Michael Shulman <shu...@sandiego.edu>

> wrote:

>>

>> On Thu, Mar 6, 2014 at 8:36 AM, Peter LeFanu Lumsdaine

>> <p.l.lu...@gmail.com> wrote:

>> > Now if U is univalent, and X has non-trivial pi0 (e.g. X=S1), then U ->

>> > (X x

>> > U) gives a univalent universe sitting inside a non-univalent one (again,

>> > with the rules as I set out earlier).

>>

>> Very nice! More specifically, not only is X × U not univalent, it's

>> not even "univalent on the image of U", as was the case for the

>> example in the groupoid model that I mentioned.

>

>

> Indeed, yes. In fact, in the case where X is connected, X × U will if I’m

> not mistaken be “merely univalent”, in that for A,B:U, if El(A) <~> El(B)

> then there merely exists some equality between X and Y. So this gives a

> weak univalence-like principle which does not imply univalence itself (or at

> least, not for the same universe).

>

> –p.

>

> --

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

Mar 6, 2014, 11:47:58 PM3/6/14

to homotopyt...@googlegroups.com

Michael Shulman <shu...@sandiego.edu> writes:

> Someone should record all of this somewhere, maybe at

> http://ncatlab.org/homotopytypetheory/show/univalence+axiom .

a couple of the posts in this thread; if there are other posts that

people feel should be added, please let me know!

Alexis.

Mar 7, 2014, 3:46:10 AM3/7/14

to Michael Shulman, Peter LeFanu Lumsdaine, Vladimir Voevodsky, Jason Gross, homotopyt...@googlegroups.com

Yes, I noticed this morning.

Sorry, Thomas

Sorry, Thomas

Mar 7, 2014, 4:29:19 PM3/7/14

to Thomas Streicher, Peter LeFanu Lumsdaine, Jason Gross, homotopyt...@googlegroups.com

Another example - the universe of Kan complexes in the universe of all simplicial sets (the later is not univalent, in fact it is contractible).

The identity type construction is just a function from the universe of bi-pointed objects to the universe - it does not care about the structure of the universe itself.

V.

The identity type construction is just a function from the universe of bi-pointed objects to the universe - it does not care about the structure of the universe itself.

V.

Mar 7, 2014, 4:52:50 PM3/7/14

to Thomas Streicher, Peter LeFanu Lumsdaine, Jason Gross, homotopyt...@googlegroups.com

This is a type forming operation associated with U2 in which both U0 and U1 lie.

V.

V.

Mar 9, 2014, 3:36:33 AM3/9/14

to Jason Gross, homotopyt...@googlegroups.com

On 2014-03-04 17:58, Jason Gross wrote:

> Hi, I managed, after much hackery, to prove in Coq that functional

> extensionality is downward closed

> <https://github.com/HoTT/HoTT/issues/334#issuecomment-36599865> (that

> is, if functional extensionality is true in U_i, then it is true in

> U_j for all j <= i). (I suspect an Agda proof would be much less

> hacky.)

There is a short Agda proof in

http://www.cse.chalmers.se/~nad/listings/equality/Equality.html (see

"lower-extensionality").

--

/NAD

> Hi, I managed, after much hackery, to prove in Coq that functional

> extensionality is downward closed

> <https://github.com/HoTT/HoTT/issues/334#issuecomment-36599865> (that

> is, if functional extensionality is true in U_i, then it is true in

> U_j for all j <= i). (I suspect an Agda proof would be much less

> hacky.)

There is a short Agda proof in

http://www.cse.chalmers.se/~nad/listings/equality/Equality.html (see

"lower-extensionality").

--

/NAD

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu