{'fraction_non_alphanumeric': 0.04126658985191824, 'fraction_numerical': 0.004992958648060428, 'mean_word_length': 4.177529827662395, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Large and Infinitary Quotient Inductive-Inductive Types

Quotient inductive-inductive types (QIITs) are generalized inductive types which allow sorts to be indexed over previously declared sorts, and allow usage of equality constructors. QIITs are especially useful for algebraic descriptions of type theories and constructive definitions of real, ordinal and surreal numbers. We develop new metatheory for large QIITs, large elimination, recursive equations and infinitary constructors. As in prior work, we describe QIITs using a type theory where each context represents a QIIT signature. However, in our case the theory of signatures can also describe its own signature, modulo universe sizes. We bootstrap the model theory of signatures using self-description and a Church-coded notion of signature, without using complicated raw syntax or assuming an existing internal QIIT of signatures. We give semantics to described QIITs by modeling each signature as a finitely complete CwF (category with families) of algebras. Compared to the case of finitary QIITs, we additionally need to show invariance under algebra isomorphisms in the semantics. We do this by modeling signature types as isofibrations. Finally, we show by a term model construction that every QIIT is constructible from the syntax of the theory of signatures.


Introduction
The aim of this work is to provide theoretical underpinning to a general notion of inductive types, called quotient inductive-inductive types (QIITs). QIITs are of interest because there are many commonly used mathematical structures, which can be conveniently described as QIITs in type theory, but cannot be defined as less general inductive types, or doing so incurs large encoding overhead.
Categories are a prime example for a structure which is described by a quotient inductive-inductive signature. Signatures for QIITs allow having multiple sorts, with later ones indexed over previous ones, and equations as well. We need both features in order to write down the following signature of categories.

id
: The benefit of having a QII signature is getting a model theory "for free", from the metatheory of QIITs. This model theory includes a category of algebras which has an initial object and also some additional structure. For the signature of categories, we get the empty category as the initial object, but it is common to consider categories with more structure, which have more interesting initial models.
Algebraic notions of models of type theories are examples for this. Here, initial models represent syntax, and initiality corresponds to induction on syntax. Several variants have been used, from contextual categories [1] and comprehension categories [2] to categories with families [3] (CwF).
A prime motivation of the current work is to further develop QIITs as a framework for the metatheory of type theories, to cover more theories and support more applications. To this end, we extend the syntax and semantics of QIITs as previously described in the literature [4,5,6], with the following features.
1. Large constructors, large elimination and algebras at different universe levels. This fills in an important formal gap; large models are routinely used in the metatheory of type theories, but they have not been presented explicitly in previous QIIT literature. For example, interpreting syntactic contexts as sets already requires a notion of large models.
To provide semantics, we show that for each signature, there is a CwF (category with families) of algebras, extended with Σ-types, extensional identity, and constant families. This additional structure corresponds to a type-theoretic flavor of finite limits, as it was shown in [13] that the category of such CwFs is biequivalent to the category of finitely complete categories.
Compared to the case of finitary QIITs, the addition of infinitary constructors and recursive equations requires a significant change in semantics: instead of strict CwF morphisms, we need to consider weak ones, and instead of modeling types as displayed CwFs, we need to model them as CwF isofibrations. The latter amounts to showing that signature extension respects algebra isomorphisms.
We also show, by a term model construction, that all QIITs are reducible to the syntax of signatures. This construction also essentially relies on invariance under isomorphisms.

Outline of the Paper
In Section 2, we describe the metatheory used in the rest of the paper. In Section 3, we introduce the theory of QIIT signatures. In Section 4 we give categorical semantics to signatures. In Section 5 we build model theory for the theory of QIIT signatures. In Section 6 we give a term model construction of QIITs. We discuss related work and conclude in Sections 7-8.

Metatheory
The metatheory used in this paper is extensional type theory, extended with a form of cumulativity and an external notion of universe polymorphism. We refer to this theory as cETT. We review the used features and notations in the following.

Core Extensional Theory
We have Russell-style predicative universes Set i indexed by natural numbers, dependent functions as (x : A) → B, and dependent pairs as (x : A) × B. We sometimes leave parameters implicit in dependent function types, e.g. write id : A → A instead of id : (A : Set i ) → A → A. We also use subscripts as a field projection notation for iterated pairs. For example, for t : (A : Set i ) × (B : Set i )×(f : A → B), we use B t to denote the projection of the second component. Sometimes we omit the subscript if it is clear from context. When we write "exists" in this paper, we always mean chosen structure given by a Σ-type.
Both for function types and Σ, the output universe level is given as the maximum of the levels of the constituent types, e.g. (x : A) → B : Set max(i,j) when A : Set i and B : Set j .
We write propositional equality as t = u, with refl t for reflexivity. We have equality reflection and uniqueness of identity proofs (UIP). The unit type is ⊤ : Set 0 , with inhabitant tt.

Cumulativity
We use cumulative universes and cumulative subtyping as described in [14]. Concretely, we have a -≤ -subtyping relation on types, specified by the following rules: Additionally, we have an internal Subtype type, which internalizes subtyping, analogously to how -= -internalizes definitional equality. Hence, we have analogous reflection and uniqueness rules.
We use cumulativity to reduce bureaucratic overhead when dealing with constructions at different universe levels. The internal Subtype is used in Section 6 to prove cumulativity for general QIIT algebras. For example, consider natural number algebras at level i, given as the Σ-type NatAlg i := (Nat : Set i ) × Nat × (Nat → Nat). It follows from the subtyping rules that i ≤ j implies N atAlg i ≤ NatAlg j . However, cumulativity for arbitrary QIIT algebras does not follow judgmentally; it can only be proven by induction on signatures, hence the need for Subtype.
Internal subtyping is not included in [14], but it can be justified by the set-theoretic model given there.

Universe Polymorphism
We need to talk about constructions at arbitrary universe levels. For the sake of simplicity, we do not assume a notion of universe polymorphism in cETT, instead we quantify over levels in an unspecified theory outside of cETT. Hence, a universe polymorphic cETT term is understood as a N-indexed family of cETT terms. We reuse the notation of cETT functions for universe polymorphism, e.g. as in the following function:

QIIT Signatures
Signatures are given as contexts in a certain type theory, the theory of signatures. We shall abbreviate it as ToS. However, ToS turns out to be a large infinitary QIIT itself, and we would like to define ToS and a notion of signature without referring to QIITs, only using features present in cETT.
In previous works by Cartmell [1] and Sterling [15], signatures for generalized algebraic theories are defined using raw syntax together with well-formedness relations. In this way, signatures can be specified without already assuming the existence of GATs or QIITs. However, raw syntax is notoriously difficult to work with, and we prefer to avoid it altogether.
At this point, we do not actually need syntactic signatures, which make it possible to do induction on signatures. We only need a way to write down well-formed signatures, and interpret them in arbitrary models of ToS. For this, a weak Church-like encoding suffices, where a signature is given as a typing context in an arbitrary model of ToS. For this, we first need to specify the notion of ToS models. However, this is the only piece of information about ToS which we need to manually provide. Other concepts such as homomorphisms of ToS models and ToS-induction, will be derived from the semantics of signatures and self-description in Section 5.
Definition 1 (Notion of model for the theory of signatures). For levels i and j, ToS i,j : Set max(i+1, j+1) is a cETT type whose elements are ToS models (or ToS-algebras). ToS i,j is an iterated Σ-type, containing all of the following components.
A category with families (CwF), where all four underlying sets (of objects, morphisms, types and terms) are in Set i . Following notation in [4], we denote these respectively as Con : Set i , Sub : Con → Con → Set i , Ty : Con → Set i and Tm : (Γ : Con) → Ty Γ → Set i . We use id and -• -to denote identity and composition for substitution. We denote the empty context as • : Con, and the unique substitution into the empty context as ǫ : Sub Γ •. Context extension is -⊲ -: (Γ : Con) → Ty Γ → Con. Substitution on types and terms is written as - [-]. Projections are noted as p : Sub (Γ ⊲ A) Γ and q : Tm (Γ ⊲ A) (A[p]), and substitution extension is -, -: (σ : A universe U : Ty Γ with decoding El : (a : Tm Γ U) → Ty Γ. Inductive function space Π : (a : Tm Γ U) → Ty (Γ ⊲ El a) → Ty Γ, with application as app : Tm Γ (Π a B) → Tm (Γ ⊲ El a) B and its inverse lam.
External function space Π ext : (A : ) and its inverse lam ext .
In the above listing, we omit equations for substitution and βη-conversion, but these should be understood to be also part of ToS i,j .
Notational conventions. We name elements of Con as Γ, ∆, Θ, elements of Sub Γ ∆ as σ, δ, ν, elements of Ty Γ as A, B, C, and elements of Tm Γ A as t, u, v. CwF components by default support de Bruijn indices, which are not easily readable. We use instead a nameful notation for binders in context extension, Π and lam, e.g. as (• ⊲ (a : U) ⊲ (t : El a)). We also define a type-theoretic flavor of app for convenience: We abbreviate non-dependent inductive Π as -⇒ -, and likewise we use -⇒ ext -and -⇒ inf -for non-dependent external and infinitary functions.
Definition 2 (Notion of signature). A QIIT signature at level j is a context in an arbitrary M : ToS i,j model. We define the type of such signatures as follows: Here, j refers to the level of external types appearing in the signature, in the domains of Π ext and Π inf functions, while the quantified i level is required to allow interpreting a signature in arbitrary-sized ToS models. Note that Sig j is universe-polymorphic, so it is a family of cETT types and it is not in any cETT universe. With this, we are able to specify QIITs, and we can also interpret each signature in an arbitrary ToS model, by applying a signature to a model. Sig j can be viewed as a precursor to a Church-encoding for the theory of signatures, but we only need contexts encoded in this way, and not other ToS components. In functional programming, this representation is sometimes called "finally tagless" [16], and it is used for defining and interpreting embedded languages.
In the following examples, we leave the abstracted M : ToS i,j implicit. Example 2. Infinitary constructors. The universe U is closed under the Π inf function type, which allows such functions to appear in the domains of Π types. This allows, for example, a signature for trees branching with arbitrary small types. This is a signature at level 1, since we have Set 0 as a Π ext domain type. Example 3. Recursive equations. Again, the universe is closed under Id, which allows us to write equations in Π domains. A minimal (and trivial) example: More interesting (and complicated) examples for recursive equations are boundary conditions in various cubical type theories [10,11,12]. Note that our Id allows iterated equations as well, but these are all trivial in the semantics, where we assume UIP.
Remark. Since signatures are parametrized by a single universe level, all external types in constructors must be contained in the same Set j universe. We opted for this setup for the sake of simplicity. Cumulativity helps here: it allows us to pick a j level which is large enough to accommodate all external types in a signature.

Overview
For each signature, we would like to have at least 1. A category of algebras, with homomorphisms as morphisms.
2. A notion of induction, which requires a notion of dependent algebras. 3. A proof that for algebras, initiality is equivalent to supporting induction.
Following [4], we do this by creating a model of ToS, where contexts are categories supporting the above requirements and substitutions are appropriate structure-preserving functors. Then, each signature can be applied to this model, yielding an interpretation of the signature as a structured category of algebras.
Our semantics has a "type-theoretic" flavor, which is inspired by the cubical set model of Martin-Löf type theory by Bezem et al. [17]. The core idea is to avoid strictness issues by starting from basic ingredients which are already strict enough. Hence, instead of modeling types as certain slices and substitution by pullback, we model types as displayed categories with extra structure, which naturally support strict reindexing.
We make a similar choice in the interpretation of signatures themselves: we use structured CwFs instead of lex categories. The reason here is that CwFs allow us to compute induction principles in strictly the same way as one would write in type theory, since we have Ty and Tm for a primitive notion of dependent objects and morphisms. In contrast, dependent objects in lex categories is a derived notion, and the induction principles we get are only up to isomorphism. This issue is perhaps not relevant from a purely categorical perspective, but we are concerned with eventually implementing QIITs in proof assistants, so we prefer if our semantics computes strictly. This was demonstrated previously in [18], where we provided a program which computed types of induction principles from signatures of higher inductive-inductive types, and we believe that the same could be achieved for the signatures and semantics described in this paper.
In the following, for given i and j levels, we define a model M i,j : ToS max(i+1,j)+1,j such that Con M i,j is a type of structured categories (of algebras). The level i marks the level of all internal sorts in an algebra, and the level j marks the level of all external sets in function domains. Hence, every algebra has level max(i + 1, j). The bump is only needed for i, since algebras merely contain elements of A : Set j types, while inductive sets are themselves elements of Set i . For example, NatAlg i : We present the components of the model in order. In the following, we use bold font to disambiguate components of M i,j from components of other structures. For example, we use σ : Sub Γ ∆ to denote a substitution in M i,j .
The model involves a large amount of technical detail; we omit a significant part of this, and only present the most salient parts.

Contexts
We define Con : Set max(i+1,j)+1 as flCwF max(i+1,j) . 4. Constant families. This includes a type former K : Con → Ty Γ, where Γ is implicitly quantified, together with lam K : Sub Γ ∆ → Tm Γ (K ∆) and its inverse app K . The idea is that K ∆ is a representation of ∆ as a type in any context. Clairambault and Dybjer called constant families "democracy" in [13].
We abbreviate the additional structure on CwFs consisting of Σ, Id and K as fl-structure.
Definition 4 (Notion of induction in an flCwF). Given Γ : flCwF i , we have the following predicate on contexts: For an example, if we interpret NatSig in the M model, we get an flCwF of natural number algebras, where Con is the type of algebras and Sub Γ ∆ is the type of homomorphisms between Γ and ∆ algebras. Ty is the type of displayed algebras, and Tm is the type of their sections: Thus, for natural number algebras, Inductive is exactly the predicate which holds when an algebra supports induction.

Con Γ supports induction if and only if it is initial. Moreover, induction and initiality are both proof-irrelevant predicates.
The reason for the "finite limit CwF" naming is the following: Clairambault and Dybjer showed that the 2-category of flCwFs is biequivalent to the 2-category of finitely complete categories [13]. In particular, in an flCwF the categorical product of Γ and ∆ can be given as Γ ⊲ K ∆, and the equalizer of σ and δ as Γ ⊲ Id (K ∆) (lam K σ) (lam K δ). While showing equivalence of initiality and induction does not need all flCwF components (e.g. Σ is not needed), we build the full flCwF semantics in order to connect to Clairambault's and Dybjer's results.
In order to talk about weak structure-preservation in the interpretation of substitutions, we need to specify isomorphisms for contexts and types.
Definition 6 (Type categories, c.f. [13]). For each Γ : Con, there is a category whose objects are types A : Ty Γ, and morphisms from A to B are terms t : ). Identity morphisms are given by q : Tm (Γ ⊲ A) (A[p]), and composition t • u by t[p, u]. The assignment of type categories to contexts extends to a split indexed category. For each σ : Sub Γ ∆, there is a functor from Ty ∆ to Ty Γ, which sends A to A[σ] and t : Definition 7. A type isomorphism, notated t : A ≃ B is an isomorphism in a type category. We note the inverse as t −1 .

Substitutions
A weak flCwF morphism σ : Sub Γ ∆ is a functor between underlying categories, which also maps types to types and terms to terms, and satisfies the following mere properties: In short, σ preserves substitution strictly and preserves empty context and context extension up to isomorphism. We notate the evident isomorphisms as Our notion of weak morphism is the same as in [19], when restricted to CwFs.
Note that the definition we just gave lives in Set max(i+1,j) , but by cumulativity it is also in Set max(i+1,j)+1 , as required by our M i,j : ToS max(i+1,j)+1,j specification of the model being defined.
These are all natural in the following sense: for σ : , and similarly for σ K and σ Id .
Moreover, σ preserves all term and substitution formers in the fl-structure.
Proof. For σ Σ , we construct the following context isomorphism: This isomorphism is the identity on σ Γ, hence we can extract the desired σ Σ : from it. For σ K , note the following: This yields a type isomorphism σ (K ∆) ≃ K (σ ∆) in the empty context, and we use the functorial action of ǫ : Sub Γ • to weaken it to any Γ context.
For σ Id , both component morphisms can be constructed by refl and equality reflection, and the morphisms are inverses by UIP. We omit here the verification of naturality and that σ preserves term and substitution formers in the flstructure.

Identity and Composition
id : Sub Γ Γ is defined in the obvious way, with identities for underlying functions and for preservation morphisms.
For σ • δ, the underlying functions are given by function composition, and the preservation morphisms are given as follows: It is easy to verify the left and right identity laws and associativity for -• -.
Lemma 1. The derived preservation isomorphisms for the fl-structure can be decomposed analogously; all derived isomorphisms in id are identities, and we have On the right sides, -• -refers to composition of type morphisms.
Proof. In the case of Id, the equations hold immediately by UIP. For Σ and K, we prove by flCwF computation and straightforward unfolding of definitions.

Empty Context
The empty context • : Con is the terminal flCwF, which has all underlying sets defined as ⊤ (or constantly ⊤), with an evident unique ǫ : Sub Γ •. Since ǫ is a strict flCwF morphism, ǫ −1 • and ǫ −1 ⊲ are both identity morphisms.

Types
We define Ty Γ : Set max(i+1,j)+1 as the type of split flCwF-isofibrations over Γ, at level max(i + 1, j). We extend Ahrens' and Lumsdaine's displayed categories and their definition of isofibrations [20]. We first define displayed flCwFs, then specify iso-cleaving as additional structure on top of that.
Definition 8 (Displayed flCwF). The type of displayed flCwFs at level i is given as the logical predicate interpretation (see e.g. [21] or [18]) of flCwF i . For each flCwF component in Γ, there is a component in a displayed flCwF which "lies over" it.
Notation. In situations where we need to refer to both "base" and displayed things, we give underlined names to contexts, substitutions, types and terms in a base flCwF. For example, we may have Γ : Con Γ living in Γ : Con, and Γ : Con A Γ living in a displayed flCwF over Γ. We only use underlining on cETT variable names, and overload flCwF component names for displayed counterparts. For example, a Con component is named the same in a base flCwF and a displayed one.
Concretely, a displayed flCwF A over Γ has the following underlying sets, which we call displayed contexts, substitutions, types and terms respectively.
Above, we implicitly quantify over Γ, ∆ and A base parameters. We also have the following components for empty context, context extension and substitution. We omit listing other components here.
In the following we will often omit Γ and A subscripts on components; for example, in the type Con A •, the • is clearly a base component in Γ.
We also need displayed counterparts to the previously defined derived notions on flCwFs; these are again given as logical predicate interpretations of the nondisplayed definitions.
Definition 9 (Displayed type categories). For each Γ : Con A Γ, there is a displayed category over the type category Ty Γ Γ, whose objects over A : Ty Γ Γ are elements of Ty A Γ A, and displayed morphisms over t : The identity morphism is given by q A , and the composition of t and u is t[p A , u]. Analogously to Definition 6, this extends to a displayed split indexed category.

Definition 10 (Displayed isomorphisms). A displayed context isomorphism
is an isomorphism in a displayed type category.
Definition 11. A vertical morphism lies over an identity morphism. We use this definition for context morphisms (substitutions) and type morphisms as well.
In contrast to [4], it is not sufficient to model types as displayed flCwFs. In ibid. the universe U in ToS was empty, and all substitutions were "neutral", i.e. semantic subsitutions were functors which may permute, duplicate or forget components of algebras, or freely reinterpret components, and it is easy to see that all such functors strictly preserve limits. In contrast, the current U is not empty: it is closed under identity and infinitary function types. Hence, substitutions and terms are not neutral anymore, as they can contain canonical type codes in U. Semantically, these canonical type codes do not merely reshuffle structure, hence they preserve limits only weakly. We will return to this in Section 4.15. We are forced to use a weaker semantics where fl-structure is not preserved strictly, and we also need to add additional structure to displayed flCwFs which expresses preservation of base isomorphisms.
Definition 12 (Context iso-cleaving). This lifts a base context isomorphism to a displayed one. It consists of Here, coe and coh abbreviate "coercion" and "coherence" respectively.
Definition 13 (Type iso-cleaving). This consists of Definition 14. A split flCwF isofibration is a displayed flCwF equipped with iso-cleaving for contexts and types.

Remark.
It is not possible to model types as fibrations or opfibrations, because we have no restriction on the variance of ToS types. For example, the type which extends a pointed set to a natural number signature, is neither a fibration nor an opfibration.

Type Substitution
We aim to define - . The underlying sets are given by simple composition: and likewise components for substitution are given by corresponding components in A. Context and type formers are given by coercing A structures along σ preservation isomorphisms. For example: Term and substitution formers are given by composing coh-lifted isomorphisms with term and substitution formers from A. For example:

Equations for term and type substitution follow from naturality of preservation isomorphisms in σ, coe[], coh[] and substitution equations in A.
Iso-cleaving is given by iso-cleaving in A and the action of σ on isomorphisms, e.g. we have coe A[σ] σ Γ := coe A (σ σ) Γ.

Terms
Tm Γ A : Set max(i+1,j)+1 is defined as the type of weak flCwF sections of A. The underlying functions of t : Tm Γ A are as follows: 3. The unique map ǫ A : Sub (t •) • id has a vertical retraction. 4. Each (t p, t q) : Sub (t (Γ ⊲ A)) (t Γ ⊲ t A) id has a vertical inverse.
Similarly to Section 4.3, we denote the evident preservation isomorphisms as t • : t • ≃ id • and t ⊲ : t (Γ ⊲ A) ≃ id t Γ ⊲ t A. In short, weak section is a dependently typed analogue of weak morphism, with dependent underlying functions and displayed preservation isomorphisms. We also have the derived fl-preservation isomorphisms.
Theorem 3. A weak section t : Tm Γ A preserves fl-structure up to vertical type isomorphisms, that is, the following are derivable: Also, the above isomorphisms are natural in the sense of Theorem 2, and t preserves type and substitution formers in the fl-structure.
Proof. The construction of isomorphisms is the same as in Theorem 2. Indeed, every construction there has a displayed counterpart which we can use here.
We note though that the move from Theorem 2 to here is not simply a logical predicate translation, because we are only lifting the codomain of a weak morphism to a displayed version, and we leave the domain non-displayed. We leave to future work the investigation of such asymmetrical (or "modal") logical predicate translations.

Term Substitution
We also have the same decomposition of derived isomorphisms as in Lemma 1. We do not have to show functoriality of term substitution here, since that is derivable in any CwF, see e.g. [4].

Context Extension and Comprehension
Γ ⊲ A : Con is defined as the total flCwF of A. This is given by bundling together all displayed flCwF components in A with corresponding base components in Γ, using the metatheoretic Σ-type. It is a straightforward extension of total categories in [20]. p : Sub (Γ ⊲ A) Γ is a strict morphism given by taking a first projection for each component. q : is likewise a strict flCwF section given by second projections. Substitution extension σ, t is given by pointwise combining σ and t with metatheoretic Σ pairing, e.g. Con (σ,t) Γ := (σ Γ, t Γ). We define U : Ty Γ as the isofibration which is constantly Set i . A constant isofibration does not actually depend on the base flCwF, and has trivial isocleaving where coe-s are identity functions. Hence, we have Con U Γ := Set i and Sub U Γ ∆ σ := Γ → ∆.

Universe
Remark. The type Tm Γ U is strictly equal to Sub Γ Set i , so it is helpful to think about semantic elements of the universe as weak morphisms from Γ to Set i .

Elements of the Universe
We define El : Tm Γ U → Ty Γ as discrete isofibration formation. For a : Tm Γ U, the underlying sets of El a are the following: Hence, in El a, Sub and Tm are propositional. We use the isomorphisms a • : a • ≃ ⊤ and a ⊲ : a (Γ ⊲ A) ≃ (Γ : a Γ) × (a A Γ) to define empty context and context extension: We likewise use preservation isomorphisms to define K, Id and Σ. Context coercion is coe σ Γ := a σ Γ. Type coercion, for A : a A Γ is given as coe t A := a t (a −1 ⊲ (Γ, A)).

Inductive Function Space
For a : Tm Γ U and B : Ty (Γ ⊲ El a), we aim to define Π a B : Ty Γ. We define this as a dependent product of isofibrations, indexed by a discrete domain. The discreteness is essential: with a general A : Ty Γ domain, Π would not be definable because of variance issues. Indeed, the category of categories is not locally cartesian closed and does not support a general Π type [22,Section A1.5].
Contexts are products of B-contexts, and types are products of B-types, indexed respectively by contexts and types of El a.
Note that since B is over the total (Γ ⊲ El a), Con B has a Σ-typed argument, and likewise the last argument of every B component. We could define substitutions similarly, as products of substitutions: This would work, but we know that Sub (El a) γ δ σ is defined as a σ γ = δ, so we can eliminate σ by singleton contraction, and use the following equivalent definition: The benefit of the contracted definition is that it computes preservation laws in algebra homomorphisms strictly as expected, while the non-contracted definition computes homomorphisms as functional logical relations.
Terms are also given as a singleton-contracted version of products of terms. In Π a B, all other structure is given pointwise by B-structure.
Iso-cleaving is given by transporting indices backwards in El a and outputs forwards in B: Likewise, coh-s are given by backwards-forwards coh-s. app : Tm Γ (Π a B) → Tm (Γ ⊲ El a) B can be defined as currying of the underlying functions, and lam as uncurrying.

External Function Space
For A : Set j and B : A → Ty Γ, we define Π ext A B : Ty Γ as the A-indexed direct product of B. Since the indexing is given by a metatheoretic function, every component is given in the evident pointwise way.

Infinitary Function Space
For A : Set j and b : A → Tm Γ U, we aim to define Π inf A b : Tm Γ U. The underlying functions are: The preservation morphisms are as follows. Note that • U = ⊤ and ⊲ U is metatheoretic Σ.
The preservation of • and -⊲ -here is in fact the main point of divergence from [4]. In ibid., substitutions and terms are modeled as strict morphisms and types as displayed CwFs (with no iso-cleaving). However, it is not the case that (Π inf A b) • = ⊤, which is the statement of strict •-preservation. The left side reduces to (a : A) → b a •, which is isomorphic to ⊤ but not strictly equal to it. Likewise for ⊲-preservation.
Hence, we are forced to interpret terms as weak sections, which in turn forces us to interpret types as isofibrations, since type substitution requires iso-cleaving.

Identity
For t and u in Tm Γ (El a), we define Id t u : Tm Γ U as expressing pointwise equality of weak sections.
Above, t A = u A is well-typed because of e : t Γ = u Γ. For substitutions, we have to complete a square of equalities: This can be given by t σ : a σ (t Γ) = t ∆ and u σ : a σ (u Γ) = u ∆. The action on terms is analogous. We omit preservation morphisms here as they are straightforward. Like Π inf , Id also does not support strict preservation of • and ⊲. Equality reflection and refl : Id t t are also evident.
With this, we have defined the M i,j : ToS max(i+1,j)+1,j model that we set out to define in Section 4.1.

Model Theory of the Theory of Signatures
At this point, we only have a notion of algebra for ToS, from Definition 1. In the following sections, we would also like to talk about initial ToS-algebras and ToS-induction. We get these notions by giving a QIIT signature for ToS, and interpreting it in the M model from the previous section.
Definition 16 (Signature for ToS). For each level j, we define ToSSig j : Sig j+i , as the signature for the theory of signatures with external sets in Set j . This is a large and infinitary QIIT signature, as we have Π ext and Π inf abstracting over A : Set j and branching with A → Ty Γ and A → Tm Γ U respectively. We present an excerpt from ToSSig j below. ...
... Now, for each i, the interpretation of ToSSig j in M i,j+1 yields an flCwF Γ such that Con Γ = ToS i,j . In short, we can recover ToS algebras from the semantics of ToSSig. This follows by computation of the interpretation and the fact that ToSSig is precisely the internal representation of ToS. Hence, we have self-description modulo the bumping of the j level. Also, as we get an flCwF of ToS i,j -algebras, we can use Definition 4 for the notion of ToS-induction.
Remark. By the definition of • and -⊲ -, the types of algebras computed by M are always left-nested iterated Σ-types which start with ⊤. Hence, we need to require that Definition 1 is similarly left-nested and starts with ⊤, in order to make the match strict.

Term Models of QIITs
In this section we construct QIITs from initial ToS-algebras. For this, we need to assume the existence of such algebras. Assumption. For each level j and k such that j + 1 ≤ k, we assume the existence of syn j : ToS j+1,j , and we assume that syn j , considered as an element of ToS k,j by Lemma 2, is inductive in the sense of Definition 4.

Assuming Syntax for the Theory of Signatures
We explain this assumption. The syntax for the theory of signatures is postulated at the lowest possible level ToS j+1,j . This is the lowest because signatures may contain A : Set j types, and since we want to view the syntax as freely generated, its inductive sorts must be large enough to contain the A types. Otherwise we would run into Russell's paradox. Then, the induction assumption says that we have induction at all levels larger than j + 1.
Example 4. We have syn 0 : ToS 1,0 , which is the syntax of closed QIIT signatures. We want to define a function length : Con syn 0 → N by induction, which returns the length of a syntactic context as a metatheoretic natural number. To this end, we define a displayed ToS over syn 0 , where Con is defined as constantly N, every other sort is defined as constantly ⊤, • is defined as 0 and Γ ⊲ A is defined as Γ + 1. By the induction assumption, we get a ToS-section from syn 0 to the displayed model, whose action on contexts is exactly the length function. Note that the induction assumption requires that the displayed model is at least at level 1, but this is not problematic because by cumulativity N : Set 1 .
For every M : ToS j+1,j , there is a unique strict ToS-morphism from syn j to M . This follows from the induction assumption on syn j and Theorem 1. We denote this morphism as -M . For example, given Γ : Con syn , we have Γ M : Con M . Also, for every displayed ToS-model M over syn j , there is a strict ToS-section of M . We also denote this as -M , so e.g. for Γ : Con syn we have Γ M : Con M Γ.
With syn at hand, we can use an alternative, more conventional representation of signatures.
Definition 17. We define SynSig j : Set j+1 , the type of syntactic signatures at j, as Con syn j .
We can convert a signature to a syntactic one by interpreting it in syn j , and we can convert in the other direction by using ToS-induction to interpret a Γ : Con syn j in an arbitrary ToS model. This is merely a logical equivalence, external to cETT (because of universe polymorphism), and not an isomorphism.

Useful Model Fragments of M
In the following, we will need three model fragments of M, which can be used to compute notions of algebras, displayed algebras and sections respectively for each syntactic signature. This is a rephrasing of the -A , -D and -S interpretations in [4], where they are discussed at more length.
Definition 18 (The Set model of ToS). For each i and j, we have A : ToS max(i+1,j)+1,j , which can be given by restricting the M i,j model of Section 4 so that we only have the first Con components in the interpretations for contexts, substitutions, types, terms, and we only have actions on contexts in the interpretations of term and substitution formers. Hence, we have: Now, for some Γ : Con syn j , the type of Γ-algebras at level i is given by Γ A , where we implicitly lift syn j : ToS j+1,j to ToS max(i+1,j)+1,j . E.g. NatSig A yields a left-nested Σ-type of pointed sets with an endofunction. Also, Γ M extends Γ A to an flCwF of Γ-algebras, and Γ A = Con Γ M .
For Γ : SynSig j , the type of displayed Γ-algebras at level i over some γ : Γ A is given by Γ D γ. Here, we also implicitly lift Γ to live in the appropriately sized syn. In other words, Γ D yields the notion of types in the flCwF of Γ-algebras given by Γ M , so we have Γ D = Ty Γ M .
Definition 20 (Displayed algebra section model of ToS). Analogously to A and D, for each i and j levels we define S as a displayed ToS model over the total model of D, which is given by restricting M i,j to the Tm components, corresponding to interpretations of terms and actions on terms.
For γ : Γ A and γ : Γ D γ, the type of Γ-sections at level i is computed as Γ S γ γ, and we have Γ S = Tm Γ M .

Term Algebras
The basic idea is that initial algebras can be built from the terms of syn j . For example, consider the syntactic signature for natural numbers: The type Tm syn NatSig (El syn N ) is isomorphic to the usual type of natural numbers, since, intuitively, such terms can only be built from iterated usage of zero and suc. We build a term algebra for each signature in this manner.
Definition 21 (Term algebra construction). For each syntactic signature Ω : SynSig j , we define a displayed ToS model over syn j , named T Ω . The underlying sets are as follows: Above, the ≃ in the definition of Sub T Ω is a context isomorphism in ∆ M , which is the flCwF of ∆-algebras. The ≃ id in Ty TΩ is a vertical context isomorphism in the displayed flCwF given by A M .
So far, the underlying sets in T Ω are similar to what was given in [4] in the construction of term algebras, but there is an important difference: in ibid. strict equalities are used instead of isomorphisms. In our case, isomorphisms are necessary once again because of infinitary functions types and our identity type; we shall see this shortly. The universe is interpreted as follows: Hence, a syntactic t : Tm Ω U is interpreted as a set of terms with type El t. In the interpretation of El, note that The ≃ id above is just an isomorphism of sets, since it lives in U M which was given as the flCwF of sets in Section 4.11. This above isomorphism is a good summary of the construction: the interpretation of a a : Tm Ω U in the term algebra is isomorphic to a set of terms. Inductive functions are interpreted by transport along such isomorphism: For the infinitary function space, we need the following, where ≃ id is again set isomorphism.
This can be given using the natural isomorphism consisting of app inf and lam inf . However, the sides are not strictly equal. For the identity type, we build the following isomorphism using equality reflection.
We omit the rest of the definition of T Ω . The interpretations of equations in the CwF and the type formers are fairly technical, and we also need to utilize iso-cleaving to interpret type substitution and substitution laws. However, the basic shape of the model remains similar to [4]. Now, we can build the term algebra for Ω by taking Ω T Ω id, which has type Ω A .
Remark. If we start with a syntactic signature at level j, then the underlying sets in the term algebra are all in Set j+1 . Hence, the term algebra for NatSig : SynSig 0 has an underlying set in Set 1 . This is a bit inconvenient, since normally we would have natural numbers in Set 0 . Our current term model construction cannot avoid this level bump, since syn j is necessarily large, and we do not have a way to construct a small set from a large set of terms. Perhaps this would be possible with a resizing rule [23]. Also, if we only consider closed finitary QIITs, with no possibility of referring to external types in signatures, then we can modify the current term model construction so that we always build sets in Set 0 . This would cover natural numbers and most dependent type theories.

Cumulativity of Algebras
We would like to show that term algebras are initial, but we want to do this on all universe levels, i.e. that term algebras are initial when lifted to any higher level. This requires showing that QII algebras are cumulative. We do this by induction on syntactic signatures.
Definition 22 (Cumulativity model). We assume j, k and l levels such that j + 1 ≤ k, j + 1 ≤ l and k ≤ l. We define a displayed model over syn j : ToS j+1,j lifted to ToS l,j . In the following, we notate the level of algebras computed by -A with an extra index, as in Γ A k . The underlying sets of the model are as follows.
The rest of the model is straightforward to define. Now, it follows from the induction assumption for syn and the reflection rule for Subtype in Section 2.2, that Γ A k ≤ Γ A l .

Term Algebras Support Induction
Definition 23. We assume j and k such that j + 1 ≤ k, and we also assume Ω : SynSig j and γ : Ω D k ( Ω T Ω id). Hence, γ is a displayed Ω-algebra over the term algebra, at level k. We are using the cumulativity of Ω here to lift the term algebra appropriately. We aim to show that γ has a section. We define a displayed model over syn j lifted to ToS k,j , which we name I Ω . The underlying sets are: Here, there is no essential change compared to [4], and we follow ibid. in the definition of I Ω . The reason is that although we have weakened strict algebra equality to isomorphism, in the current construction we only have to show equalities of substitutions and terms, which we do not need to weaken (and they cannot be sensibly weakened anyway).
Theorem 4 (Initiality of term algebras). For each j and k such that j + 1 ≤ k, and Ω : SynSig j , the term algebra given by Ω T Ω id is initial at level k.
Proof. For each γ : Ω D k ( Ω T Ω id), we have Ω I Ω id : Γ S ( Ω T Ω id) γ. Hence, term algebras are inductive in the sense of Definition 4, and by Theorem 1 they are also initial.

Related Work
Cartmell [1] defines generalized algebraic theories (GATs) using type-theoretic syntax. Compared to our QII signatures, he supports infinite signatures and sort equations but does not cover infinitary constructors or recursive equations. A way to encode sort equations in our system is using isomorphisms instead of equalities. In contrast to our algebraic definition, Cartmell's signatures are given by presyntax, named variables and typing relations, there is no explicit model theory provided for signatures, and no explicit term model construction is given. Cartmell focuses instead on showing that contextual categories serve as classifying categories for GATs.
A more semantic approach to QIITs is given by Altenkirch et al. [5]. They generalize the initial algebra semantics of inductive types to QIITs by considering towers of functors and building complete categories of algebras from them. Their notion of signature does not enforce strict positivity, hence describes a larger class of QII signatures. They show equivalence of initiality and induction, but the lack of a positivity restriction prevents construction of initial algebras.
The work of Kaposi et al. [4] is the direct precursor of our work. They do not consider infinitary constructors or constructors with recursive equations, which makes their semantics considerably simpler. They also do not provide a model theory of signatures, instead they assume signatures as an ad-hoc QIIT.
Higher inductive types (HITs) are generalizations of QIITs in settings with proof-relevant identity types. They were introduced before QIITs [7]. [18] describes a syntax for higher inductive-inductive types using a theory of signatures similar to ours, but it does not construct categories of algebras and initial algebras. Semantics for different subclasses of HITs are given by [8,24,25,26,27]. Cubical type theories were shown to support some HITs in a computational way [28,29].
Our notion of displayed CwF is an extension of displayed categories [20], although in a setting with UIP.

Conclusions and Further Work
An important motivation of the current work was to use QIITs as a framework for algebraic theories, with the metatheory of type theories in mind as a key application. We would prefer QIITs to • Be formally precise.
• Not gloss over issues of size.
• Be rich enough to cover most type theories in the wild, including the theory of QIIT signatures.
• Be direct enough, so that signatures for type theories can be written out without excessive encoding overhead.
• Be suitable for practical implementation in proof assistants.
• Be reducible to a minimal set of basic type formers.
With the current work, we have improved the state of QIITs with respect to the above criteria. However, a number of open research problems remain.
With regards to the expressiveness of QIIT signatures, we do not yet support sort equations, i.e. equations of elements of Tm Γ U in signatures. Sort equations are included in Cartmell's generalized algebraic theories [1], and they appear to be highly useful for giving an algebraic representation for Russell-style universes and cumulative universes [15]. We leave this for future work, but we note that the current isofibration-based semantics does not work in the presence of strict sort equations, since they are not invariant under isomorphism; instead, sort equations are compatible with the stricter semantics of [4].
While we have made an effort to shape the syntax and semantics of QIITs to be amenable to implementation in proof assistants, much needs to be done before we can have a practical implementation. For one, we would need to consider QIITs in a type theory where transports along equality proofs compute, and would need to work out computing transports for QIITs. Cubical Agda has recently made strides in implementing HITs [30], but as of now it does not support computing transports on indexed inductive types.
With regards to the reduction of QIITs to simple type formers, the reduction of infinitary QIITs appears to be more challenging than the finitary case. [8,Section 9] shows that infinitary QIITs are not constructible from inductive types and simple quotients with relations. In the finitary case, a generalization of the approach in [31] seems promising; this amounts to a Streicher-style initial algebra construction [32] for the theory of finitary QIIT signatures. In particular, Brunerie et al. [33] have formalized in Agda this construction for a comparable type theory, using UIP, function extensionality, propositional extensionality and simple quotient types.
Another line of possible future work would be to explore a more general functorial style of semantics for QIITs. So far, we considered set-based 1-categorical semantics, which is what we need when we want to reason inductively about syntaxes of type theories. However, it would be fruitful to consider algebras in structured categories other than the category of sets.