Higher induction-induction-recursion

HIIRT.md

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.

A Logical Framework for Algebraic Signatures

I've previously used this in a presentation. The general idea comes from my thesis but the syntax is bit more streamlined.

We work in a type theory with four universes:

• Set: this represents the metatheory, in the sense of two-level type theory. The equality type in Set (denoted ≡) can be viewed as definitional equality.
• Sig: types in Sig can be viewed as algebraic signatures.
• Sort: can be used to specify sorts in signatures.
• ℂ: this represents the type theory where algebras (and initial algebras, as inductive types) live. The "external", pre-existing types that we can refer to in signatures must come from ℂ.

Moreover, we have the following cumulative subtyping:

• Sort ⊆ Sig ⊆ Set
• ℂ ⊆ Set

This means, for instance, that Sort : Sig and Sig : Set, and if A : Sort, then A : Sig and A : Set.

Lastly, there are restrictions on eliminations:

• From Sort and Sig, we can only eliminate to Sig.
• From ℂ, we can only eliminate to ℂ.

By specifying different type formers in Sig and Sort, we get different kinds of signatures as inhabitants of Sig. Basics:

• We assume ⊤ and Σ in Sig.
• We assume Π in Sig with domain in Sort and codomain in Sig.

We use (x : A) × B as notation for Σ types and (x : A) → B for Π types in general.

At this point, inhabitants of Sig correspond to closed inductive-inductive signatures. Example:

NatSig : Sig
NatSig := (Nat : Sort) × (zero : Nat) × (suc : Nat → Nat) × ⊤

The arrow in the type of suc has domain in Sort and codomain in Sig (because Nat : Sort implies Nat : Sig), so it checks out. In contrast, the following signature is ill-typed:

NegSig : Sig
NegSig := (A : Sort) × (con : (A → A) → A) × ⊤

In the type of con, the domain of the function must be in Sort, but Sort does not contain any function type at this point.

Whenever we have a signature, we have a corresponding type of algebras. For NatSig, we have

NatAlg : Set
NatAlg = (Nat : ℂ) × (zero : Nat) × (suc : Nat → Nat) × ⊤

Informally, the computation of algebras from signatures replaces

• Sig with Set
• Sig type formers with Set type formers
• Sort with ℂ
• Sort type formers with ℂ type formers

Another example; this one's properly inductive-inductive:

ConTySig : Sig
ConTySig := (Con : Sort) × (Ty : Con → Sort) × (nil : Con) × (ext : (Γ : Con) → Ty Γ → Con) × ⊤

Let's add more type formers:

• Assume Π in Sort with domain in ℂ and codomain in Sort.
• Assume Π in Sig with domain in ℂ and codomain in Sig.

This gets us to infinitary parameterized inductive-inductive signatures. For example, if ℕ : ℂ, we can define ℕ-branching trees:

TreeSig : Sig
TreeSig := (Tree : Sort) × (branch : (ℕ → Tree) → Tree) × (leaf : Tree) × ⊤

We can represent signature parameters by abstracting over ℂ:

ListSig : ℂ → Sig
ListSig A := (List : Sort) × (nil : List) × (cons : A → List → List) × ⊤

Now,

• If we add intensional identity to Sort (with elimination to Sig), we get higher inductive-inductive signatures.
• If we add extensional identity to Sort, we get quotient inductive-inductive signatures.

Inductive-Recursive Signatures

We add a new Tarski-style universe:

SortOver : ℂ → Sig
El : {A : ℂ} → SortOver A → A → Sig

Now, we can declare a sort which has a recursive function associated to it. For example:

FooSig = (Foo : SortOver ℕ) × (foo : El Foo 0) × (bar : El Foo 1) × ⊤

The corresponding algebra contains a function associated to the Foo sort:

FooAlg = (Foo : ℂ)   × (f : Foo → ℕ)
       × (foo : Foo) × (f foo ≡ 0)
       × (bar : Foo) × (f bar ≡ 1)
       × ⊤

