key: cord-0054936-ng5qf8cq
authors: Fiore, Marcelo P.; Pitts, Andrew M.; Steenkamp, S. C.
title: Constructing Infinitary Quotient-Inductive Types
date: 2020-04-17
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-45231-5_14
sha: 01fb7400cd1e6ae8d73874b55c8b0937a4bb3fee
doc_id: 54936
cord_uid: ng5qf8cq

This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types can be encoded using the combination of inductive-inductive definitions involving strictly positive occurrences of Hofmann-style quotient types, and Abel’s size types. The latter, which provide a convenient constructive abstraction of what classically would be accomplished with transfinite ordinals, are used to prove termination of the recursive definitions of the elimination and computation properties of our encoding of QW-types. The development is formalized using the Agda theorem prover.

One of the key features of proof assistants based on dependent type theory such as Agda, Coq and Lean is their support for inductive definitions of families of types. Homotopy Type Theory [29] introduces a potentially very useful extension of the notion of inductive definition, the higher inductive types (HITs). To define an ordinary inductive type one declares how its elements are constructed. To define a HIT one not only declares element constructors, but also declares equality constructors in identity types (possibly iterated ones), specifying how the constructed elements and identities are to be equated. In this paper we work in a dependent type theory satisfying uniqueness of identity proofs (UIP), so that identity types are trivial in dimensions higher than one. Nevertheless, as Altenkirch and Kaposi [5] point out, HITs are still useful in such a one-dimensional setting. They introduce the term quotient inductive type (QIT) for this truncated form of HIT. Figure 1 gives two examples of QITs, using Agda-style notation for dependent type theory; in particular, Set denotes a universe of types and ≡ denotes the identity type. The first example specifies the element and equality constructors for the type Bag X of finite multisets of elements from a type X. The second example, adapted from [5] , specifies the element and equality constructors for the type ωTree X of trees whose nodes are labelled with elements of X and that have unordered countably infinite branching. Both examples illustrate the nice feature of QITs that users only have to specify the particular identifications between data needed for their applications. Thus the standard property of equality that it is an equivalence relation respecting the constructors is inherited by construction from the usual properties of identity types, without the need to say so in the declaration of the QIT. The second example also illustrates a more technical aspect of QITs, that they enable constructive versions of structures that classically use non-constructive choice principles. The first example in Figure 1 only involves element constructors of finite arity ([] is nullary and x :: _ is unary) and consequently Bag X is isomorphic to the type obtained from the ordinary inductive type of finite lists over X by quotienting by the congruence generated by swap. Of course this assumes, as we do in this paper, that the type theory comes with Hofmann-style quotient types [18, Section 3.2.6.1]. By contrast, the second example in the figure involves an element constructor with countably infinite arity. So if one first forms the ordinary inductive type of ordered countably branching trees (by dropping the equality constructor perm from the declaration) and then quotients by a suitable relation to get the equalities specified by perm, one needs the axiom of countable choice to be able to lift the node element constructor to the quotient; see [5, Section 2.2] for a detailed discussion. The construction of the Cauchy reals as a higher inductive-inductive type [29, Section 11 .3] provides a similar, but more complicated example where use of countable choice is avoided. Such examples have led to the folklore that as far as constructive type theories go, infinitary QITs are more expressive than the combination of ordinary inductive (or inductive-recursive, or inductive-inductive) types with quotient types. In this paper we use Abel's sized types [2] to show that, for a wide class of QITs, this view is not justified. Thus we make two main contributions:

First we define a family of QITs called QW-types and give elimination and computation rules for them (Section 2). The usual W-types of Martin-Löf [22] are inductive types giving the algebraic terms over a possibly infinitary signature.

One specifies a QW-type by giving a family of equations between such terms. So such QITs give initial algebras for possibly infinitary algebraic theories. As we indicate in Section 3, they can encode a very wide range of examples of possibly infinitary quotient-inductive types, namely those that do not involve constructors taking previously constructed equalities as arguments (so do not cover the infinitary extension of the very general scheme considered by Dybjer and Moeneclaey [12] ). In set theory with the Axiom of Choice (AC), QW-types can be constructed simply as Quotients of the underlying W-type-hence the name.

Secondly, we prove that contrary to expectation, without AC it is still possible to construct QW-types using quotients, but not simply by quotienting a W-type. Instead, the type to be quotiented and the relation by which to quotient are given simultaneously by definitions that refer to each other. Thus our construction (in Section 4) involves inductive-inductive definitions [15] . The elimination and computation functions which witness that the quotiented type correctly represents the required QW-type are defined recursively. In order to prove that our recursive definitions terminate we combine the use of inductive definitions involving strictly positive occurrences of quotient types with sized types (currently, we do not know whether it is possible to avoid sizing in favour of, say, a suitable well-founded termination ordering). Sized types provide a convenient constructive abstraction of what classically would be accomplished with sequences of transfinite ordinal length.

