Martin Escardo, 28 February 2018. --------------------------------------------------- A self-contained, brief and complete formulation of Voevodsky's univalence Axiom --------------------------------------------------- 1. Introduction ------------ In introductions to the subject for a general audience of mathematicians or logicians, the univalence axiom is typically explained by handwaving. This gives rise to several misconceptions, which cannot be properly addressed in the absence of a precise definition. Here we give a complete formulation of the univalence axiom from scratch, * first written informally but rigorously in mathematical English prose, and * then formally in Agda notation for Martin-Löf type theory. (Search for "univalenceFromScratch" to jump to the formal version.) The univalence axiom is not true or false in, say, ZFC or the internal language of an elementary topos. It cannot even be formulated. As the saying goes, it is not even wrong. This is because univalence is a property of Martin-Löf's *identity type* of a universe of types. Nothing like Martin-Löf's identity type occurs in ZFC or topos logic as a *native* concept like in MLTT. Of course, we can create *models* of the identity type and univalence in these theories, which will make univalence hold or fail. But in these notes we try to understand the primitive concept of identity type, and the univalence axiom, directly and independently of any such particular model, as in the original Martin-Löf type theory. In particular, we don't use the equality sign "=" to denote the identity type Id, or think of it as a path space. The underlying idea of these notes is that they should be as concise as possible (and not more). They are not meant to be an Encyclopedia of univalence. The source code for this file is available at https://github.com/martinescardo/TypeTopology/tree/master/source Issues and contributions are welcome. This document is also available at https://arxiv.org/abs/1803.02294 with the Agda code as an ancillary file. 2. Informal, rigorous construction of the univalence type ------------------------------------------------------ univalence is a type, and the univalence axiom says that this type has some inhabitant. It takes a number of steps to construct this type, in addition to subtle decisions (e.g. to work with equivalences rather than isomorphisms, as discussed below). We first need to briefly introduce Martin-Löf type theory (MLTT). We will not give a course in MLTT. Instead, we will mention which constructs of MLTT are needed to give a complete definition of the univalence type. This will be enough to illustrate the important fact that in order to understand univalence we first need to understand Martin-Löf type theory well. * Types and their elements ------------------------ Types are the analogues of sets in ZFC and of objects in topos theory. Types are constructed together with their elements, and not by collecting some previously existing elements. When a type is constructed, we get freshly new elements for it. We write x:X to declare that the element x has type X. This is not something that is true or false (like a membership relation x ∈ X in ZFC). For example, if ℕ is the type of natural numbers, we may write 17 : ℕ, (13,17) : ℕ × ℕ. However, the following statements are nonsensical and syntactically incorrect, rather than false: 17 : ℕ × ℕ (nonsense), (13,17) : ℕ (nonsense). This is no different from the situation in the internal language of a topos. * Products and sums of type families ---------------------------------- Given a family of types A(x) indexed by elements x of a type X, we can form its product and sum: Π(x:X), A(x), Σ(x:X), A(x), which we also write Π A and Σ A. An element of the type Π A is a function that maps elements x:X to elements of A(x). An element of the type Σ A is a pair (x,a) with x:X and a:A(x). (We adopt the convention that Π and Σ scope over the whole rest of the expression.) We also have the type X→Y of functions from X to Y, which is the particular case of Π with the constant family A(x):=Y. We also have the cartesian product X×Y, whose elements are pairs. This is the particular case of Σ, again with A(x):=Y. We also have the disjoint sum X+Y, the empty type 𝟘 and the one-element type 𝟙, which will not be needed here. * Quantifiers and logic --------------------- There is no underlying logic in MLTT. Propositions are types, and Π and Σ play the role of universal and existential quantifiers, via the so-called Curry-Howard interpretation of logic. As for the connectives, implication is given by the function-type construction →, conjunction by the binary cartesian product ×, and disjunction by the binary disjoint sum +. The elements of a type correspond to proofs, and instead of saying that a type A has a given element, it is common practice to say that A holds, when the type A is understood as a proposition. In this case, x:A is read as saying that x is a proof of A. But this is just a linguistic device, which is (deliberately) not reflected in the formalism. We remark that in univalent mathematics the terminology *proposition* is reserved for subsingleton types (types whose elements are all identified). The propositions that arise in the construction of the univalence type are all subsingletons. * The identity type ----------------- Given a type X and elements x,y:X, we have the identity type Id_X(x,y), with the subscript X often elided. The idea is that Id(x,y) collects the ways in which x and y are identified. We have a function refl : Π(x:X), Id(x,x), which identifies any element with itself. Without univalence, refl is the only given way to construct elements of the identity type. In addition to refl, for any given type family A(x,y,p) indexed by elements x,y:X and p:Id(x,y) and any given function f : Π(x:X), A(x,x,refl(x)), we have a function J(A,f) : Π(x,y:X), Π(p:Id(x,y)), A(x,y,p) with J(A,f)(x,x,refl(x)) stipulated to be f(x). We will see examples of uses of J in the steps leading to the construction of the univalence type. Then, in summary, the identity type is given by the data Id,refl,J. With this, the exact nature of the type Id(x,y) is fairly under-specified. It is consistent that it is always a subsingleton in the sense that K(X) holds, where K(X) := Π(x,y:X), Π(p,q:Id(x,y)), Id(p,q). The second identity type Id(p,q) is that of the type Id(x,y). This is possible because any type has an identity type, including the identity type itself, and the identity type of the identity type, and so on, which is the basis for univalent mathematics (but this is not discussed here, as it is not needed in order to construct the univalence type). The K axiom says that K(X) holds for every type X. In univalent mathematics, a type X that satisfies K(X) is called a set, and with this terminology, the K axiom says that all types are sets. On the other hand, the univalence axiom provides a means of constructing elements other than refl(x), at least for some types, and hence the univalence axiom implies that some types are not sets. (Then they will instead be 1-groupoids, or 2-groupoids, ⋯, or even ∞-groupoids, with such notions defined within MLTT rather than via models, but we will not address this important aspect of univalent mathematics here). * Universes --------- Our final ingredient is a "large" type of "small" types, called a universe. It is common to assume a tower of universes 𝓤₀, 𝓤₁, 𝓤₂, ... of "larger and larger" types, with 𝓤₀ : 𝓤₁, 𝓤₁ : 𝓤₂, 𝓤₂ : 𝓤₃, ⋮ When we have universes, a type family A indexed by a type X: 𝓤 may be considered to be a function A:X→𝓥 for some universe 𝓥. Universes are also used to construct types of mathematical structures, such as the type of groups, whose definition starts like this: Grp := Σ(G: 𝓤), is-set(G) × Σ(e:G), Σ(_∙_:G×G→G), (Π(x:G), Id(e∙x,x)) × ⋯ Here is-set(G):=Π(x,y:G),Π(p,q:Id(x,y)),Id(p,q), as above. With univalence, Grp itself will not be a set, but a 1-groupoid instead, namely a type whose identity types are all sets. Moreover, if 𝓤 satisfies the univalence axiom, then for A,B:Grp, the identity type Id(A,B) can be shown to be in bijection with the group isomorphisms of A and B. * univalence ---------- univalence is a property of the identity type Id_𝓤 of a universe 𝓤. It takes a number of steps to define the univalence type. We say that a type X is a singleton if we have an element c:X with Id(c,x) for all x:X. In Curry-Howard logic, this is is-singleton(X) := Σ(c:X), Π(x:X), Id(c,x). (Alternative terminology not used here: X is contractible.) For a function f:X→Y and an element y:Y, its fiber is the type of points x:X that are mapped to (a point identified with) y: f⁻¹(y) := Σ(x:X),Id(f(x),y). The function f is called an equivalence if its fibers are all singletons: is-equiv(f) := Π(y:Y), is-singleton(f⁻¹(y)). The type of equivalences from X: 𝓤 to Y:𝓤 is Eq(X,Y) := Σ(f:X→Y), is-equiv(f). Given x:X, we have the singleton type consisting of the elements y:X identified with x: singletonType(x) := Σ(y:X), Id(y,x). We also have the element η(x) of this type: η(x) := (x, refl(x)). We now need to *prove* that singleton types are singletons: Π(x:X), is-singleton(singletonType(x)). In order to do that, we use J with the type family A(y,x,p) := Id(η(x),(y,p)), and the function f : Π(x:X), A(x,x,refl(x)) defined by f(x) := refl(η(x)). With this we get a function φ : Π(y,x:X), Π(p:Id(y,x)), Id(η(x),(y,p)) φ := J(A,f). (Notice the reversal of y and x.) With this, we can in turn define a function g : Π(x:X), Π(σ:singletonType(x)), Id(η(x),σ) g(x,(y,p)) := φ(y,x,p). Finally, using g we get our desired result, that singleton types are singletons: h : Π(x:X), Σ(c:singletonType(x)), Π(σ:singletonType(x)), Id(c,σ) h(x) := (η(x),g(x)). Now, for any type X, its identity function id_X, defined by id(x) := x, is an equivalence. This is because the fiber id⁻¹(x) is simply the singleton type defined above, which we proved to be a singleton. We need to name this function, because it is needed in the formulation of the univalence of 𝓤: idIsEquiv : Π(X: 𝓤), is-equiv(id_X). (The identity function id_X should not be confused with the identity type Id_X.) Now we use J a second time to define a function IdToEq : Π(X,Y: 𝓤), Id(X,Y) → Eq(X,Y). For X,Y: 𝓤 and p:Id(X,Y), we set A(X,Y,p) := Eq(X,Y) and f(X) := (id_X , idIsEquiv(X)), and IdToEq := J(A,f). Finally, we say that the universe 𝓤 is univalent if the map IdToEq(X,Y) is itself an equivalence: is-univalent(𝓤) := Π(X,Y: 𝓤), is-equiv(IdToEq(X,Y)). * The univalence axiom -------------------- The type is-univalent(𝓤) may or may not have an inhabitant. The univalence axiom says that it does. Without the univalence axiom (or some other axiom such as the assertion that K(𝓤) has an inhabitant), the inhabitedness of the type is-univalent(𝓤) is undecided. * Notes ----- 1. The minimal Martin-Löf type theory needed to formulate univalence has Π, Σ, Id, 𝓤, 𝓤'. Two universes 𝓤: 𝓤' suffice, where univalence talks about 𝓤. 2. It can be shown, by a very complicated and interesting argument, that Π(u,v: is-univalent(𝓤)), Id(u,v). This says that univalence is a subsingleton type (any two of its elements are identified). In the first step we use u (or v) to get function extensionality (any two pointwise identified functions are identified), which is *not* provable in MLTT, but is provable from the assumption that 𝓤 is univalent. Then, using this, one shows that being an equivalence is a subsingleton type. Finally, again using function extensionality, we get that a product of subsingletons is a subsingleton. But then Id(u,v) holds, which is what we wanted to show. But this of course omits the proof that univalence implies function extensionality (originally due to Voevodsky), which is fairly elaborate. 3. For a function f:X→Y, consider the type Iso(f) := Σ(g:Y→X), (Π(x:X), Id(g(f(x)),x)) × (Π(y:Y), Id(f(g(y)),y)). We have functions r:Iso(f)→is-equiv(f) and s:is-equiv(f)→Iso(f). However, the type is-equiv(f) is always a subsingleton, assuming function extensionality, whereas the type Iso(f) need not be. What we do have is that the function r is a retraction with section s. Moreover, the univalence type formulated as above, but using Iso(f) rather than is-equiv(f) is provably empty, e.g. for MLTT with Π, Σ, Id, the empty and two-point types, and three universes, as shown by Shulman. With only one universe, the formulation with Iso(f) is consistent, as shown by Hofmann and Streicher's groupoid model, but in this case all elements of the universe are sets and Iso(f) is a subsingleton, and hence equivalent to is-equiv(f). So, to have a consistent axiom in general, it is crucial to use the type is-equiv(f). It was Voevodsky's insight that not only a subsingleton version of Iso(f) is needed, but also how to construct it. The construction of is-equiv(f) is very simple and elegant, and motivated by homotopical models of the theory, where it corresponds to the concept with the same name. But the univalence axiom can be understood without reference to homotopy theory. 3. Voevodsky gave a model of univalence for MLTT with Π,Σ, empty type, one-point type, two-point type, natural numbers, and an infinite tower of universes in simplicial sets, thus establishing the consistency of the univalence axiom. The consistency of the univalence axiom shows that, before we postulate it, MLTT is "proto-univalent" in the sense that it cannot distinguish concrete isomorphic types such as X:=ℕ and Y:=ℕ×ℕ by a property P: 𝓤→𝓤 such that P(X) holds but P(Y) doesn't. This is because, being isomorphic, X and Y are equivalent. But then univalence implies Id(X,Y), which in turn implies P(X) ⇔ P(Y) using J. Because univalence is consistent, it follows that for any given concrete P: 𝓤→𝓤, it is impossible to prove that P(X) holds but P(Y) doesn't. So MLTT is invariant under isomorphism in this doubly negative, meta-mathematical sense. With univalence, it becomes invariant under isomorphism in a positive, mathematical sense. 4. Thus, we see that the formulation of univalence is far from direct, and has much more to it than the (in our opinion, misleading) slogan "isomorphic types are equal". What the consistency of the univalence axiom says is that one possible understanding of the identity type Id(X,Y) for X,Y: 𝓤 is as precisely the type Eq(X,Y) of equivalences, in the sense of being in one-to-one correspondence with it. Without univalence, the nature of the identity type of the universe in MLTT is fairly under-specified. It is a remarkable property of MLTT that it is consistent with this understanding of the identity type of the universe, discovered by Vladimir Voevodsky (and foreseen by Martin Hofmann and Thomas Streicher (1996) in a particular case). This paper only explains what the *univalence axiom* is. A brief and reasonably complete introduction to *univalent mathematics* is given by Grayson. References ---------- Daniel R. Grayson. An introduction to univalent foundations for mathematicians, 2017. https://arxiv.org/abs/1711.01477 Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 83--111. Oxford Univ. Press, New York, 1998. http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=8452D335B33D098D993C3D5E870CAE03?doi=10.1.1.37.606&rep=rep1&type=pdf Chris Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky), 2012. https://arxiv.org/abs/1211.2851 Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. The simplicial model of univalent foundations, 2012. https://arxiv.org/abs/1203.2553 Per Martin-L\"of. Constructive mathematics and computer programming. In Logic, methodology and philosophy of science, VI (Hannover, 1979), volume 104 of Stud. Logic Found. Math., pages 153--175. North-Holland, Amsterdam, 1982. http://archive-pml.github.io/martin-lof/pdfs/Constructive-mathematics-and-computer-programming-1982.pdf Michael Shulman. Solution to Exercise 4.6 (in pure MLTT), March 2018. https://github.com/HoTT/HoTT/commit/531bc5865089cb8b32a0c49d0f9bf220f811a292 The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013. https://homotopytypetheory.org/book/ Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Math. Structures Comput. Sci., 25(5):1278--1294, 2015. https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/Univalent%20library%20paper%20current.pdf 3. Formal construction of the univalence type in Agda -------------------------------------------------- We now give a symbolic rendering of the above construction of the univalence type, in Agda notation. (Agda documentation is at http://wiki.portal.chalmers.se/agda/pmwiki.php). The fragment of Agda used here amounts to the subset of MLTT with Π,Σ,Id and a tower of universes as discussed above. By default, Agda has the K axiom, which, as discussed above, contradicts univalence, and hence we disable it. Inductive definitions in Agda are given with the keyword "data". Unlike Coq, Agda doesn't derive the induction principles, and one has to do this manually, as we do in the definition of J. Finally, notice that in Agda one constructs things by first specifying their types and then giving a definition with the equality sign. The letters 𝓤, 𝓥, 𝓦 range over universes, the successor of a universe 𝓤 is written 𝓤 ⁺, and the first universe after the universes 𝓤 and 𝓥 is written 𝓤 ⊔ 𝓥, to avoid subscripts. \begin{code} {-# OPTIONS --without-K --exact-split --safe #-} module UnivalenceFromScratch where open import Agda.Primitive using (_⊔_) renaming (lzero to 𝓤₀ ; lsuc to _⁺ ; Level to Universe) _̇ : (𝓤 : Universe) → _ 𝓤 ̇ = Set 𝓤 -- This should be the only use of the Agda keyword 'Set' in this development. infix 0 _̇ data Σ {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } (Y : X → 𝓥 ̇ ) : 𝓤 ⊔ 𝓥 ̇ where _,_ : (x : X) (y : Y x) → Σ Y data Id {𝓤 : Universe} {X : 𝓤 ̇ } : X → X → 𝓤 ̇ where refl : (x : X) → Id x x J : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } → (A : (x y : X) → Id x y → 𝓥 ̇ ) → ((x : X) → A x x (refl x)) → (x y : X) (p : Id x y) → A x y p J A f x .x (refl .x) = f x is-singleton : {𝓤 : Universe} → 𝓤 ̇ → 𝓤 ̇ is-singleton X = Σ \(c : X) → (x : X) → Id c x fiber : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → Y → 𝓤 ⊔ 𝓥 ̇ fiber f y = Σ \x → Id (f x) y is-equiv : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇ is-equiv f = (y : _) → is-singleton(fiber f y) Eq : {𝓤 𝓥 : Universe} → 𝓤 ̇ → 𝓥 ̇ → 𝓤 ⊔ 𝓥 ̇ Eq X Y = Σ \(f : X → Y) → is-equiv f singletonType : {𝓤 : Universe} {X : 𝓤 ̇ } → X → 𝓤 ̇ singletonType x = Σ \y → Id y x η : {𝓤 : Universe} {X : 𝓤 ̇ } (x : X) → singletonType x η x = (x , refl x) singletonTypesAreSingletons : {𝓤 : Universe} {X : 𝓤 ̇ } (x : X) → is-singleton(singletonType x) singletonTypesAreSingletons {𝓤} {X} = h where A : (y x : X) → Id y x → 𝓤 ̇ A y x p = Id (η x) (y , p) f : (x : X) → A x x (refl x) f x = refl (η x) φ : (y x : X) (p : Id y x) → Id (η x) (y , p) φ = J A f g : (x : X) (σ : singletonType x) → Id (η x) σ g x (y , p) = φ y x p h : (x : X) → Σ \(c : singletonType x) → (σ : singletonType x) → Id c σ h x = (η x , g x) id : {𝓤 : Universe} (X : 𝓤 ̇ ) → X → X id X x = x idIsEquiv : {𝓤 : Universe} (X : 𝓤 ̇ ) → is-equiv(id X) idIsEquiv X = g where g : (x : X) → is-singleton (fiber (id X) x) g = singletonTypesAreSingletons IdToEq : {𝓤 : Universe} (X Y : 𝓤 ̇ ) → Id X Y → Eq X Y IdToEq {𝓤} = J A f where A : (X Y : 𝓤 ̇ ) → Id X Y → 𝓤 ̇ A X Y p = Eq X Y f : (X : 𝓤 ̇ ) → A X X (refl X) f X = (id X , idIsEquiv X) is-univalent : (𝓤 : Universe) → 𝓤 ⁺ ̇ is-univalent 𝓤 = (X Y : 𝓤 ̇ ) → is-equiv(IdToEq X Y) \end{code} Thus, we see that even in its concise symbolic form, the formulation of univalence is far from direct. Using projections pr₁ and pr₂ rather than pattern matching on Σ types (by defining Σ as a record type), Agda calculates the following normal form for the term is-univalent: λ 𝓤 → (X Y : Set 𝓤) (y : Σ (λ f → (y₁ : Y) → Σ (λ c → (x : Σ (λ x₁ → Id (f x₁) y₁)) → Id c x))) → Σ (λ c → (x : Σ (λ x₁ → Id (J (λ X₁ Y₁ p → Σ (λ f → (y₁ : Y₁) → Σ (λ c₁ → (x₂ : Σ (λ x₃ → Id (f x₃) y₁)) → Id c₁ x₂))) (λ X₁ → (λ x₂ → x₂) , (λ x₂ → (x₂ , refl x₂) , (λ yp → J (λ y₁ x₃ p → Id (x₃ , refl x₃) (y₁ , p)) (λ x₃ → refl (x₃ , refl x₃)) (pr₁ yp) x₂ (pr₂ yp)))) X Y x₁) y)) → Id c x) This is with lots of subterms elided. With all of them explicitly given, the normal form of is-univalent is λ 𝓤 → (X Y : 𝓤 ̇ ) (y : Σ {𝓤} {𝓤} {X → Y} (λ f → (y₁ : Y) → Σ {𝓤} {𝓤} {Σ {𝓤} {𝓤} {X} (λ x → Id {𝓤} {Y} (f x) y₁)} (λ c → (x : Σ {𝓤} {𝓤} {X} (λ x₁ → Id {𝓤} {Y} (f x₁) y₁)) → Id {𝓤} {Σ {𝓤} {𝓤} {X} (λ x₁ → Id {𝓤} {Y} (f x₁) y₁)} c x))) → Σ {𝓤 ⁺} {𝓤 ⁺} {Σ {𝓤 ⁺} {𝓤} {Id {𝓤 ′} {𝓤 ̇ } X Y} (λ x → Id {𝓤} {Σ {𝓤} {𝓤} {X → Y} (λ f → (y₁ : Y) → Σ {𝓤} {𝓤} {Σ {𝓤} {𝓤} {X} (λ x₁ → Id {𝓤} {Y} (f x₁) y₁)} (λ c → (x₁ : Σ {𝓤} {𝓤} {X} (λ x₂ → Id {𝓤} {Y} (f x₂) y₁)) → Id {𝓤} {Σ {𝓤} {𝓤} {X} (λ x₂ → Id {𝓤} {Y} (f x₂) y₁)} c x₁))} (J {𝓤 ⁺} {𝓤} {𝓤 ̇ } (λ X₁ Y₁ p → Σ {𝓤} {𝓤} {X₁ → Y₁} (λ f → (y₁ : Y₁) → Σ {𝓤} {𝓤} {Σ {𝓤} {𝓤} {X₁} (λ x₁ → Id {𝓤} {Y₁} (f x₁) y₁)} (λ c → (x₁ : Σ {𝓤} {𝓤} {X₁} (λ x₂ → Id {𝓤} {Y₁} (f x₂) y₁)) → Id {𝓤} {Σ {𝓤} {𝓤} {X₁} (λ x₂ → Id {𝓤} {Y₁} (f x₂) y₁)} c x₁))) (λ X₁ → (λ x₁ → x₁) , (λ x₁ → (x₁ , refl x₁) , (λ yp → J {𝓤} {𝓤} {X₁} (λ y₁ x₂ p → Id {𝓤} {Σ {𝓤} {𝓤} {X₁} (λ y₂ → Id {𝓤} {X₁} y₂ x₂)} (x₂ , refl x₂) (y₁ , p)) (λ x₂ → refl (x₂ , refl x₂)) (pr₁ yp) x₁ (pr₂ yp)))) X Y x) y)} (λ c → (x : Σ {𝓤 ⁺} {𝓤} {Id {𝓤 ⁺} {𝓤 ̇ } X Y} (λ x₁ → Id {𝓤} {Σ {𝓤} {𝓤} {X → Y} (λ f → (y₁ : Y) → Σ {𝓤} {𝓤} {Σ {𝓤} {𝓤} {X} (λ x₂ → Id {𝓤} {Y} (f x₂) y₁)} (λ c₁ → (x₂ : Σ {𝓤} {𝓤} {X} (λ x₃ → Id {𝓤} {Y} (f x₃) y₁)) → Id {𝓤} {Σ {𝓤} {𝓤} {X} (λ x₃ → Id {𝓤} {Y} (f x₃) y₁)} c₁ x₂))} (J {𝓤 ⁺} {𝓤} {𝓤 ̇ } (λ X₁ Y₁ p → Σ {𝓤} {𝓤} {X₁ → Y₁} (λ f → (y₁ : Y₁) → Σ {𝓤} {𝓤} {Σ {𝓤} {𝓤} {X₁} (λ x₂ → Id {𝓤} {Y₁} (f x₂) y₁)} (λ c₁ → (x₂ : Σ {𝓤} {𝓤} {X₁} (λ x₃ → Id {𝓤} {Y₁} (f x₃) y₁)) → Id {𝓤} {Σ {𝓤} {𝓤} {X₁} (λ x₃ → Id {𝓤} {Y₁} (f x₃) y₁)} c₁ x₂))) (λ X₁ → (λ x₂ → x₂) , (λ x₂ → (x₂ , refl x₂) , (λ yp → J {𝓤} {𝓤} {X₁} (λ y₁ x₃ p → Id {𝓤} {Σ {𝓤} {𝓤} {X₁} (λ y₂ → Id {𝓤} {X₁} y₂ x₃)} (x₃ , refl x₃) (y₁ , p)) (λ x₃ → refl (x₃ , refl x₃)) (pr₁ yp) x₂ (pr₂ yp)))) X Y x₁) y)) → Id {𝓤 ⁺} {Σ {𝓤 ⁺} {𝓤} {Id {𝓤 ⁺} {𝓤 ̇ } X Y} (λ x₁ → Id {𝓤} {Σ {𝓤} {𝓤} {X → Y} (λ f → (y₁ : Y) → Σ {𝓤} {𝓤} {Σ {𝓤} {𝓤} {X} (λ x₂ → Id {𝓤} {Y} (f x₂) y₁)} (λ c₁ → (x₂ : Σ {𝓤} {𝓤} {X} (λ x₃ → Id {𝓤} {Y} (f x₃) y₁)) → Id {𝓤} {Σ {𝓤} {𝓤} {X} (λ x₃ → Id {𝓤} {Y} (f x₃) y₁)} c₁ x₂))} (J {𝓤 ⁺} {𝓤} {𝓤 ̇ } (λ X₁ Y₁ p → Σ {𝓤} {𝓤} {X₁ → Y₁} (λ f → (y₁ : Y₁) → Σ {𝓤} {𝓤} {Σ {𝓤} {𝓤} {X₁} (λ x₂ → Id {𝓤} {Y₁} (f x₂) y₁)} (λ c₁ → (x₂ : Σ {𝓤} {𝓤} {X₁} (λ x₃ → Id {𝓤} {Y₁} (f x₃) y₁)) → Id {𝓤} {Σ {𝓤} {𝓤} {X₁} (λ x₃ → Id {𝓤} {Y₁} (f x₃) y₁)} c₁ x₂))) (λ X₁ → (λ x₂ → x₂) , (λ x₂ → (x₂ , refl x₂) , (λ yp → J {𝓤} {𝓤} {X₁} (λ y₁ x₃ p → Id {𝓤} {Σ {𝓤} {𝓤} {X₁} (λ y₂ → Id {𝓤} {X₁} y₂ x₃)} (x₃ , refl x₃) (y₁ , p)) (λ x₃ → refl (x₃ , refl x₃)) (pr₁ yp) x₂ (pr₂ yp)))) X Y x₁) y)} c x)