Recall that _≡_ refers to the equality type in Set, i.e. definitional equality. Generally speaking, we want to specify the recursive components of algebras up to definitional equality.

We add a Π type to Sig with domain in SortOver and codomain in Sig.

Π : {I : ℂ} → (A : SortOver I) → ((i : I) → El A i → Sig) → Sig

We use the following notation: (i^a : A) → B stands for Π {I} A (λ i a. B). This function type also has application and abstraction; these are specified as the definitional isomorphism:

((i^a : A) → B i a) ≃ ((i : I)(a : El A i) → B i a)

Example for a list signature defined together with a length function:

ListSig : ℂ → Sig
ListSig A = (List : SortOver ℕ)
          × (nil  : El List 0)
          × (cons : A → (n^_ : List) → El List (n + 1))
          × ⊤

The corresponding algebras:

ListAlg : ℂ → Set
ListAlg A = (List : ℂ)               × (len : List → ℕ)
          × (nil : List)             × (len nil ≡ 0)
          × (cons : A → List → List) × (∀ a as. len (cons a as) ≡ len as + 1)
          × ⊤

Whenever we abstract over an element of a fibered sort in a signature, we additionally always abstract over the value which stands for the result of the recursive function on that value. This makes it possible to recover the equations which specify the recursive functions.

I don't describe here the exact algorithm which computes the IR algebras. Technically, what I wrote above is equivalent to what we get from the algorithm, but it's not strictly the same. The algorithm works by simple recursion on type formers so it has to return "packed" results. We'd get the cons constructor and the equation packed as below:

(a : A)(as : List) → (as' : List) × (len as' ≡ len as + 1)

Let's assume now that ℂ has Π types, and add a Π to SortOver with domain in ℂ and codomain in SortOver:

Π : (A : ℂ)(B : A → (I : ℂ) × SortOver I) → SortOver ((a : A) → fst (B a))

The codomain is fibered over an I : ℂ that we can choose for each a : A. Note that (a : A) → fst (B a) uses the Π type former in ℂ. We use the following notation: (a : A) → (I, B) means Π A (λ a. (I, B)). Application and abstraction are specified by the isomorphism:

Π A b ≃ ((a : A)(i : fst (b a)) → El (snd (b a)) i)

Consider an IR universe which contains Bool and Π, in Agda:

data U : Set
El : U → Set

data U where
  Bool' : U
  Π'    : (a : U) → (El a → U) → U