To present our results we need a version of Martin-Löf Type Theory with (1) uniqueness of identity proofs, (2) quotient types and hence also function extensionality, (3) inductive-inductive datatypes (with strictly positive occurrences of quotient types) and (4) sized types. Lean 3 provides (1) and (2) out of the box, but also the Axiom of Choice, unfortunately. Neither it, nor Coq provide (3) and (4) . Agda provides (1) via unrestricted dependent pattern-matching, (2) via a combination of postulates and the rewriting mechanism of Cockx and Abel [8] , (3) via its very liberal mechanism for mutual definitions and (4) thanks to the work of Abel [2] . Therefore we make use of the type theory implemented by Agda (version 2.6.0.1) to give formal proofs of our results. The Agda code can be found at doi: 10.17863/CAM.48187. In this paper we describe the results informally, using Agda-style notation for dependent type theory. In particular we use Set to denote the universe at the lowest level of a countable hierarchy of (Russell-style) universes. We also use Agda's convention that an implicit argument of an operation can be made explicit by enclosing it in {braces}.

We begin by recalling some facts about types of well-founded trees, the W-types of Martin-Löf [22] . We take signatures to be elements of the dependent product

So a signature is given by a pair Σ = (A, B) consisting of a type A : Set and a family of types B : A → Set. Each such signature determines a polynomial endofunctor [1, 16] S{Σ} : Set → Set whose value at X : Set is the following dependent product S{Σ}X = a : A, (B a → X)

An S-algebra is by definition an element of the dependent product

S-algebra morphisms (X, s) → (X , s ) are given by functions h : X → X together with an element of the type

Then the W-type W{Σ} determined by Σ is the underlying type of an initial S-algebra. More generally, Dybjer [11] shows that the initial algebra of any nonnested, strictly positive endofunctor on Set is given by a W-type; and Abbott, Altenkirch, and Ghani [1] extend this to the case with nested uses of W-types as part of their work on containers. (These proofs take place in extensional type theory [22] , but work just as well in the intensional type theory with uniqueness of identity proofs and function extensionality that we are using here.) More concretely, given a signature Σ = (A, B), if one thinks of elements a : A as names of operation symbols whose (not necessarily finite) arity is given by the type B a : Set, then the elements of W{Σ} represent the closed algebraic terms (i.e. well-founded trees) over the signature. From this point of view it is natural to consider not only closed terms solely built up from operations, but also open terms additionally built up with variables drawn from some type X. As well as allowing operators of possibly infinite arity, we also allow terms involving possibly infinitely many variables (the second example in Figure 1 involves such terms). Categorically, the type T{Σ}X of such open terms is the free S-algebra on X and is another W-type, for the signature obtained from Σ by adding the elements of X as nullary operations. Nevertheless, it is convenient to give a direct inductive definition:

Given an S-algebra (Y, s) : Alg{Σ} and a function f : X → Y , the unique morphism of S-algebras from the free S-algebra (T X, σ) on X to (Y, s) has underlying function T X → Y mapping each t : T X to the element t = f in Y defined 1 by recursion on the structure of t:

As the notation suggests, = is the Kleisli lifting operation ("bind") for a monad structure on T; indeed, it is the free monad on the endofunctor S. The notion of "QW-type" that we introduce in this section is obtained from that of W-type by considering not only the algebraic terms over a given signature, but also equations between terms. To code equations we use a type-theoretic rendering of a categorical notion of equational system introduced by Fiore and Hur, referred to as term equational system [14, Section 2] and as monadic equational system [13, Section 5] , here instantiated to free monads on signatures. Thus a system of equations over Σ is an element of the dependent product

An S{Σ}-algebra S X → X 

The category-theoretic view of QW-types is that they are simply S-algebras that are initial among those satisfying a given system of equations:

Definition 2. A QW-type for a signature Σ = (A, B) : Sig and system of equations ε = (E, V, l, r) : Syseq{Σ} is given by a type QW{Σ}{ε} : Set equipped with an S-algebra structure and a proof that it satisfies the equations

together with functions that witness that it is the initial such algebra:

