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