El Bool'    = Bool
El (Π' a b) = (x : El a) → El (b x)

To reproduce this using our signatures, we need some universe inside ℂ which is closed under Bool and Π. Let's stratify ℂ to a countable hierarchy: assume ℂ i : ℂ (i + 1) for i : ℕ, and assume type formers as needed in each ℂ i. We assume that we can eliminate from ℂ i to any ℂ j. Let us also assume that Π and Σ land in ℂ (i ⊔ j), as in Agda.

We also have to refine Sig and Sort to account for the ℂ levels.

• We have Sig i j : Set, where i specifies sizes of of "ordinary" external parameters in signatures, while j specifies the sizes of inductive-recursive base types of fibered sorts.

For example, if we have ℕ : ℂ 0, then

ℕListSig : Sig 0 j
ℕListSig = (List : Sort) × (nil : List) × (cons : ℕ → List → List) × ⊤

Here, the second j index can be arbitrary since we don't use IR type formers in the signature.

When taking algebras of signatures, in principle we could choose any level for each of the sorts. For simplicity here I assume that a sort in a Sig i j is uniformly interpreted as ℂ i in algebras. For example:

ℕListAlg : Set
ℕListAlg = (List : ℂ 0) × (nil : List) × (cons : ℕ → List → List) × ⊤

(This sizing choice is generally consistent for initial algebras).

Let's get back to the IR universe example.

USig : Sig 0 1
USig = (U     : SortOver (ℂ 0))
     × (Bool' : El U Bool)
     × (Π'    : (A^_ : U) → (B^_ : A → (ℂ 0, U)) → El U ((x : A) → B x)
     × ⊤

This is a bit more complicated. Let's look at Π'.

• First, we abstract over U, which binds two names: A : ℂ 0 is the base value, and we could also bind a : El U A in the "fiber", but here we don't need to refer to it.
• Next, we abstract over a fibered function. Here, B : A → ℂ 0; recall the typing rule for the Π type in SortOver. A → (ℂ 0, U) is a non-dependent fibered function type.

What about the algebras? We make the following choice: in a Sig i j, a sort over anything yields a ℂ i type in the algebra. In the current case:

UAlg : Set
UAlg = (U     : ℂ 0)                     × (f : U → ℂ 0)
     × (Bool' : U  )                     × (f Bool' ≡ Bool)
     × (Π'    : (a : U) → (f a → U) → U  × (∀ a b → f (Π' a b) ≡ ((x : f a) → f (b x)))
     × ⊤

Once again, the formal algorithm would pack up Π' differently, but UAlg is otherwise what we have in Agda.

Only one ingredient is missing now: the ability to add equations (or paths) between elements of fibered sorts. We assume that ℂ has identity type =, and also close SortOver A under an identity type:

Id : (a : SortOver I) → El a i → El a j → SortOver (i = j)

We can choose between extensional and intensional rules.

In the extensional case, we assume extensional = in ℂ, and also

refl    : (a : SortOver I)(x : El a i) → El (Id a x x) refl
reflect : El (Id a x y) p → x ≡ y

where by ≡ we mean the equality type in Set. x ≡ y is well-typed because by equality reflection for p, the indices of the sides are definitionally the same.

In the intensional case, we assume intensional = in ℂ, and make it possible to eliminate from Id to Sig:

refl : (a : SortOver I)(x : El a i) → El (Id a x x) refl

J : (a : SortOver I)(x : El a i)
    (B : ∀ j (y : El a j) (p : i = j) → El (Id a x y p) → Sig)
    → B i x refl refl
    → ∀ j y p (q : El (Id a x y p))
    → B j y p q

Jβ : J a x B br i x refl refl ≡ br

Now, I have never seen any usage of such J in signatures. Already in ordinary HIITs it's rare to use the non-fibered J (and often it is ill-advised to do so; it's preferable to try to come up with better-behaved definitions in cubical type theories. Raw J in HIITs tends to behave poorly).

In any case, let's adapt Mike Shulman's higher IR universe. In pseudo-Agda, with = standing for propositional equality and ≡ for strict equality:

data U : Type
El : U → Type

data U where
  sig : (A : U) → (El A → U) → U
  pi : (A : U) → (El A → U) → U
  path : (A : U) → El A → El A → U
  ua : (A B : U) → (El A = El B) → A = B

El (sig A B)    ≡ Σ (El A) (λ a → El (B a))
El (pi A B)     ≡ Π (El A) (λ a → El (B a))
El (path A a b) ≡ (a = b)
ap El (ua A B p) = p

Our version:

USig : Sig 0 1
USig = (U    : SortOver (ℂ 0))
     × (sig  : (A^_ : U) → (B^_ : A → (ℂ 0, U)) → El U ((x : A) × B x)
     × (pi   : (A^_ : U) → (B^_ : A → (ℂ 0, U)) → El U ((x : A) → B x)
     × (path : (A^_ : U) → (x : A) → (y : A) → El U (x = y)
     × (ua   : (A^a : U)(B^b : U) → (p : A = B) → El (Id U a b) p
     × ⊤

I haven't really checked the semantics of HIIR signatures. It might be the case that definitional equations for recursive functions don't work when we compute algebras, or it might be the case that strict equality works even for the ap El (ua A B p) case in Mike's definition.

However, as I mentioned, for things that we want to mechanize in a proof assistant, we should instead use a cubical flavor of HIIR signatures. What I described here is in the "book HoTT" style that I also used in my thesis.

The QIIR case, in comparison, looks pretty straightforward and I don't expect any complication in the semantics of signatures.