Given the definitions of S{Σ} in (2) and Sat{ε} in (8), properties (9) and (10) suggest that a QW-type is an instance of the notion of quotient-inductive type [5] with element constructor qwintro and equality constructor qwequ. For this to be so, QW{Σ}{ε} needs to have the requisite dependently-typed elimination and computation 2 properties for these element and equality constructors. As Proposition 1 below shows, these follow from (11)-(13), because we are working in a type theory with function extensionality (by virtue of assuming quotient types). To state the proposition we need a dependent version of (6). For each

type X : Set, function f : X → x : QW, P x and term t : T(X), we get an element lift P p f t : P (t = fst • f ) defined by recursion on the structure of t:

Proposition 1. For a QW-type as in the above definition, given P and p as in (14) and a term of type

there are elimination and computation terms:

(Note that (16) uses McBride's heterogeneous equality type [23] , which we denote by ≡≡, because lift P p f (l e) and lift P p f (r e) inhabit different types, namely P (l e = fst • f ) and P (r e = fst • f ) respectively.)

The proof of the proposition can be found in the accompanying Agda code (doi: 10.17863/CAM.48187).

So QW-types are in particular quotient-inductive types (QITs). Conversely, in the next section we show that a wide range of QITs can be encoded as QW-types. Then in Section 4 we prove: Theorem 1. In constructive dependent type theory with uniqueness of identity proofs (or equivalently the Axiom K of Streicher [27] ) and universes with induct ive-inductive datatypes [15] permitting strictly positive occurrences of quotient types [18] and sized types [2] , for every signature and system of equations (Defin ition 1) there is a QW-type as in Definition 2.

Remark 1 (Free algebras). Definition 2 defines QW-types as initial algebras. A corollary of Theorem 1 is that free-algebras also exist. In other words, given a signature Σ and a type X : Set, there is an S-algebra

satisfying a system of equations ε and equipped with a function X → F{Σ}{ε}X, and which is universal among such S-algebras. Thus QW{Σ}{ε} is isomorphic to F{Σ}{ε}∅, where ∅ is the empty datatype.

To see that such free algebras can be constructed as QW-types, given a signature Σ = (A, B), let Σ X be the signature (X A, B ), where X A is the coproduct datatype (with constructors inl : X → X A and inr : A → X A) and where B : X A → Set maps each inl x to ∅ and each inr a to B a. Given a system of equations ε = (E, V, l, r), let ε X be the system (E, V, l X , r X ) where for each e : E, l X e = l e = η and r X e = r e = η (using η : V e → T{Σ X }(V e) as in (5) and the S{Σ}-algebra structure s on T{Σ X }(V e) given by s(a, b) = σ(inr a, b)). Then one can show that the QW-type QW{Σ X }{ε X } is the free algebra F{Σ}{ε}X, with the function X → F{Σ}{ε}X sending each x : X to qwintro(inl x, _) : QW{Σ X }{ε X }, and the S{Σ}-algebra structure on F{Σ}{ε}X being given by the function sending (a, b) : S(QW{Σ X }{ε X }) to qwintro(inr a, b).

Remark 2 (Strictly positive equational systems). A very general, categorical notion of equational system was introduced by Fiore and Hur [14, Section 3]. They regard any endofunctor S : Set → Set as a functorial signature. A functorial term over such a signature, S G L, is specified by another functorial signature G : Set → Set (the term's context) together with a functor L from S-algebras to G-algebras that commutes with the forgetful functors to Set. Then an equational system is given by a pair of such terms in the same context, S G L and S G R say. An S-algebra s : S X → X satisfies the equational system if L(X, s) and R(X, s) are equal G-algebras.

Taking the strictly positive endofunctors Set → Set to be the smallest collection containing the identity and constant endofunctors and closed under forming dependent products and dependent functions over fixed types then, as in [11] (and also in the type theory in which we work), up to isomorphism every such endofunctor is of the form S{Σ} for some signature Σ : Sig. If we restrict attention to equational systems S G L, R with S and G strictly positive, then it turns out that such equational systems are in bijection with the systems of equations from Definition 1, and the two notions of satisfaction for an algebra coincide in that case. (See our Agda development for a proof of this.) So Dybjer's characterisation of W-types as initial algebras for strictly positive endofunctors generalises to the fact that QW-types are initial among the algebras satisfying strictly positive equational systems in the sense of Fiore and Hur.

Higher inductive types (HITs) are originally motivated by their use in homotopy type theory to construct homotopical cell complexes, such as spheres, tori, and so on [29] . Intuitively, a higher inductive type is an inductive type with point constructors also allowing for path constructors, surface constructors, etc., which are represented as elements of (iterated) identity types. For example, the sphere is given by the HIT 3 :

In the presence of the UIP axiom we will refer to HITs as quotient inductive types (QITs) [5] , since all paths beyond the first level are trivial and any HIT is truncated to an h-set. We use the terms element constructor and equality constructor to refer to the point constructors and the only non-trivial level of path constructors.

We believe that QW-types can be used to encode a wide range of QITs: see Example 1 (Finite multisets). The element constructors for finite multisets are encoded exactly as with a W-type: the constructors are [] and x :: _ for each x : X. So we take A to be 1 X, the coproduct of the unit type 1 (whose single constructor is denoted tt) with X. The arity of [] is zero, and the arity of each x :: _ is one, represented by the empty type ∅ and unit type 1 respectively; so we take B : A → Set to be the function [λ_→ 0 | λ_→ 1] : 1 X → Set mapping inl tt to ∅ and each inr x to 1.

The swap equality constructor is parameterised by elements of E = X × X. For each (x, y) : E, swap x y yields an equation involving a single free variable (called ys : Bag X in Figure 1 ); so we take V : E → Set to be λ_→ 1. Each side of the equation named by swap x y is coded by an element of T{Σ}(V (x, y)) = T{Σ} (1) . Recalling the definition of T from (5), the single free variable corresponds to η tt : T{Σ}(1) and then the left-hand side of the equation is σ(inr x, (λ_→ σ(inr y, (λ_→ η tt)))) and the right-hand side is σ(inr y, (λ_→ σ(inr x, (λ_→ η tt)))).

So, altogether, the signature and system of equations for the QW-type corresponding to the first example in Figure 1 is:

(λ_→ σ(inr y, (λ_→ η tt)))) r = λ (x, y) → σ(inr y, (λ_→ σ(inr x, (λ_→ η tt)))) Example 2 (Unordered countably-branching trees). Here the element constructors are leaf of arity zero and, for each x : X, node x of arity N. So we use the signature with A = 1 X and B = [λ_→ ∅ | λ_→ N].

The perm equality constructor is parameterised by elements of So, altogether, the signature and system of equations for the QW-type corresponding to the second example in Figure 1 is:

That unordered countably-branching trees are a QW-type is significant since no previous work on various subclasses of QITs (or indeed QIITs [19, 10] ) supports infinitary QITs [6, 26, 28, 12, 19, 10] . See Example 5 for another, more substantial infinitary QW-type. So this extension represents one of our main contributions. QW-types generalise prior developments; the internal encodings for particular subclasses of 1-HITs given by Sojakova [26] and Swan [28] are direct instances of QW-types, as the next two examples show.

Example 3. W-suspensions [26] are an instance of QW-types. The data for a W-suspension is: A , C : Set, a type family B : A → Set and functions l , r : C → A . The equivalent QW-type is:

Example 4. The non-indexed case of W-types with reductions [28] are QW-types.

The data of such a type is: Y : Set, X : Y → Set and a reindexing map R : (y : Y ) → Xy. The reindexing map identifies a term σ (y, α) with some α (R y) used to construct it. The equivalent QW-type is given by:

Example 5. Lumsdaine and Shulman [21, Section 9] give an example of a HIT not constructible in type theory from only pushouts and N. Their HIT F can be thought of as a set of notations for countable ordinals. It consists of three point constructors: 0 : F , S : F → F , and sup : (N → F ) → F , and five path constructors which are omitted here for brevity. It is inspired by the infinitary algebraic theory of Blass [7, Section 9] and hence it is not surprising that it can be encoded by a QW-type; the details can be found in our Agda code.

Basold, Geuvers, and van derWeide [6] present a schema (though not a model) for infinitary QITs that do not support conditional path equations. Constructors are defined by arbitrary polynomial endofunctors built up using (non-dependent) products and sums, which means in particular that parameters and arguments can occur in any order. They require constructors to be in uncurried form. Basold, Geuvers, and van derWeide [12, Sections 3.1 and 3.2] present a schema for finitary QITs that supports conditional path equations, where constructors are allowed to take inductive arguments not just of the datatype being declared, but also of its identity type. This schema can be generalised to infinitary QITs with conditional path equations. We believe this extension of their schema to be the most general schema for QITs. The schema requires all parameters to appear before all arguments, whereas the schema for regular inductive types in Agda is more flexible, allowing parameters and arguments in any order.

We wish to combine the schema for infinitary QITs of Basold, Geuvers, and van der Weide [6] with the schema for QITs with conditional path equations of Dybjer and Moeneclaey [12] to provide a general schema. Moreover, we would like to combine the arbitrarily ordered parameters and arguments of the former with the curried constructors of the latter in order to support flexible pattern matching.

For consistency with the definition of inductive types in Agda [9, equation (25) and figure 1] we will define strictly positive (i.e. polynomial) endofunctors in terms of strictly positive telescopes.

A telescope is given by the grammar:

A telescope extension (x : A)∆ binds (free) occurrences of x inside the tail ∆.

The type A may contain free variables that are later bound by further telescope extensions on the left. A telescope can also exist in a context which binds any free variables not already bound in the telescope. Such a context is implicit in the following definitions. A function type ∆ → C from a telescope ∆ to a type C is defined as an iterated dependent function type by:

A strictly positive endofunctor on a variable Y is presented by a strictly positive telescope

where each type scheme Φ i is described by a expression on Y made up of Π-types, Σ-types, and any (previously defined "constant") types A not containing Y , according to the grammar:

For example, ∆ def = (x : X)(f : N → Y ) is the strictly positive telescope for the node constructor in Figure 1 . In this instance, reordering x and f is permitted by exchange. Note that the variable Y can never appear in the argument position of a Π-type.

Now it is possible to define the form of the endpoints of an equality (within the context of a strictly positive telescope), corresponding to the notion of an abstract syntax tree with free variables. With this intuition in mind, we can take the definition in Dybjer and Moeneclaey's presentation [12] of endpoints given by point constructor patterns: l, r, p ::= c i k | y

Where y : Y is in the context of the telescope for the equality constructor, and k is a term built without any rule for Y , but which may use other point constructor patterns p : Y . (That is, any sub-term of type Y must either be a variable y : Y found in the telescope, or a constructor for Y applied to further point constructor patterns and earlier defined constants. It could not, for instance, use the function application rule for Y with some function g : M → Y , not least since such functions cannot be defined before defining Y .) Note that this exactly matches the type T in (5). Basold, Geuvers, and van der Weide's presentation has a sightly more general notion of constructor term [6, Definition 6] (Dybjer and Moeneclaey's presentation [12] has more restricted telescopes). It is defined by rules which operate in the context of a strictly positive (polynomial) telescope and permit use of its bound variables, and the use of constructors c i , but not any other rules for Y . We take the dependent form of their rules for products and functions. Note that these rules do not allow the use of terms of type ≡ Y in the endpoints.

