SPLST'15 Two Set-based Implementations of Quotients in Type Theory Niccolò Veltri Institute of Cybernetics, Tallinn University of Technology Akadeemia tee 21, 12618 Tallinn, Estonia, niccolo@cs.ioc.ee Abstract. We present and compare two different implementations of quotient types in Intensional Type Theory. We first introduce quotients as particular inductive-like types following Martin Hofmann’s extension of Calculus of Constructions with quotient types [6]. Then we give an impredicative encoding of quotients. This implementation is reminiscent of Church numerals and more generally of encodings of inductive types in Calculus of Constructions. 1 Introduction In mathematics, given a set X and an equivalence relation R on X, the quotient set X/R is the set of equivalence classes of X with respect to R, i.e. X/R = {[x] | x ∈ X}, where [x] = {y ∈ X | x R y}. An important example is the set of integer numbers, constructed as the quotient set (N × N)/SameDiff, where SameDiff (n1 , m1 ) (n2 , m2 ) if and only if n1 + m2 = n2 + m1 . Another example is the set of real numbers, constructed as the quotient set CauchyQ /Diff →0 , where CauchyQ is the set of Cauchy sequences of rational numbers and Diff →0 {xn } {yn } if and only if the sequence {xn − yn } converges to 0. A fundamental usage of quotients in programming is the construction of finite multisubsets of a given type X as “lists modulo permutations”, and of finite subsets of X as “lists modulo permutations and multiplicity”. In Martin-Löf type theory (MLTT) [8] and in Calculus of Inductive Con- structions (CIC) [1] quotients are typically represented by setoids. A setoid is a pair (A, R) where A is a set and R is an equivalence relation on A. A map between setoids (A, R) and (B, S) is a map f : A → B compatible with the rela- tions, i.e. if a R b then (f a) S (f b). Every set A can be represented as the setoid (A, ≡), where ≡ is propositional equality on A. Given an equivalence relation R on A the quotient A/R is represented as the setoid (A, R). There is a canonical setoid map abs : (A, ≡) → (A, R), abs = id, that is clearly compatible, and every setoid map f : (A, ≡) → (B, S) such that (f a) S (f b) whenever a R b extends to a setoid map lift f : (A, R) → (B, S). The implementation of quotients as setoids forces us to lift every type former to setoids. For example the type formers of products, function spaces, lists and trees must become setoid transformers. Moreover in several applications it is preferable to work with sets instead of setoids. 194 SPLST'15 In this paper we present two different frameworks for reasoning about set- based quotients, i.e. quotients as types. We first introduce in Section 2 quotients as particular inductive-like types. The presentation is inspired by quotient types in Martin Hofmann’s PhD thesis [6], and works fine both in MLTT and in CIC. Our presentation is settled in MLTT. In Section 3 we show an alternative encoding of quotients in a small extension of Calculus of Constructions (CC). The two implementations are pretty different in flavor. We highlight their main features and show some examples. In Section 4 we present integer numbers as the quotient of N × N mentioned in the introduction, and in Section 5 we present finite multisubsets of a given type X as the quotient of List X also mentioned above. The presentations work fine both in MLTT and in our extension of CC. Note that integer numbers are already definable in type theory without the need of quotient types. In MLTT, for example, integers are implemented as two distinct copies of natural numbers N + N, interpreted as the negative and non- negative numbers. Note that in order to avoid the presence of two zeros, the elements of the first copy of N have to be considered as “shifted by one”, i.e. inl n has to be read as −(n + 1). Another possibility is to introduce integers as the type > + N + N, specifying zero explicitly and “shifting by one” both copies. Using such implementations, defining operations on integers and proving that such operations satisfy the laws of arithmetic (e.g. Z is a integral domain) become tedious due to the number of cases involved in the definitions. In Section 4 we want to show that our implementation is more elegant and less tedious to work with than the other two presented above. We have fully formalized the results of this paper in the dependently typed programming language Agda [9]. The formalization is available at http://cs. ioc.ee/~niccolo/quotients/. In order to be consistent with the formalization, in this paper we use the notation of MLTT. 2 Inductive-Like Quotients In this section, we introduce quotient types as particular inductive-like types introduced by M. Hofmann [6]. First we briefly describe the type theory under consideration. 2.1 The Type Theory under Consideration We consider Martin-Löf type theory (MLTT) with inductive types and a cumu- lative hierarchy of universes Uk . We allow dependent functions to have implicit arguments and indicated implicit argument positions with curly brackets (as in Agda). We write ≡ for propositional equality (identity types) and = for judgmen- tal (definitional) equality. Reflexivity, symmetry, transitivity and substitutivity of ≡ are named refl, sym, trans and subst, respectively. We assume uniqueness of identity proofs for all types, i.e., an inhabitant for Y Y Y UIP = p1 ≡ p2 . {X:U } {x1 ,x2 :X} p1 ,p2 :x1 ≡x2 195 SPLST'15 A type X is said to be a proposition, if it has at most one inhabitant, i.e., if the type Y isProp X = x1 ≡ x2 x1 ,x2 :X is inhabited. Uniqueness of identity proofs is needed only to prove that the propositional truncation of a type is a proposition (Subsection 2.4), which in turn is needed in the proof of Proposition 1. 2.2 The Implementation We now describe quotient types à la Hofmann. We call them “inductive-like quotients” because they are given a dependent elimination principle (sometimes also called induction principle). Let X be a type and R an equivalence relation on X. For any type Y and function f : X → Y , we say that f is R-compatible (or simply compatible, when the intended equivalence relation is clear from the context), if the type Y compat f = x1 Rx2 → f x1 ≡ f x2 {x1 ,x2 :X} is inhabited. The quotient of X by the relation R is described by the following data: (i) a carrier type X/R; (ii) a constructor abs : X → X/R together with a proof sound : compat abs; (iii) a dependent eliminator: Q for every family of types Y : X/R → Uk and functionQf : x:X Y (abs x) with p : dcompat f , there exists a function lift f p : q:X/R Y q; (iv) a computation Q rule: for every family of types Y : X/R → Uk , function f : x:X Y (abs x) with p : dcompat f and x : X we have liftβ f p x : lift f p (abs x) ≡ f x Q The predicate dcompat represents compatibility for dependent functions f : x:X Y (abs x): Y Y dcompat f = subst Y (sound r) (f x1 ) ≡ f x2 . {x1 ,x2 :X} r:x1 Rx2 We postulate the existence of data (i)–(iv) for all types X and equivalence re- lations R on X. Notice that the predicate dcompat depends on the availability of sound. Also notice that, in (iii), we allow elimination on every universe Uk . In our development, we actually eliminate only on U and once on U1 (Proposition 1). We now take a look at some derived results and examples. 196 SPLST'15 2.3 Classical Quotients Classically every equivalence class in a quotient X/R has a representative ele- ment in the original set, i.e. a map rep : X/R → X that satisfies the following conditions: Y complete : (rep (abs x)) R x x:X Y stable : abs (rep q) ≡ q q:X/R If we postulate the existence of such quotients for all sets and equivalence relations it is possible to derive the law of excluded middle [2]. In general in constructive mathematics, for a given equivalence class there is no canonical choice of a representative. This idea is reflected in the imple- mentation of quotients we presented in the previous section. Every map of type X/R → X is of the form lift f p for a certain R-compatible map f : X → X. But for a general type X and equivalence relation R strictly weaker then equality, there is no such canonical f . 2.4 Propositional Truncation The propositional truncation (or squash) kXk of a type X is the quotient of X by the total relation λ x1 x2 . >. Intuitively kXk is the unit type > if X is inhabited and it is empty otherwise. In other words, kXk is the proposition associated with the type X. Indeed: isPropk : isProp kXk isPropk x1 x2 = lift (λ y1 . lift (λ y2 . sound ?) p1 x2 ) p2 x1 where ? : > is the constructor of the unit type, while p1 and p2 are simple compatibility proofs. Note that in these compatibility proofs we need to show that two equality proofs are equal, and we do it by using the uniqueness of identity proofs. Note that the propositional truncation operation defines a monad: the unit is | | and multiplication µk : kkXkk → kXk is defined as µk = lift id p, where p is the easy proof of compatibility that follows from the fact that kXk is a proposition. In general, for a given family of equivalence relations RX : X → X → U, indexed by X : U, the functor F X = X/RX is not a monad, since there is no way of constructing a multiplication µ : (X/RX )/RX/RX → X/RX . 2.5 Function Extensionality Let X and Y be types. Extensional equality of functions is an equivalence relation on X → Y : FunExt≡ : (X → Y ) → (X → Y ) → U Y FunExt≡ f g = f x ≡ gx x:X 197 SPLST'15 For the quotient (X → Y )/FunExt≡ there exists a map that associates a representative function to each equivalence class. rep : (X → Y )/FunExt≡ → (X → Y ) rep q x = lift (λf. f x) (λp. p x) q Using the computation rule liftβ of quotients we obtain rep (abs f ) x ≡ f x, for all f : X → Y and x : X. The computation rule holds only up to proposi- tional equality. If equality in liftβ were definitional, one could prove, using rep, the principle of function extensionality. Indeed, consider f, g : X → Y with FunExt≡ f g. Then the following sequence of equations holds: f = λx. f x = λx. rep (abs f ) x = rep (abs f ) ≡ rep (abs g) = λx. rep (abs g) x = λx. g x = g 2.6 Effectiveness Q A quotient X/R is said to be effective, if the type x1 ,x2 :X abs x1 ≡ abs x2 → x1 R x2 is inhabited. In general, effectiveness does not hold for all quotients. Moreover, postulating effectiveness for all quotients implies the law of excluded middle [7]. Clearly classical quotients, discussed in Subsection 2.3, are effective. Indeed, if for x1 , x2 : X we have abs x1 ≡ abs x2 then, using complete we are done, since rep (abs x1 ) R x1 , rep (abs x2 ) R x2 and rep (abs x1 ) ≡ rep (abs x2 ). For a general type X and a general equivalence relation R on X, we can only prove that, under the assumption of proposition extensionality, the quotient X/R satisfies a weaker property. The principle of proposition extensionality states that logically equivalent propositions are equal:1 Y PropExt = isProp X → isProp Y → X ↔ Y → X ≡ Y {X,Y :U } where X ↔ Y = (X Q → Y ) × (Y → X). We say that a quotient X/R is weakly effective, if the type x1 ,x2 :X abs x1 ≡ abs x2 → kx1 R x2 k is inhabited. If we extend our type theory with PropExt, we can prove that all quotients are weakly effective. Proposition 1. Under the hypothesis of proposition extensionality, all quotients are weakly effective. Proof. In fact, let X be a type, R an equivalence relation on X and x : X. Consider the function kx R k : X → U, kx R k = λ x0 . kx R x0 k. We show that kxR k is R-compatible. Let x1 , x2 : X with x1 Rx2 . We have xRx1 ↔ xRx2 and therefore kx R x1 k ↔ kx R x2 k. Since propositional truncations are propositions 1 Note that proposition extensionality is accepted in homotopy type theory [12]. Propositions are (-1)-types and proposition extensionality is univalence for (-1)- types. 198 SPLST'15 (proof isPropk in Subsection 2.4), using proposition extensionality, we conclude kx R x1 k ≡ kx R x2 k. We have constructed a term px : compat kx R k, and therefore a function lift kx R k px : X/R → U (large elimination is fundamental in order to apply lift, since kx R k : X → U and X → U : U). Moreover, lift kx R k px (abs y) ≡ kx R yk by its computation rule. Let abs x1 ≡ abs x2 for some x1 , x2 : X. We have: kx1 R x2 k ≡ lift kx1 R k px1 (abs x2 ) ≡ lift kx1 R k px1 (abs x1 ) ≡ kx1 R x1 k and x1 R x1 holds, since R is reflexive. 3 Impredicative Encoding of Quotients In this section, we present an implementation of quotients in Calculus of Con- structions (CC). The implementation is different in flavor from the one discussed in Section 2. 3.1 The Type Theory under Consideration Remember that our presentation is done using the language of MLTT. Our Agda formalization makes use of type-in-type instead of Agda’s current implementa- tion of universe polymorphism. This means that we are working in a type theory with only one universe U and U : U. Type-in-type is known to be inconsistent [5, 3], but we are using it only to simulate in Agda the impredicativity of CC, which is consistent. In Subsection 3.3 we need the existence of dependent sums and identity types. P are definable in CC. Consider X : U and P : X → U. The dependent sum Both x:X P x can be defined as follows: ! X Y Y Px= Px→Y →Y x:X Y :U x:X Consider X : U and x1 , x2 : X. We can define (Leibniz ) equality x1 ≡ x2 as follows: Y x1 ≡ x2 = P x1 → P x2 P :X→U One can easily define the constructor and the first projection map of depen- dent sums. ! Y X pair : Px→ Px x:X x:X pair x p = λY f. f x p X fst : Px→X x:X fst c = c X (λx p. x) 199 SPLST'15 It is also possible to prove that Leibniz equality is a substitutive equiv- alence Q relation. But is not possible to construct theP second projection map snd : c:P P x P (fst c), showing that the type x:X P x defined above is x:X a weak dependent sum. Leibniz equality is also weak, since it is not possible to prove “dependent substitutivity”, Q i.e. given a type X, a family of types Y : X → U and a predicate P : x:X → Y x → U, we cannot construct a term subst2 of type Y subst Y p y1 ≡ y2 → P x1 y1 → P x2 y2 p:x1 ≡x2 for all x1 , x2 : X, y1 : Y x1 and y2 : Y x2 . The results of Subsection 3.3 rely on the existence of terms snd and subst2 . Therefore we extend CC with identity types and dependent sums as primitives. As a consequence we obtain that the terms snd and subst2 are easily definable. An instance of subst2 gives us sufficient conditions for proving equality of pairs. Let X be a type and P : X → U a family of types. Then for all x1 , x2 : X, p1 : P x1 and p2 : P x2 : Y pair≡ : subst P r p1 ≡ p2 → pair x1 p1 ≡ pair x2 p2 r:x1 ≡x2 pair≡ r s = subst2 (λx p. pair x1 p1 ≡ pair x p) r s refl We also assume the dependent version of the principle of function extension- ality, i.e. there is a term dfunext that inhabits the type ! Y Y Y Y DFunExt = f1 x ≡ f2 x → f1 ≡ f2 Q {X:U } {Y :X→U } {f1 f2 : x:X →Y x} x:X 3.2 The Implementation We now describe our impredicative implementation of quotients. Let X be a type and R an equivalence relation on X. We define the quotient of X over R as the following type: Y Y X/R = compat f → Y Y :U f :X→Y In other words, X/R is a polymorphic function which assigns, to every type Y equipped with a compatible function f : X → Y , an element of Y . One can then define the constructor abs: abs : X → X/R abs x = λY f r. f x Using the principle of function extensionality one proves that abs is an R- compatible map. Notice that the dependent version of the principle of function 200 SPLST'15 extensionality is needed here, since elements of type X/R are dependent maps. sound : compat abs sound r = dfunext (λY. dfunext (λf. dfunext (λp. p r))) One can then define the non-dependent elimination principle, which turns out to be just function application. Crucially the computation rule holds defini- tionally, as witnessed below in the observation that refl proves the corresponding propositional equality. Y Y lift : compat f → X/R → Y {Y :U } f :X→Y lift {Y } f r q = q Y f p Y Y Y Y liftβ : lift f p (abs x) ≡ f x {Y :U } f :X→Y r:compat f x:X liftβ f r x = refl Note the similarity with Church numerals and the implementation of depen- dent sums given above, and more generally the similarity with the impredicative encoding of inductive types in CC [10]. Moreover this representation is inspired by the impredicative encoding of higher inductive types [12, Ch. 6] in CIC [11]. 3.3 Dependent Elimination While in practice having a definitional computation rule is convenient, it is im- possible to derive a dependent elimination principle. Implementations of induc- tive types in CC in general suffer from this problem [4]. In this subsection we assume the uniqueness property of lift i.e. the fact that, for every type Y and R-compatible function f : X → Y , lift f r is the only map that makes the following diagram commute: X f /7 Y abs  lift f r X/R From the uniqueness property we derive Q the dependent elimination principle. Let Y : X/R → U be a type family and f : x:X Y (abs x) a map with compati- bility proof r : dcompat P f . Using the non-dependent eliminator we define a map of type X/R → q:X/R Y q. Y Y X dlift0 : dcompat f → X/R → Yq Q {Y :X→U } f : x:X Y (abs x) q:X/R dlift0 f r = lift (λx. pair (abs x) (f x)) (λp. pair≡ (sound p) (r p)) 201 SPLST'15 Notice that, for all x : X, fst (dlift0 f r (abs x)) = abs x = id (abs x). Therefore, by the uniqueness property, we obtain a term sq : fst (dlift0 f r q) ≡ q for all q : X/R. This allows us to derive the dependent elimination principle: Y Y Y dlift : dcompat f → Yq Q {Y :X→U } f : x:X Y (abs x) q:X/R dlift {Y } f r q = subst Y sq (snd (dlift0 f r q)) 4 Integer Numbers As an example we present integer numbers. In order to do that we need to have natural numbers in our system (defined as Church numerals in CC or defined inductively in MLTT, it does not matter). We introduce a synonym for pairs of natural numbers, Diff = N × N, and we use the notation − for the constructor of Diff. Elements of Diff represent differences of natural numbers. We define an equivalence relation SameDiff on Diff relating pairs with the same difference: SameDiff : Diff → Diff → U SameDiff (n1 − m1 ) (n2 − m2 ) = plus n1 m2 ≡ plus n2 m1 where plus is addition on N. We define Z = Diff/SameDiff. We show formally that Z is a commutative monoid. The unit zeroZ is the equivalence class of zeroDiff = zero − zero, where zero is the unit of N. Addition is defined in two steps. First we introduce an addition operation on Diff. plusDiff : Diff → Diff → Diff plusDiff (n1 − m1 ) (n2 − m2 ) = plus n1 n2 − plus m1 m2 Before lifting addition to Z, we introduce a useful variant of compat2 , the compatibility predicate for two-argument functions. Let X, Y and Z be types and R, S and T equivalence relations on X, Y and Z respectively. The predicate compat02 on X → Y → Z is defined as follows: Y Y compat02 f = x1 R x2 → y1 S y2 → (f x1 y1 ) T (f x2 y2 ) {x1 ,x2 :X} {y1 ,y2 :Y } A function f satisfies compat02 if it sends R-related and S-related inputs to T -related outputs. It is easy to construct a proof p : compat02 plusDiff . We are ready to lift the addition plusDiff to Z: plusZ : Z → Z → Z plusZ = lift2 (λ d e. abs (plusDiff d e)) (λ r s. sound (p r s)) where lift2 is the two-argument version of lift. We prove the right unit law. First notice that the law holds in Diff up to SameDiff, i.e. for all d : Diff, we have a 202 SPLST'15 proof sd : SameDiff (plusDiff d (zero − zero)) d. We lift this proof to Z: Y rightUnitZ : plusZ z zeroZ ≡ z z:Z rightUnitZ = absEpi (λ d. sound sd ) where absEpi is a proof that the map abs : X → X/R is an epimorphism, for all types X and equivalence relations R on X, i.e. for all types Y and maps f1 , f2 : X/R → Y , if f1 (abs x) ≡ f2 (abs x) for all x : X, then for all q : X/R we have f1 q ≡ f2 q. This is an easy consequence of the uniqueness property. We observe that working with impredicative quotients facilitates proofs, since the computation rule holds definitionally. 5 Finite Multisubsets Another example we present is finite multisubsets of a given type X. In this section we work in MLTT. Let X be a type with decidable equality, i.e. there exists a function dec≡ : X → X → Bool such that dec≡ x1 x2 = true if and only if x1 ≡ x2 . We introduce the binary relation Perm on List X, inductively defined by the rules: Perm xs ys Perm [] [] Perm (x :: xs) (x :: ys) Perm xs ys Perm xs ys Perm ys zs Perm (x :: y :: xs) (y :: x :: ys) Perm xs zs Two lists xs and ys are in the relation Perm if xs is a permutation of ys. The relation is transitive by construction, and it is easily provable reflexive and symmetric. Therefore we form the quotient Multisubset X = List X/Perm, i.e. a finite multisubset of X is a list modulo permutations. We introduce a function counting the multiplicity of an element x in a list xs. If the element does not belong to the list, then its multiplicity is zero. Note that decidable equality on X is fundamental in order to count the number of occurrences of x in xs. multiplicity : X → List X → N multiplicity x [] = zero multiplicity x (y :: xs) with dec≡ x y multiplicity x (y :: xs) | true = suc (multiplicity x xs) multiplicity x (y :: xs) | false = multiplicity x xs The function multiplicity can be proved compatible with the relation Perm. This is true since permuting a list does not alter the number of occurrences of an element in it. The proof is easily done by induction on the structure of Perm. Therefore the function multiplicity lifts to Multisubset X. 203 SPLST'15 We conclude this section by noting that there are other possible definitions of “equality” on finite multisubsetsQ of X. For example one could define a relation Perm0 on List X as Perm0 xs ys = x:X (x ∈ xs) ∼ = (x ∈ ys), where ∼ = is type isomorphism and ∈ is list membership. The definition of Perm0 is more concise that the definition of Perm. The two relations are logically equivalent, but prov- ing multiplicity compatible with Perm0 is much more complicated than proving multiplicity compatible with Perm. 6 Conclusions In this paper we showed two different implementation of quotient types. Both are set-based and therefore different from the setoid-based approach. In Section 2 we presented inductive-like quotients in Martin-Löf type theory. They do not need impredicativity in order to be introduced, but their exis- tence has to be postulated. Moreover the computation rule only holds up to propositional equality. Hofmann’s extension of Calculus of Constructions [6] is consistent, therefore the same holds for our implementation in MLTT. In Section 3 we presented an impredicative encoding of quotients in Calculus of Constructions. In order to derive the dependent elimination principle from the uniqueness property we need to extend CC with dependent sums and identity types. Our implementation shows that, at the cost of impredicativity, quotient types are definable. However they are “weak”, similarly to Leibniz equality or the impredicative encoding of dependent sums given in Subsection 3.2. To get “strong” quotients, one needs to introduce postulates, such as the uniqueness property. Geuvers [4] showed that postulating dependent elimination for im- predicative encodings of inductive types is safe. Similarly this can be extended to our quotient types. The uniqueness property of quotients is logically equiva- lent to the dependent elimination principle, therefore assuming the uniqueness property is also safe. There are other ways of deriving the dependent elimination principle for inductive types in impredicative systems such as CC, most notably parametricity [13]. Acknowledgement This research was supported by the ERDF funded ICT na- tional programme project ”Coinduction”, the Estonian Science Foundation grant no. 9219 and the Estonian Ministry of Education and Research institutional re- search grant no. PUT33-13. References 1. Y. Bertot and P. Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer, 2004. 2. L. Chicli, L. Pottier, and C. Simpson. Mathematical quotients and quotient types in Coq. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, volume 2646 of Lecture Notes in Computer Science, pages 95–107. Springer, 2003. 3. T. Coquand. An analysis of Girard’s paradox. In Symposium on Logic in Computer Science, pages 227–236. IEEE Computer Society, 1986. 204 SPLST'15 4. H. Geuvers. Induction is not derivable in second order dependent type theory. In S. Abramsky, editor, Typed Lambda Calculi and Applications, volume 2044 of Lecture Notes in Computer Science, pages 166–181. Springer, 2001. 5. J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur, Ph.D. thesis, Université Paris VII, 1972. 6. M. Hofmann. Extensional concepts in intensional type theory, Ph.D. thesis, Uni- versity of Edinburgh, 1995. 7. M. Maietti. About effective quotients in constructive type theory. In T. Altenkirch, B. Reus, and W. Naraschewski, editors, Types for Proofs and Programs, volume 1657 of Lecture Notes in Computer Science, pages 166–178. Springer, 1999. 8. B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf ’s type theory. Oxford University Press Oxford, 1990. 9. U. Norell. Dependently typed programming in Agda. In P. Koopman, R. Plasmei- jer, and S. D. Swierstra, editors, Advanced Functional Programming, volume 5832 of Lecture Notes in Computer Science, pages 230–266. Springer, 2009. 10. F. Pfenning and C. Paulin-Mohring. Inductively defined types in the calculus of constructions. In M. G. Main, A. Melton, M. W. Mislove, and D. A. Schmidt, edi- tors, Mathematical Foundations of Programming Semantics, volume 442 of Lecture Notes in Computer Science, pages 209–228. Springer, 1989. 11. M. Shulman. Higher inductive types via impredicative polymor- phism. Blog post, 2011. http://homotopytypetheory.org/2011/04/25/ higher-inductive-types-via-impredicative-polymorphism. 12. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foun- dations of Mathematics. Institute for Advanced Study, 2013. http:// homotopytypetheory.org/book. 13. P. Wadler. The Girard–Reynolds isomorphism. Theoretical Computer Science, 375(1):201–226, 2007. 205