We present and compare two di erent implementations of quotient types in Intensional Type Theory. We rst 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.
In this paper we present two di erent frameworks for reasoning about
setbased quotients, i.e. quotients as types. We rst introduce in Section 2 quotients
as particular inductive-like types. The presentation is inspired by quotient types
in Martin Hofmann's PhD thesis [
Note that integer numbers are already de nable 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 nonnegative numbers. Note that in order to avoid the presence of two zeros, the elements of the rst 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, de ning 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 de nitions. 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 [
In this section, we introduce quotient types as particular inductive-like types
introduced by M. Hofmann [
The Type Theory under Consideration We consider Martin-Lof type theory (MLTT) with inductive types and a cumulative 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 judgmental (de nitional) equality. Re exivity, symmetry, transitivity and substitutivity of are named re , sym, trans and subst, respectively.
We assume uniqueness of identity proofs for all types, i.e., an inhabitant for UIP =
Y
Y
Y fX:Ug fx1;x2:Xg p1;p2:x1 x2 p1
p2:
A type X is said to be a proposition, if it has at most one inhabitant, i.e., if the type isProp X = x1
x2
Y 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 a 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 compat f =
Y fx1;x2:Xg x1Rx2 ! f x1 f x2 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: for every family of types Y : X=R ! Uk and function f : Qx:X Y (abs x) with p : dcompat f , there exists a function lift f p : Qq:X=R Y q; (iv) a computation rule: for every family of types Y : X=R ! Uk, function f : Qx:X Y (abs x) with p : dcompat f and x : X we have lift f p x : lift f p (abs x)
f x Y
Y fx1;x2:Xg r:x1Rx2
The predicate dcompat represents compatibility for dependent functions f : Qx:X Y (abs x): dcompat f = subst Y (sound r) (f x1) f x2: We postulate the existence of data (i){(iv) for all types X and equivalence relations 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. 2.3
Classical Quotients Classically every equivalence class in a quotient X=R has a representative element in the original set, i.e. a map rep : X=R ! X that satis es the following conditions: complete : Y (rep (abs x)) R x
x:X stable : Y 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 [
In general in constructive mathematics, for a given equivalence class there is no canonical choice of a representative. This idea is re ected in the implementation 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 de nes a monad: the unit is j j and multiplication k : kkXkk ! kXk is de ned 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 FunExt f g =
Y f x x:X
gx
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 propositional equality. If equality in lift were de nitional, 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
E ectiveness
A quotient X=R is said to be e ective, if the type Qx1;x2:X abs x1 abs x2 !
x1 R x2 is inhabited. In general, e ectiveness does not hold for all quotients.
Moreover, postulating e ectiveness for all quotients implies the law of excluded
middle [
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 satis es a weaker property. The principle of proposition extensionality states that logically equivalent propositions are equal:1
PropExt = isProp X ! isProp Y ! X $ Y ! X
Y
Y fX;Y :Ug where X $ Y = (X ! Y ) (Y ! X). We say that a quotient X=R is weakly e ective, if the type Qx1;x2:X abs x1 abs x2 ! kx1 R x2k is inhabited.
If we extend our type theory with PropExt, we can prove that all quotients are weakly e ective.
Proposition 1. Under the hypothesis of proposition extensionality, all quotients are weakly e ective.
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 x0k. We show that
kxR k is R-compatible. Let x1; x2 : X with x1 Rx2. We have xRx1 $ xRx2 and
therefore kx R x1k $ kx R x2k. Since propositional truncations are propositions
1 Note that proposition extensionality is accepted in homotopy type theory [
Propositions are (-1)-types and proposition extensionality is univalence for (-1)types. (proof isPropk in Subsection 2.4), using proposition extensionality, we conclude kx R x1k kx R x2k. 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 x2k lift kx1R k px1 (abs x2) lift kx1 R k px1 (abs x1) kx1 R x1k and x1 R x1 holds, since R is re exive.
In this section, we present an implementation of quotients in Calculus of Constructions (CC). The implementation is di erent in avor 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
implementation 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
[
In Subsection 3.3 we need the existence of dependent sums and identity types. Both are de nable in CC. Consider X : U and P : X ! U . The dependent sum Px:X P x can be de ned as follows: pair : Y
P x !
X P x x:X x:X pair x p = Y f: f x p fst : X P x ! X
x:X fst c = c X ( x p: x) X P x = Y x:X
Y :U
Y P x ! Y x:X
Consider X : U and x1; x2 : X. We can de ne (Leibniz ) equality x1 follows: x2 as x1 x2 =
Y
P x1 ! P x2
P :X!U
One can easily de ne the constructor and the rst projection map of dependent sums. !
! Y !
It is also possible to prove that Leibniz equality is a substitutive equivalence relation. But is not possible to construct the second projection map snd : Qc:Px:X P x P (fst c), showing that the type Px:X P x de ned above is a weak dependent sum. Leibniz equality is also weak, since it is not possible to prove \dependent substitutivity", i.e. given a type X, a family of types Y : X ! U and a predicate P : Qx:X ! Y x ! U , we cannot construct a term subst2 of type
Y 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 de nable. An instance of subst2 gives us su cient 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: pair :
Y r:x1 x2 pair r s = subst2 ( x p: pair x1 p1
pair x p) r s re subst P r p1 p2 ! pair x1 p1 pair x2 p2
We also assume the dependent version of the principle of function extensionality, i.e. there is a term dfunext that inhabits the type
DFunExt =
Y
Y
Y fX:Ug fY :X!Ug ff1 f2:Qx:X !Y xg
Y f1 x x:X
! f2 x ! f1 f2 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 de ne the quotient of X over R as the following type:
X=R = Y
Y Y :U f:X!Y
compat f ! 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 de ne 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 Rcompatible map. Notice that the dependent version of the principle of function 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 de ne the non-dependent elimination principle, which turns out to be just function application. Crucially the computation rule holds de nitionally, as witnessed below in the observation that re proves the corresponding propositional equality.
lift : Y
Y fY :Ug f:X!Y lift fY g f r q = q Y f p
compat f ! X=R ! Y lift : Y
Y
Y
Y lift f p (abs x) f x fY :Ug f:X!Y r:compat f x:X lift f r x = re
Note the similarity with Church numerals and the implementation of
dependent sums given above, and more generally the similarity with the impredicative
encoding of inductive types in CC [
Dependent Elimination
While in practice having a de nitional computation rule is convenient, it is
impossible to derive a dependent elimination principle. Implementations of
inductive types in CC in general su er from this problem [
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 abs X=R f lift f r 7/ Y
From the uniqueness property we derive the dependent elimination principle. Let Y : X=R ! U be a type family and f : Qx:X Y (abs x) a map with compatibility proof r : dcompat f . Using the non-dependent eliminator we de ne a map of type X=R ! Pq:X=R Y q.
dlift0 :
Y
Y
dcompat f ! X=R ! X Y q
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: dlift :
Y
Y As an example we present integer numbers. In order to do that we need to have natural numbers in our system (de ned as Church numerals in CC or de ned inductively in MLTT, it does not matter). We introduce a synonym for pairs of natural numbers, Di = N N, and we use the notation for the constructor of Di . Elements of Di represent di erences of natural numbers. We de ne an equivalence relation SameDi on Di relating pairs with the same di erence:
SameDi (n1 ! Di m1) (n2 ! U m2) = plus n1 m2 plus n2 m1 where plus is addition on N. We de ne Z = Di =SameDi . We show formally that Z is a commutative monoid. The unit zeroZ is the equivalence class of zeroDi = zero zero, where zero is the unit of N. Addition is de ned in two steps. First we introduce an addition operation on Di .
plusDi : Di plusDi (n1 ! Di m1) (n2 ! Di 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 de ned as follows: compat02 f =
Y
Y fx1;x2:Xg fy1;y2:Y g
x1 R x2 ! y1 S y2 ! (f x1 y1) T (f x2 y2)
A function f satis es compat02 if it sends R-related and S-related inputs to T -related outputs. It is easy to construct a proof p : compat02 plusDi . We are ready to lift the addition plusDi to Z: plusZ : Z ! Z ! Z plusZ = lift2 ( d e: abs (plusDi 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 Di up to SameDi , i.e. for all d : Di , we have a proof sd : SameDi (plusDi d (zero
zero)) d. We lift this proof to Z: rightUnitZ : Y 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 de nitionally. 5
Another example we present is nite 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 de ned by the rules:
Perm [] []
Perm (x :: y :: xs) (y :: x :: ys)
Perm (x :: xs) (x :: ys)
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 re exive and symmetric. Therefore we form the quotient Multisubset X = List X=Perm, i.e. a nite 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) j true = suc (multiplicity x xs) multiplicity x (y :: xs) j 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.
We conclude this section by noting that there are other possible de nitions of \equality" on nite multisubsets of X. For example one could de ne a relation Perm0 on List X as Perm0 xs ys = Qx:X (x 2 xs) = (x 2 ys), where = is type isomorphism and 2 is list membership. The de nition of Perm0 is more concise that the de nition of Perm. The two relations are logically equivalent, but proving multiplicity compatible with Perm0 is much more complicated than proving multiplicity compatible with Perm. 6
In this paper we showed two di erent implementation of quotient types. Both are set-based and therefore di erent from the setoid-based approach.
In Section 2 we presented inductive-like quotients in Martin-Lof type theory.
They do not need impredicativity in order to be introduced, but their
existence has to be postulated. Moreover the computation rule only holds up to
propositional equality. Hofmann's extension of Calculus of Constructions [
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 de nable. 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 [
Acknowledgement This research was supported by the ERDF funded ICT national programme project "Coinduction", the Estonian Science Foundation grant no. 9219 and the Estonian Ministry of Education and Research institutional research grant no. PUT33-13.