As with inductive types, the element constructors of QITs are specified by strictly positive telescopes. The equality constructors also permit conditions to appear in strictly positive positions, where l and r are constructor terms according to grammar (22) : Φ(Y ), Ψ(Y ) ::= (same grammar as in (21)

Definition 3. A QIT is defined by a list of named element constructors and equality constructors:

where ∆ i are strictly positive telescopes on Y according to (21) , and Θ j are strictly positive telescopes on Y and ≡ Y in which conditions may also occur in strictly positive positions according to (23) .

QITs without equality constructors are inductive types. If none of the equality constructors contain Y in an argument position then it is called non-recursive, otherwise it is called recursive [6] . If none of the equality constructors contain an equality in Y then we call it a non-conditional, or equational, QIT, otherwise it is called a conditional [12] , or quasi-equational, QIT. If all of the constant types A in any of the constructors are finite (isomorphic to Fin n for n : N) then it is called a finitary QIT [12] . Otherwise, it is called a generalised [12] , or infinitary, QIT.

We are not aware of any existing examples in the literature of HITs which allow the point constructors to be conditional (though it is not difficult to imagine), nor any schemes for HITs that allow such definitions. However, we do believe this is worth investigating further.

Any equational QIT can be encoded as a QW-type.

We believe this can be proved analogously to the approach of Dybjer [11] for inductive types, though the endpoints still need to be considered and we have not yet translated the schema in definition 3 into Agda.

Remark 3. Assuming Conjecture 1, Basold, Geuvers, and van der Weide's schema [6] , being an equational (non-conditional) instance of Definition 3, can be encoded as a QW-type.

In Section 2 we defined a QW-type to be initial among algebras over a given (possibly infinitary) signature satisfying a given systems of equations (Definition 2). If one interprets these notions in classical Zermelo-Fraenkel set theory with the axiom of Choice (ZFC), one regains the usual notion from universal algebra of initial algebras for infinitary equational theories. Since in the set-theoretic interpretation there is an upper bound on the cardinality of arities of operators in a given signature Σ, the ordinal-indexed sequence S α (∅) of iterations of the functor in (2) starting from the empty set eventually becomes stationary; and so the sequence has a small colimit, namely the set W{Σ} of well-founded trees over Σ. A system of equations ε (Definition 1) over Σ generates a Σ-congruence relation ∼ on W{Σ}. The quotient set W{Σ}/∼ yields the desired initial algebra for (Σ, ε) provided the S-algebra structure on W{Σ} induces one on the quotient set. It does so, because for each operator, using AC one can pick representatives of the (possibly infinitely many) equivalence classes that are the arguments of the operator, apply the interpretation of the operator in W{Σ} and then take the equivalence class of that. So the set-theoretic model of type theory in ZFC models QW-types. Is this use of choice really necessary? Blass [7, Section 9] shows that if one drops AC and just works in ZF, then provided a certain large cardinal axiom is consistent with ZFC, it is consistent with ZF that there is an infinitary equational theory with no initial algebra. He shows this by first exhibiting a countably presented equational theory whose initial algebra has to be an uncountable regular cardinal; and secondly appealing to the construction of Gitik [17] of a model of ZF with no uncountable regular cardinals (assuming a certain large cardinal axiom). Lumsdaine and Shulman [21] turn the infinitary equational theory of Blass into a higher-inductive type that cannot be proved to exist in ZF (and hence cannot be constructed in type theory just using pushouts and the natural numbers). We noted in Example 5 that this higher inductive type can be presented as a QW-type.

So one cannot hope to construct QW-types using a type theory which is interpretable in just ZF. However, the type theory in which we work, with its universes closed under inductive-inductive definitions, already requires going beyond ZF to be able to give it a naive, classical set-theoretic interpretation (by assuming the existence of enough strongly inaccessible cardinals, for example). So the above considerations about initial algebras for infinitary equational theories in classical set theory do not rule out the construction of QW-types in the type theory in which we work. However, something more than just quotienting a W-type is needed in order to prove Theorem 1. Figure 2 gives a first attempt to do this (which later we will modify using sized types to get around a termination problem). The definition is relative to a given signature Σ : Sig and system of equations ε = (E, V, l, r) : Syseq Σ. It makes use of quotient types, which we add to Agda via postulates, as shown in Figure 3 . 4 The REWRITE pragma makes elim R B f e (mk R x) definitionally equal to f x and is not merely a computational convenience-this is what allows function extensionality to be proved from these postulated quotient types. The POLARITY pragmas enable the postulated quotients to be used in datatype declarations at positions that Adga deems to be strictly positive; a case in point being the definitions of Q 0 and Q 1 in Figure 2 . Agda's test for strict positivity is sound with respect to a set-theoretic semantics of inductively defined datatypes that are built up using strictly positive uses of dependent functions; the semantics of such datatypes uses initial algebras for endofunctors possessing a rank. Here we mutual data Q0 : Set where sq : T Q → Q0 data Q1 : Q0 → Q0 → Set where sqeq : (e : E)(ρ : V e → Q) → Q1 (sq(T'ρ (l e))) (sq(T'ρ (r e))) sqη : (x : Q0) → Q1 (sq(η(qu x))) x sqσ : (s : S(T Q)) → Q1 (sq(σ s)) (sq(ι(S'(qu • sq) s))) are allowing the inductively defined datatypes to be built up using quotients as well, but this is semantically unproblematic, since quotienting does not increase rank. (Later we need to combine the use of POLARITY with sized types; the semantics of this has been studied for System F ω [3] , but needs to be explored further for Agda.) We build up the underlying inductive type Q 0 to be quotiented using a constructor sq that takes well-founded trees T(Q 0 /Q 1 ) of whole equivalence classes with respect to a relation Q 1 that is mutually inductively defined with Q 0 -an instance of an inductive-inductive definition [15] . The definition of Q 1 makes use of the actions on functions of the signature endofunctor S and its associated free monad T (Section 2); those actions are defined as follows:

