Is Univalence downward-closed with regard to universes?

[Jason Gross]

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

[Michael Shulman]

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.

[Peter LeFanu Lumsdaine]

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.

[Vladimir Voevodsky]

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

[Thomas Streicher]

> 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

[Vladimir Voevodsky]

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.

[Jason Gross]

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

[Michael Shulman]

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.

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

It is equivalent to *something* in U_n, but there's no reason that the
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

[Thomas Streicher]

> 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

[Peter LeFanu Lumsdaine]

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.

 

[Peter LeFanu Lumsdaine]

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.

[Vladimir Voevodsky]

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.

[Vladimir Voevodsky]

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.

Good example.

V.

[Vladimir Voevodsky]

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.

V.

[Jason Gross]

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

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 

[Michael Shulman]

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.

[Thomas Streicher]

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

[Peter LeFanu Lumsdaine]

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.

[Michael Shulman]

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.

[Michael Shulman]

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.

[Peter LeFanu Lumsdaine]

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.

[Thomas Streicher]

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

[Peter LeFanu Lumsdaine]

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.

[Thomas Streicher]

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

[Michael Shulman]

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:

[Peter LeFanu Lumsdaine]

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.

[Michael Shulman]

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

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

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

[Alexis Hazell]

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

> Someone should record all of this somewhere, maybe at
> http://ncatlab.org/homotopytypetheory/show/univalence+axiom .

As a starting point, I've just done a straightforward copy-and-paste of
a couple of the posts in this thread; if there are other posts that
people feel should be added, please let me know!


Alexis.

[Thomas Streicher]

Yes, I noticed this morning.

Sorry, Thomas

[Vladimir Voevodsky]

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.

[Vladimir Voevodsky]

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

V.

[Nils Anders Danielsson]

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