The univalence axiom for a universe states that for all , the map
defined by path induction, is an equivalence. So we have
In a post to the Homotopy Type Theory Google Group, Peter LeFanu Lumsdaine wrote:
Let be any pointed type, and be a universe (with rules as I set out a couple of emails ago). Then is again a universe, admitting all the same constructors as : take
,
,and so on; that is, constructor operations on are constantly on the first component, and mirror those of on the second component.
Now if is univalent, and has non-trivial (e.g. ), then ) 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 , we can consider ; this shows we can additionally have the smaller universe represented by an element of the larger one.
[N]ot only is not univalent, itβs not even βunivalent on the image of β, as was the case for the example in the groupoid model that I mentioned.
Revision on October 11, 2018 at 07:43:10 by Ali Caglayan. See the history of this page for a list of all contributions to it.