The definition of Q 1 also uses the natural transformation ι :

Turning to the proof of Theorem 1 using the definitions in Figure 2 , the S-algebra structure (9) is easy to define without using any form of choice, because of the type of Q 0 's constructor sq. Indeed, we can just take qwintro to be qu • sq • ι : S(QW) → QW. 5 The first constructor sqeq of the data type Q 1 ensures that the quotient Q 0 /Q 1 satisfies the equations in ε, so that we get qwequ as in (10) ; and the other two constructors, sqη and sqσ make identifications that module quot where postulate ty : (11)- (13) . However, there is a problem. Given X : Set, s : S X → X and e : Sat X, for qwrec X s e we have to construct a function r : Q → X. Since Q = Q 0 /Q 1 is a quotient, we will have to use the eliminator quot.elim from Figure 3 to define r. The following is an obvious candidate definition mutual r : Q → X r = quot.elim Q 1 (λ_ → X) r 0 r 1

(where we have elided the details of the invariance proof r 1 ). The problem with this mutually recursive definition is that it is not clear to us (and certainly not to Agda) whether it gives totally defined functions: although the value of r 0 at a typical element sq t is explained in terms of the structurally smaller element t, the explanation involves r, whose definition uses the whole function r 0 rather than some application of it at a structurally smaller argument. Agda's termination checker rejects the definition. We get around this problem by using a type-based termination method, namely Agda's implementation of sized types [2] . Intuitively, this provides a type Size of "sizes" which give a constructive abstraction of features of ordinals in ZF when they are used to index sequences of sets that eventually become stationary, such as in various transfinite constructions of free algebras [20, 14] . In Agda, the type Size comes equipped with various relations and functions: given sizes i, j : Size, there is a relation i : Size< j to indicate strictly increasing size (so the type Size< j is treated as a subtype of Size); there is a successor operation ↑ : Size → Size (and also a join operation _ s _ : Size → Size → Size, but we do not need it here); and a size ∞ : Size to indicate where a sequence becomes stationary. Thus we construct the QW-type QW{Σ}{ε} as Q ∞ for a suitable size-indexed sequence of types Q : Size → Set, shown in Figure 4 .

For each size i : Size, the type Q i is a quotient Q 0 i/Q 1 i, where the constructors of the data types Q 0 i and Q 1 i take arguments of smaller sizes j : Size< i. Consequently in the following sized version of (26)

the definition of r 0 {i} involves a recursive call via r to the whole function r 0 , but at a size j which is smaller than i. So now Agda accepts that the definition of qwrec X s e as r ∞, with r as in (27), is terminating. Thus we get a function qwrec for (11) . We still have (9) , but now with qwintro = qu ∞ • sq {∞} • ι; and as before, the constructor sqeq of Q 1 in Figure 4 ensures that QW = (Q 0 ∞)/Q 1 ∞ satisfies the equations ε. With these definitions it turns out that each qwrec X s e is an S-algebra morphism up to definitional equality, so that the function qwrechom needed for (12) is straightforward to define. Finally, the function qwuniq needed for (13) can be constructed via a sequence of lemmas making use of the other two constructors of the data type Q 1 , namely sqη, which makes use of an auxiliary function for coercing between different size instances of Q 0 , and sqσ. We refer the reader to the accompanying Agda code (doi: 10.17863/CAM.48187) for the details of the construction of qwuniq. Altogether, the sized definitions in Figure 4 allow us to complete a proof of Theorem 1.

QW-types are a general form of QIT that capture many examples, including simple 1-cell complexes and non-recursive QITs [6] , non-structural QITs [26] , W-types with reductions [28] , and also infinitary QITs (e.g. unordered infinitely branching trees [5] , and ordinals [21] ). They also capture the notion of initial (and free) algebras for strictly positive equational systems [14] , analogously to how W-types capture the notion of initial (and free) algebras for strictly positive endofunctors (see Remark 2) . Using Agda to formalise our results, we have shown that it is possible to construct any QW-type, even infinitary ones, in intensional type theory satisfying UIP, using inductive-inductive definitions permitting strictly positive occurrences of quotients and sized types (see Theorem 1 and Section 4). We conclude by mentioning related work and some possible directions for future work.

Quotients of monads. In view of Remark 2, Section 4 gives a construction of initial algebras for equational systems [14] on the free monad T{Σ} generated by a signature Σ. By a suitable change of signature (see Remark 1) this extends to a construction of free algebras, rather than just initial ones. We can show that the construction works for an arbitrary strictly positive monad and not just for free ones. Given such a construction one gets a quotient monad morphism from the base monad to the quotient monad. This contravariantly induces a forgetful functor from the algebras of the latter to that of the former. Using the adjoint triangle theorem, one should be able to construct a left adjoint. This would then cover examples such as the free group over a monoid, free ring over a group, etc.

Quotient inductive-inductive types. The notion of QW-type generalises to indexed QW-types, analogously to the generalisation of W-types to Petersson-Synek trees for inductively defined indexed families of types [24, Chapter 16] , and we will consider it in subsequent work. More generally, we wonder whether our analysis of QITs using quotients, inductive-inductive and sized types can be extended to cover the notion of quotient inductive-inductive type (QIIT) [4, 19] . Dijkstra [10] studies such types in depth and in Chapter 6 of his thesis gives a construction for finitary ones in terms of countable colimits, and hence in terms of countable coproducts and quotients. One could hope to pass to the infinitary case by using sized types as we have done, provided an analogue for QIITs can be found of the monadic construction in Section 4 for our class of QITs, the QW-types. Kaposi, Kovács, and Altenkirch [19] give a specification of finitary QIITs using a domain-specific type theory called the theory of signatures and prove existence of QIITs matching this specification. It might be possible to encode their theory of signatures using QW-types (it can already be encoded as a QIIT), or to extend QW-types making this possible. This would allow infinitary QIITs.

Schemas for QITs. We have shown by example that QW-types can encode a wide range of QITs. However, we have yet to extend this to a proof of Conjecture 1 that every instance of the schema for QITs considered in Section 3 can be so encoded.

Conditional path equations. In Section 3 we mentioned the fact that Dybjer and Moeneclaey [12] give a model for finitary 1-HITs and 2-HITs in which constructors are allowed to take arguments involving the identity type of the datatype being declared. On the face of it, QW-types are not able to encode such conditional QITs. We plan to consider whether it is possible to extend the notion of QW-type to allow encoding of infinitary QITs with such conditional equations.

Homotopy Type Theory (HoTT). Our development makes use of UIP (and heterogeneous equality), which is well-known to be incompatible with the Univalence Axiom [29, Example 3.1.9]. Given the interest in HoTT, it is certainly worth investigating whether a result like Theorem 1 holds in univalent foundations for a suitably coherent version of QW-types. We are currently investigating this using set-truncation.

Pattern matching for QITs and HITs. Our reduction of QITs to inductioninduction, strictly positive quotients and sized types is of theoretical interest, but in practice one could wish for more direct support in systems like Agda, Lean and Coq for the very useful notion of quotient inductive types (or more generally, for higher inductive types). Even having better support for the special case of quotient types would be welcome. It is not hard to envisage the addition of a general schema for declaring QITs; but when it comes to defining functions on them, having to do that with eliminator forms rapidly becomes cumbersome (for example, for functions of several QIT arguments). Some extension of dependently typed pattern matching to cover equality constructors as well as element constructors is needed and the third author has begun work on that based on the approach of Cockx and Abel [9] . 6 6 In this context it is worth mentioning that the cubical features of recent versions of Agda give access to cubical type theory [30] . This allows for easy declaration of HITs and hence in particular QITs (and quotients avoiding the need for POLARITY pragmas) and a certain amount of pattern matching when it comes to defining functions on them: the value of a function on a path constructor can be specified by using generic elements of the interval type in point-level patterns; but currently the user is given little mechanised assistance to solve the definitional equality constraints on end-points of paths that are generated by this method.

Containers: Constructing strictly positive types

Type-Based Termination, Inflationary Fixed-Points, and Mixed Induct ive-Coinductive Types

Well-Founded Recursion with Copatterns and Sized Types

Quotient Inductive-Inductive Types

Type Theory in Type Theory Using Quotient Inductive Types

Higher Inductive Types in Programming

Words, Free Algebras, and Coequalizers. Fundamenta Mathematicae

Sprinkles of Extensionality for Your Vanilla Type Theory

Elaborating Dependent (Co)Pattern Matching

Quotient Inductive-Inductive Definitions

Representing Inductively Defined Sets by Wellorderings in Martin-Löf's Type Theory

Finitary Higher Inductive Types in the Groupoid Model. Electronic Notes in Theoretical Computer Science

An Equational Metalogic for Monadic Equational Systems

On the Construction of Free Algebras for Equational Systems

A Finite Axiomatisation of Inductive-Inductive Defin itions

Polynomial Functors and Polynomial Monads

All Uncountable Cardinals Can Be Singular

Extensional Concepts in Intensional Type Theory

Constructing Quotient Inductive-Inductive Types

A Unified Treatment of Transfinite Constructions for Free Algebras, Free Monoids, Colimits, Associated Sheaves, and so on

Semantics of Higher Inductive Types

Studies in Logic and the Foundations of Mathematics

Dependently Typed Functional Programs and their Proofs

Programming in Martin-Löf 's Type Theory

Brouwer's Fixed-Point Theorem in Real-Cohesive Homotopy Type Theory

Higher Inductive Types as Homotopy-Initial Algebras

Investigations into Intensional Type Theory

W-Types with Reductions and the

The Univalent Foundations Program, Homotopy Type Theory: Univalent Founda tions for Mathematics

Cubical Agda: A Dependently Typed Program ming Language with Univalence and Higher Inductive Types

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use

Acknowledgement We would like to acknowledge the contribution Ian Orton made to the initial development of the work described here. He and the first author supervised the third author's Master's dissertation Quotient Inductive Types: A Schema, Encoding and Interpretation, in which the notion of QW-type (there called a W + -type) was introduced.