Logical Methods in Computer Science
Vol. 8 (2:12) 2012, pp. 1–27
www.lmcs-online.org

Submitted
Published

Jan. 7, 2011
Jun. 19, 2012

GENERIC FIBRATIONAL INDUCTION ∗
NEIL GHANI, PATRICIA JOHANN, AND CLÉMENT FUMEX
University of Strathclyde, Glasgow G1 1XH, UK
e-mail address: {Neil.Ghani, Patricia.Johann, Clement.Fumex}@cis.strath.ac.uk
Abstract. This paper provides an induction rule that can be used to prove properties of
data structures whose types are inductive, i.e., are carriers of initial algebras of functors.
Our results are semantic in nature and are inspired by Hermida and Jacobs’ elegant algebraic formulation of induction for polynomial data types. Our contribution is to derive,
under slightly different assumptions, a sound induction rule that is generic over all inductive types, polynomial or not. Our induction rule is generic over the kinds of properties to
be proved as well: like Hermida and Jacobs, we work in a general fibrational setting and
so can accommodate very general notions of properties on inductive types rather than just
those of a particular syntactic form. We establish the soundness of our generic induction
rule by reducing induction to iteration. We then show how our generic induction rule can
be instantiated to give induction rules for the data types of rose trees, finite hereditary
sets, and hyperfunctions. The first of these lies outside the scope of Hermida and Jacobs’
work because it is not polynomial, and as far as we are aware, no induction rules have
been known to exist for the second and third in a general fibrational framework. Our
instantiation for hyperfunctions underscores the value of working in the general fibrational
setting since this data type cannot be interpreted as a set.

1. Introduction
Iteration operators provide a uniform way to express common and naturally occurring
patterns of recursion over inductive data types. Expressing recursion via iteration operators makes code easier to read, write, and understand; facilitates code reuse; guarantees
properties of programs such as totality and termination; and supports optimising program transformations such as fold fusion and short cut fusion. Categorically, iteration
operators arise from initial algebra semantics of data types, in which data types are regarded as carriers of initial algebras of functors. Lambek’s Lemma ensures that the carrier
of the initial algebra of F is its least fixed point µF , and initiality ensures that, given
any F -algebra h : F A → A, there is a unique F -algebra homomorphism, denoted f old h,
from the initial algebra in : F (µF ) → µF to that algebra. For each functor F , the map
1998 ACM Subject Classification: F.3.2, D.3.1.
Key words and phrases: Induction, algebraic semantics of data types, fibrations, category theory.
∗
This paper is revised and significantly expanded version of [9].
This research is partially supported by EPSRC grant EP/C0608917/1.

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-8 (2:12) 2012

CC

N. Ghani, P. Johann, and C. Fumex
Creative Commons

2

N. GHANI, P. JOHANN, AND C. FUMEX

fold : (F A → A) → µF → A is the iteration operator for the data type µF . Initial algebra
semantics thus provides a well-developed theory of iteration which is...
• ...principled, in that it is derived solely from the initial algebra semantics of data types.
This is important because it helps ensure that programs have rigorous mathematical
foundations that can be used to ascertain their meaning and correctness.
• ...expressive, and so is applicable to all inductive types — i.e., to every type which is the
carrier of an initial algebra of a functor — rather than just to syntactically defined classes
of data types such as polynomial data types.
• ...correct, and so is valid in any model — set-theoretic, domain-theoretic, realisability,
etc. — in which data types are interpreted as carriers of initial algebras.
Because induction and iteration are closely linked — induction is often used to prove properties of functions defined by iteration, and the correctness of induction rules is often established by reducing it to that of iteration — we may reasonably expect that initial algebra
semantics can be used to derive a principled, expressive, and correct theory of induction
for data types as well. In most treatments of induction, given a functor F together with a
property P to be proved about data of type µF , the premises of the induction rule for µF
constitute an F -algebra with carrier Σx : µF. P x. The conclusion of the rule is obtained by
supplying such an F -algebra as input to the iteration operator for µF . This yields a function from µF to Σx : µF. P x from which a function of type ∀x : µF. P x can be obtained. It
has not, however, been possible to characterise F -algebras with carrier Σx : µF. P x without
additional assumptions on F . Induction rules are thus typically derived under the assumption that the functors involved have a certain structure, e.g., that they are polynomial.
Moreover, taking the carriers of the algebras to be Σ-types assumes that properties are
represented as type-valued functions. So while induction rules derived as described above
are both principled and correct, their expressiveness is limited along two dimensions: with
respect to the data types for which they can be derived and the nature of the properties
they can verify.
A more expressive, yet still principled and correct, approach to induction is given by
Hermida and Jacobs [10]. They show how to lift each functor F on a base category of types
to a functor F̂ on a category of properties over those types, and take the premises of the
induction rule for the type µF to be an F̂ -algebra. Hermida and Jacobs work in a fibrational
setting and the notion of property they consider is, accordingly, very general. Indeed, they
accommodate any notion of property that can be suitably fibred over the category of types,
and so overcome one of the two limitations mentioned above. On the other hand, their
approach gives sound induction rules only for polynomial data types, so the limitation on
the class of data types treated remains in their work.
This paper shows how to remove the restriction on the class of data types treated.
Our main result is a derivation of a sound generic induction rule that can be instantiated
to every inductive type, regardless of whether it is polynomial or not. We think this is
important because it provides a counterpart for induction to the existence of an iteration
operator for every inductive type. We take Hermida and Jacobs’ approach as our point of
departure and show that, under slightly different assumptions on the fibration involved, we
can lift any functor on the base category of a fibration to a functor on the total category of
the fibration. The lifting we define forms the basis of our generic induction rule.

GENERIC FIBRATIONAL INDUCTION

3

The derivation of a generic, sound induction rule covering all inductive types is clearly
an important theoretical result, but it also has practical consequences:
• We show in Example 2 how our generic induction rule can be instantiated to the families
fibration over Set (the fibration most often implicitly used by type theorists and those
constructing inductive proofs with theorem provers) to derive the induction rule for rose
trees that one would intuitively expect. The data type of rose trees lies outside the scope
of Hermida and Jacobs’ results because it is not polynomial. On the other hand, an
induction rule for rose trees is available in the proof assistant Coq, although it is neither
the one we intuitively expect nor expressive enough to prove properties that ought to be
amenable to inductive proof. Indeed, if we define rose trees in Coq by
Node : list rose -> rose
then Coq generates the following induction rule
rose_ind : forall P : rose -> Prop,
(forall l : list rose, P (Node l)) ->
forall r : rose, P r
But to prove a property of a rose tree Node l, we must prove that property assuming only
that l is a list of rose trees, and without recourse to any induction hypothesis. There is,
of course, a presentation of rose trees by mutual recursion as well, but this doesn’t give
the expected induction rule in Coq either. Intuitively, what we expect is an induction
rule whose premise is
forall [r_0, ..., r_n] : list rose,
P(r_0) -> ... -> P(r_n) -> P(Node [r_0, ..., r_n])
The rule we derive for rose trees is indeed the expected one, which suggests that our
derivation may enable automatic generation of more useful induction rules in Coq, rather
than requiring the user to hand code them as is currently necessary.
• We further show in Example 3 how our generic induction rule can be instantiated, again
to the families fibration over Set, to derive a rule for the data type of finite hereditary
sets. This data type is defined in terms of quotients and so lies outside most current
theories of induction.
• Finally, we show in Example 7 how our generic induction rule can be instantiated to the
subobject fibration over ωCP O⊥ to derive a rule for the data type of hyperfunctions.
Because this data type cannot be interpreted as a set, a fibration other than the families
fibration over Set is required; in this case, use of the subobject fibration allows us to
derive an induction rule for admissible subsets of hyperfunctions. The ability to treat the
data type of hyperfunctions thus underscores the importance of developing our results
in the general fibrational framework. Moreover, the functor underlying the data type of
hyperfunctions is not strictly positive [7], so the ability to treat this data type also underscores the advantage of being able to handle a very general class of functors going beyond
simply polynomial functors. As far as we know, induction rules for finite hereditary sets
and hyperfunctions have not previously existed in the general fibrational framework.

4

N. GHANI, P. JOHANN, AND C. FUMEX

Although our theory of induction is applicable to all inductive functors — i.e., to all
functors having initial algebras, including those giving rise to nested types [15], GADTs [21],
indexed containers [1], dependent types [19], and inductive recursive types [6] — our examples show that working in the general fibrational setting is beneficial even if we restrict our
attention to strictly positive data types. We do, however, offer some preliminary thoughts
in Section 5 on the potentially delicate issue of instantiating our general theory with fibrations appropriate for deriving induction rules for specific classes of higher-order functors
of interest. It is also worth noting that the specialisations of our generic induction rule to
polynomial functors in the families fibration over Set coincide exactly with the induction
rules of Hermida and Jacobs. But the structure we require of fibrations generally is slightly
different from that required by Hermida and Jacobs, so while our theory is in essence a
generalisation of theirs, the two are, strictly speaking, incomparable. The structure we
require of our fibrations is, nevertheless, certainly present in all standard fibrational models
of type theory (see Section 4). Like Hermida and Jacobs, we prove our generic induction
rule correct by reducing induction to iteration. A more detailed discussion of when our
induction rules coincide with those of Hermida and Jacobs is given in Section 4.
We take a purely categorical approach to induction in this paper, and derive our generic
induction rule from only the initial algebra semantics of data types. As a result, our work
is inherently extensional. Although translating our constructions into intensional settings
may therefore require additional effort, we expect the guidance offered by the categorical
viewpoint to support the derivation of induction rules for functors that are not treatable at
present. Since we do not use any form of impredicativity in our constructions, and instead
use only the weaker assumption that initial algebras exist, this guidance will be widely
applicable.
The remainder of this paper is structured as follows. To make our results as accessible
as possible, we illustrate them in Section 2 with a categorical derivation of the familiar
induction rule for the natural numbers. In Section 3 we derive an induction rule for the
special case of the families fibration over Set. We also show how this rule can be instantiated
to derive the one from Section 2, and the ones for rose trees and finite hereditary sets
mentioned above. Then, in Section 4 we present our generic fibrational induction rule,
establish a number of results about it, and illustrate it with the aforementioned application
to hyperfunctions. The approach taken in this section is completely different from the
corresponding one in the conference version of the paper [9], and allows us to improve upon
and extend our previous results. Section 5 concludes, discusses possible instantiations of
our generic induction rule for higher-order functors, and offers some additional directions
for future research.
When convenient, we identify isomorphic objects of a category and write = rather
than ≃. We write 1 for the canonical singleton set and denote its single element by · . In
Sections 2 and 3 we assume that types are interpreted as objects in Set, so that 1 also
denotes the unit type in those sections. We write id for identity morphisms in a category
and Id for the identity functor on a category.
2. A Familiar Induction Rule
Consider the inductive data type Nat, which defines the natural numbers and can be specified in a programming language with Haskell-like syntax by
data Nat = Zero | Succ Nat

GENERIC FIBRATIONAL INDUCTION

5

The observation that Nat is the least fixed point of the functor N on Set — i.e., on the
category of sets and functions — defined by N X = 1 + X can be used to define the
following iteration operator:
foldNat
foldNat z s Zero
foldNat z s (Succ n)

=
=
=

X → (X → X) → Nat → X
z
s (foldNat z s n)

The iteration operator foldNat provides a uniform means of expressing common and naturally occurring patterns of recursion over the natural numbers.
Categorically, iteration operators such as foldNat arise from the initial algebra semantics
of data types, in which every data type is regarded as the carrier of the initial algebra of
a functor F . If B is a category and F is a functor on B, then an F -algebra is a morphism
h : F X → X for some object X of B. We call X the carrier of h. For any functor F , the
collection of F -algebras itself forms a category Alg F which we call the category of F -algebras.
In Alg F , an F -algebra morphism between F -algebras h : F X → X and g : F Y → Y is a
map f : X → Y such that the following diagram commutes:
FA

Ff

/ FB
g

h



A

f



/B

When it exists, the initial F -algebra in : F (µF ) → µF is unique up to isomorphism and
has the least fixed point µF of F as its carrier. Initiality ensures that there is a unique
F -algebra morphism fold h : µF → X from in to any F -algebra h : F X → X. This gives
rise to the following iteration operator fold for the inductive type µF :
fold
fold h (in t)

:
=

(F X → X) → µF → X
h (F (fold h) t)

Since fold is derived from initial algebra semantics it is principled and correct. It is also
expressive, since it can be defined for every inductive type. In fact, fold is a single iteration
operator parameterised over inductive types rather than a family of iteration operators, one
for each such type, and the iteration operator foldNat above is the instantiation to Nat of
the generic iteration operator fold .
The iteration operator foldNat can be used to derive the standard induction rule for Nat
which coincides with the standard induction rule for natural numbers, i.e., with the familiar
principle of mathematical induction. This rule says that if a property P holds for 0, and if
P holds for n + 1 whenever it holds for a natural number n, then P holds for all natural
numbers. Representing each property of natural numbers as a predicate P : Nat → Set
mapping each n : Nat to the set of proofs that P holds for n, we wish to represent this rule
at the object level as a function indNat with type
∀(P : Nat → Set). P Zero → (∀n : Nat. P n → P (Succ n)) → (∀n : Nat. P n)
Code fragments such as the above, which involve quantification over sets, properties, or
functors, are to be treated as “categorically inspired” within this paper. This is because
quantification over such higher-kinded objects cannot be interpreted in Set. In order to
give a formal interpretation to code fragments like the one above, we would need to work
in a category such as that of modest sets. While the ability to work with functors over
categories other than Set is one of the motivations for working in the general fibrational

6

N. GHANI, P. JOHANN, AND C. FUMEX

setting of Section 4, formalising the semantics of such code fragments would obscure the
central message of this paper. Our decision to treat such fragments as categorically inspired
is justified in part by the fact that the use of category theory to suggest computational constructions has long been regarded as fruitful within the functional programming community
(see, e.g., [2, 3, 18]).
A function indNat with the above type takes as input the property P to be proved, a
proof φ that P holds for Zero, and a function ψ mapping each n : Nat and each proof that P
holds for n to a proof that P holds for Succ n, and returns a function mapping each n : Nat
to a proof that P holds for n, i.e., to an element of P n. We can write indNat in terms
of foldNat — and thus reduce induction for Nat to iteration for Nat — as follows. First
note that indNat cannot be obtained by instantiating the type X in the type of foldNat
to a type of the form P n for a specific n because indNat returns elements of the types
P n for different values n and these types are, in general, distinct from one another. We
therefore need a type containing all of the elements of P n for every n. Such a type can
informally be thought of as the union over n of P n, and is formally given by the dependent
type Σn : Nat. P n comprising pairs (n, p) where n : Nat and p : P n.
The standard approach to defining indNat is thus to apply foldNat to an N -algebra
with carrier Σn : Nat. P n. Such an algebra has components α : Σn : N at. P n and β : Σn :
N at. P n → Σn : N at. P n. Given φ : P Zero and ψ : ∀n. P n → P (Succ n), we choose
α = (Zero, φ) and β (n, p) = (Succ n, ψ n p) and note that f oldN at α β : N at → Σn :
N at. P n. We tentatively take indNat P φ ψ n to be p, where f oldN at α β n = (m, p).
But in order to know that p actually gives a proof for n itself, we must show that m = n.
Fortunately, this follows easily from the uniqueness of foldNat α β. Indeed, we have that
1 + N at

/ 1 + Σn : N at. P n

/ 1 + N at

[α,β]

in



N at

foldNat α β

in



/ Σn : N at. P n

λ(n,p). n


/ Nat

commutes and, by initiality of in, that (λ(n, p). n)◦(f oldN at α β) is the identity map. Thus
n = (λ(n, p). n)(f oldN at α β n) = (λ(n, p). n)(m, p) = m
πP′

Letting
be the second projection on dependent pairs involving the predicate P , the
induction rule for Nat is thus
indNat
: ∀(P : Nat → Set). P Zero → (∀n : Nat. P n → P (Succ n))
→ (∀n : Nat. P n)
′
indNat P φ ψ = πP ◦ (foldNat (Zero, φ) (λ(n, p). (Succ n, ψ n p)))
As expected, this induction rule states that, for every property P , to construct a proof that
P holds for every n : Nat, it suffices to provide a proof that P holds for Zero, and to show
that, for any n : Nat, if there is a proof that P holds for n, then there is also a proof that
P holds for Succ n.
The use of dependent types is fundamental to this formalization of the induction rule
for Nat, but this is only possible because properties to be proved are taken to be set-valued
functions. The remainder of this paper uses fibrations to generalise the above treatment
of induction to arbitrary inductive functors and arbitrary properties which are suitably
fibred over the category whose objects interpret types. In the general fibrational setting,
properties are given axiomatically via the fibrational structure rather than assumed to be
(set-valued) functions.

GENERIC FIBRATIONAL INDUCTION

7

3. Induction Rules for Predicates over Set
The main result of this paper is the derivation of a sound induction rule that is generic over
all inductive types and which can be used to verify any notion of property that is fibred
over the category whose objects interpret types. In this section we assume that types are
modelled by sets, so the functors we consider are on Set and the properties we consider are
functions mapping data to sets of proofs that these properties hold for them. We make these
assumptions because it allows us to present our derivation in the simplest setting possible,
and also because type theorists often model properties in exactly this way. This makes the
present section more accessible and, since the general fibrational treatment of induction can
be seen as a direct generalisation of the treatment presented here, Section 4 should also be
more easily digestible once the derivation is understood in this special case. Although the
derivation of this section can indeed be seen as the specialisation of that of Section 4 to the
families fibration over Set, no knowledge of fibrations is required to understand it because
all constructions are given concretely rather than in their fibrational forms.
We begin by considering what we might naively expect an induction rule for an inductive
data type µF to look like. The derivation for Nat in Section 2 suggests that, in general, it
should look something like this:
ind : ∀P : µ F → Set. ??? → ∀ x : µF. P x
But what should the premises — denoted ??? here — of the generic induction rule ind be?
Since we want to construct, for any term x : µF , a proof term of type P x from proof terms
for x’s substructures, and since the functionality of the fold operator for µF is precisely
to compute a value for x : µF from the values for x’s substructures, it is natural to try to
equip P with an F -algebra structure that can be input to fold to yield a mapping of each
x : µF to an element of P x. But this approach quickly hits a snag. Since the codomain
of every predicate P : µF → Set is Set itself, rather than an object of Set, F cannot be
applied to P as is needed to equip P with an F -algebra structure. Moreover, an induction
rule for µF cannot be obtained by applying fold to an F -algebra with carrier P x for any
specific x. This suggests that we should try to construct an F -algebra not for P x for each
term x, but rather for P itself.
Such considerations led Hermida and Jacobs [10] to define a category of predicates P
and a lifting for each polynomial functor F on Set to a functor F̂ on P that respects the
structure of F . They then constructed F̂ -algebras with carrier P to serve as the premises of
their induction rules. The crucial part of their construction, namely the lifting of polynomial
functors, proceeds inductively and includes clauses such as
(F\
+ G) P = F̂ P + ĜP
and

(F\
× G) P = F̂ P × ĜP

The construction of Hermida and Jacobs is very general: they consider functors on bicartesian categories rather than just on Set, and represent properties by bicartesian fibrations
over such categories instead of using the specific notion of predicate from Definition 3.2
below. On the other hand, they define liftings for polynomial functors.
The construction we give in this section is in some sense orthogonal to Hermida and
Jacobs’: we focus exclusively on functors on Set and a particular category of predicates, and
show how to define liftings for all inductive functors on Set, including non-polynomial ones.

8

N. GHANI, P. JOHANN, AND C. FUMEX

In this setting, the induction rule we derive properly extends Hermida and Jacobs’, thus
catering for a variety of data types that they cannot treat. In the next section we derive
analogous results in the general fibrational setting. This allows us to derive sound induction
rules for initial algebras of functors defined on categories other than Set which can be used
to prove arbitrary properties that are suitably fibred over the category interpreting types.
We begin with the definition of a predicate.
Definition 3.1. Let X be a set. A predicate on X is a function P : X → Set mapping
each x ∈ X to a set P x. We call X the domain of P .
We may speak simply of “a predicate P ” if the domain of P is understood. A predicate
P on X can be thought of as mapping each element x of X to the set of proofs that P holds
for x. We now define our category of predicates.
Definition 3.2. The category of predicates P has predicates as its objects. A morphism
from a predicate P : X → Set to a predicate P ′ : X ′ → Set is a pair (f, f ∼ ) : P → P ′ of
functions, where f : X → X ′ and f ∼ : ∀x : X. P x → P ′ (f x). Composition of predicate
morphisms is given by (g, g∼ ) ◦ (f, f ∼ ) = (g ◦ f, λxp. g ∼ (f x)(f ∼ xp)).
Diagrammatically, we have
f

/ X′
④
∼
❉❉
④
❉❉ f
④④
❉❉
④/ ④P ′
④
P
}④
"

X ❉
❉

Set
As the diagram indicates, the notion of a morphism from P to P ′ does not require the sets
of proofs P x and P ′ (f x), for any x ∈ X, to be equal. Instead, it requires only the existence
of a function f ∼ which maps, for each x, each proof in P x to a proof in P ′ (f x). We denote
by U : P → Set the forgetful functor mapping each predicate P : X → Set to its domain
X and each predicate morphism (f, f ∼ ) to f .
An alternative to Definition 3.2 would take the category of predicates to be the arrow
category over Set, but the natural lifting in this setting does not indicate how to generalise
liftings to other fibrations. Indeed, if properties are modelled as functions, then every
functor can be applied to a property, and hence every functor can be its own lifting. In the
general fibrational setting, however, properties are not necessarily modelled by functions,
so a functor cannot, in general, be its own lifting. The decision not to use arrow categories
to model properties is thus dictated by our desire to lift functors in a way that indicates
how liftings can be constructed in the general fibrational setting.
We can now give a precise definition of a lifting.
Definition 3.3. Let F be a functor on Set. A lifting of F from Set to P is a functor F̂ on
P such that the following diagram commutes:
P

F̂

/P
U

U



Set



F

/ Set

We can decode the definition of F̂ as follows. The object part of F̂ must map each predicate
P : X → Set to a predicate F̂ P : F X → Set, and thus can be thought of type-theoretically

GENERIC FIBRATIONAL INDUCTION

9

as a function ∀(X : Set). (X → Set) → F X → Set. Of course, F̂ must also act on
morphisms in a functorial manner.
We can now use the definition of a lifting to derive the standard induction rule from
Section 2 for Nat as follows.
Example 1. The data type of natural numbers is µN where N is the functor on Set defined
by N X = 1 + X. A lifting N̂ of N can be defined by sending each predicate P : X → Set
b P : N X → Set given by
to the predicate N
N̂ P (inl ·)
N̂ P (inr n)

=
=

1
Pn

An N̂ -algebra with carrier P : Nat → Set can be given by in : 1 + Nat → Nat and
in∼ : ∀t : 1 + Nat. N̂ P t → P (in t). Since in (inl ·) = 0 and in (inr n) = n + 1, we see that
in∼ consists of an element h1 : P 0 and a function h2 : ∀n : Nat. P n → P (n + 1). Thus, the
second component in ∼ of an N̂ -algebra with carrier P : Nat → Set and first component in
gives the premises of the familiar induction rule in Example 1.
The notion of predicate comprehension is a key ingredient of our lifting. It begins to
explain, abstractly, what the use of Σ-types is in the theory of induction, and is the key
construct allowing us to define liftings for non-polynomial, as well as polynomial, functors.
Definition 3.4. Let P be a predicate on X. The comprehension of P , denoted {P }, is the
type Σx : X. P x comprising pairs (x, p) where x : X and p : P x. The map taking each
predicate P to {P }, and taking each predicate morphism (f, f ∼ ) : P → P ′ to the morphism
{(f, f ∼ )} : {P } → {P ′ } defined by {(f, f ∼ )}(x, p) = (f x, f ∼ x p), defines the comprehension
functor {−} from P to Set.
We are now in a position to define liftings uniformly for all functors:
Definition 3.5. If F is a functor on Set, then the lifting F̂ is the functor on P given as
follows. For every predicate P on X, F̂ P : F X → Set is defined by F̂ P = (F πP )−1 ,
where the natural transformation π : {−} → U is given by πP (x, p) = x. For every predicate
morphism f : P → P ′ , F̂ f = (k, k ∼ ) where k = F U f , and k∼ : ∀y : F X. F̂ P y → F̂ P ′ (k y)
is given by k∼ y z = F {f }z.
In the above definition, note that the inverse image f −1 of f : X → Y is indeed a predicate
P : Y → Set. Thus if P is a predicate on X, then πP : {P } → X and F πP : F {P } → F X.
Thus F̂ P is a predicate on F X, so F̂ is a lifting of F from Set to P. The lifting F̂ captures
an “all” modality, in that it generalises Haskell’s all function on lists to arbitrary data
types. A similar modality is given in [17] for indexed containers.
The lifting in Example 1 is the instantiation of the construction in Definition 3.5 to
the functor N X = 1 + X on Set. Indeed, if P is any predicate, then N̂ P = (N πP )−1 ,
i.e., N̂ P = (id + πP )−1 . Then, since the inverse image of the coproduct of functions is the
coproduct of their inverse images, since id −1 1 = 1, and since πP−1 n = {(n, p) | p : P n} for
all n, we have N̂ P (inl ·) = 1 and N̂ P (inr n) = P n. As we will see, a similar situation
to that for Nat holds in general: for any functor F on Set, the second component of an
F̂ -algebra whose carrier is the predicate P on the data type µF and whose first component
is in gives the premises of an induction rule that can be used to show that P holds for all
data of type µF .

10

N. GHANI, P. JOHANN, AND C. FUMEX

The rest of this section shows that F -algebras with carrier {P } are interderivable with
F̂ -algebras with carrier P , and then uses this result to derive our induction rule.
Definition 3.6. The functor K1 : Set → P maps each set X to the predicate K1 X = λx :
X. 1 on X and each f : X → Y to the predicate morphism (f, λx : X. id).
The predicate K1 X is called the truth predicate on X. For every x : X, the set K1 Xx of
proofs that K1 X holds for x is a singleton, and thus is non-empty. We intuitively think of
a predicate P : X → Set as being true if P x is non-empty for every x : X. We therefore
consider P to be true if there exists a predicate morphism from K1 X to P whose first
component is id X . For any functor F , the lifting F̂ is truth-preserving, i.e., F̂ maps the
truth predicate on any set X to that on F X.
Lemma 3.7. For any functor F on Set and any set X, F̂ (K1 X) ∼
= K1 (F X).
Proof. By Definition 3.5, F̂ (K1 X) = (F πK1 X )−1 . We have that πK1 X is an isomorphism
because there is only one proof of K1 X for each x : X, and thus that F πK1 X is an isomorphism as well. As a result, (F πK1 X )−1 maps every y : F X to a singleton set, and therefore
F̂ (K1 X) = (F πK1 X )−1 ∼
= λy : F X. 1 = K1 (F X).
The fact that K1 is a left-adjoint to {−} is critical to the constructions below. This is
proved in [10]; we include its proof here for completeness and to establish notation. The
description of comprehension as a right adjoint can be traced back to Lawvere [14].
Lemma 3.8. K1 is left adjoint to {−}.
Proof. We must show that, for any predicate P and any set Y , the set P(K1 Y, P ) of
morphisms from K1 Y to P in P is in bijective correspondence with the set Set(Y, {P })
of morphisms from Y to {P } in Set. Define maps (−)† : Set(Y, {P }) → P(K1 Y, P ) and
(−)# : P(K1 Y, P ) → Set(Y, {P }) by h† = (h1 , h2 ) where hy = (v, p), h1 y = v and h2 y = p,
and (k, k∼ )# = λ(y : Y ). (ky, k∼ y). These give a natural isomorphism between Set(Y, {P })
and P(K1 Y, P ).
Naturality of (−)† ensures that (g ◦f )† = g † ◦K1 f for all f : Y ′ → Y and g : Y → {P }.
Similarly for (−)# . Moreover, id† is the counit, at P , of the adjunction between K1 and
{−}. These observations are used in the proof of Lemma 3.10. Lemmas 3.9 and 3.10 are the
key results relating F -algebras and F̂ algebras, i.e., relating iteration and induction. They
are special cases of Theorem 4.8 below, but we include their proofs to ensure continuity of
our presentation and to ensure that this section is self-contained.
We first we show how to construct F̂ -algebras from F -algebras
Lemma 3.9. There is a functor Φ : Alg F → Alg F̂ such that if k : F X → X, then
Φk : F̂ (K1 X) → K1 X.
Proof. For an F -algebra k : F X → X define Φk = K1 k, and for two F -algebras k : F X → X
and k′ : F X ′ → X ′ and an F -algebra morphism h : X → X ′ between them define the F̂ algebra morphism Φh : Φk → Φk ′ by Φh = K1 h. Then K1 (F X) ∼
= F̂ (K1 X) by Lemma 3.7,
so that Φk is an F̂ -algebra and K1 h is an F̂ -algebra morphism. It is easy to see that Φ
preserves identities and composition.

GENERIC FIBRATIONAL INDUCTION

11

We can also construct F -algebras from F̂ -algebras.
Lemma 3.10. The functor Φ has a right adjoint Ψ such that if j : F̂ P → P , then Ψj :
F {P } → {P }.
Proof. We construct the adjoint functor Ψ : Alg F̂ → Alg F as follows. Given an F̂ -algebra
j : F̂ P → P , we use the fact that F̂ (K1 {P }) ∼
= K1 (F {P }) by Lemma 3.7 to define
†
#
Ψj : F {P } → {P } by Ψj = (j ◦ F̂ id ) . To specify the action of Ψ on an F̂ -algebra
morphism h, define Ψh = {h}. Clearly Ψ preserves identity and composition.
Next we show Φ ⊣ Ψ, i.e., for every F -algebra k : F X → X and F̂ -algebra j : F̂ P → P
with P a predicate on X, there is a natural isomorphism between F -algebra morphisms
from k to Ψj and F̂ -algebra morphisms from Φk to j. We first observe that an F -algebra
morphism from k to Ψj is a map from X to {P }, and an F̂ -algebra morphism from Φk
to j is a map from K1 X to P . A natural isomorphism between such maps is given by the
adjunction K1 ⊣ {−} from Lemma 3.8. We must check that f : X → {P } is an F -algebra
morphism from k to Ψj iff f † : K1 X → P is an F̂ -algebra morphism from Φk to j.
To this end, assume f : X → {P } is an F -algebra morphism from k to Ψj, i.e., assume
f ◦k = Ψj ◦F f . We must prove that f † ◦ Φk = j ◦ F̂ f † . By the definition of Φ in Lemma 3.9,
this amounts to showing f † ◦ K1 k = j ◦ F̂ f † . Now, since (−)† is an isomorphism, f is an F algebra morphism iff (f ◦k)† = (Ψj◦F f )† . Naturality of (−)† ensures that (f ◦k)† = f † ◦K1 k
and that (Ψj ◦ F f )† = (Ψj)† ◦ K1 (F f ), so the previous equality holds iff
f † ◦ K1 k = (Ψj)† ◦ K1 (F f )

(3.1)

But
j ◦ F̂ f †
= j ◦ F̂ id † ◦ K1 f )
= (j ◦ F̂ id† ) ◦ F̂ (K1 f )
= (Ψj)† ◦ K1 (F f )
= f † ◦ K1 k

by naturality of (−)† and f = id ◦ f
by the functoriality of F̂
by the definition of Ψ, the fact that (−)† and (−)#
are inverses, and Lemma 3.7
by Equation 3.1

Thus, f † is indeed an F̂ -algebra morphism from Φk to j.
Lemma 3.10 ensures that F -algebras with carrier {P } are interderivable with F̂ -algebras
with carrier P . For example, the N -algebra [α, β] with carrier {P } from Section 2 can be
derived from the N̂ -algebra with carrier P given in Example 1. Since we define a lifting
F̂ for any functor F , Lemma 3.10 thus shows how to construct F -algebras with carrier
Σx : µF. P x for any functor F and predicate P on µF .
Corollary 3.11. For any functor F on Set, the predicate K1 (µF ) is the carrier of the
initial F̂ -algebra.
Proof. Since Φ is a left adjoint it preserves initial objects, so applying Φ to the initial
F -algebra in : F (µF ) → µF gives the initial F̂ -algebra. By Lemma 3.9, Φ in has type
F̂ (K1 (µF )) → K1 (µF ), so the carrier of the initial F̂ -algebra is K1 (µF ).

12

N. GHANI, P. JOHANN, AND C. FUMEX

We can now derive our generic induction rule. For every predicate P on X and every F̂ algebra (k, k∼ ) : F̂ P → P , Lemma 3.10 ensures that Ψ constructs from (k, k∼ ) an F -algebra
with carrier {P }. Applying the iteration operator to this algebra gives a map
fold (Ψ (k, k∼ )) : µF → {P }
This map decomposes into two parts: φ = πP ◦ fold (Ψ (k, k∼ )) : µF → X and ψ : ∀(t :
µF ). P (φ t). Initiality of in : F (µF ) → µF , the definition of Ψ, and the naturality of πP
ensure φ = fold k. Recalling that πP′ is the second projection on dependent pairs involving
the predicate P , this gives the following sound generic induction rule for the type X, which
reduces induction to iteration:
genind
: ∀ (F : Set → Set) (P : X → Set) ((k, k ∼ ) : (F̂ P → P )) (t : µF ).
P (fold k t)
genind F P = πP′ ◦ fold ◦ Ψ
Notice this induction rule is actually capable of dealing with predicates over arbitrary sets
and not just predicates over µF . However, when X = µF and k = in, initiality of in further
ensures that φ = fold in = id, and thus that genind specialises to the expected induction
rule for an inductive data type µF :
ind

∀ (F : Set → Set) (P : µF → Set) ((k, k ∼ ) : (F̂ P → P )).
(k = in) → ∀(t : µF ). P t
= πP′ ◦ fold ◦ Ψ
:

ind F P

This rule can be instantiated to familiar rules for polynomial data types, as well as to ones
we would expect for data types such as rose trees and finite hereditary sets, both of which
lie outside the scope of Hermida and Jacobs’ method.
Example 2. The data type of rose trees is given in Haskell-like syntax by
data Rose = Node(List Rose)
The functor underlying Rose is F X = List X and its induction rule is
indRose

:

indRose F P
Calculating F̂ P = (F πP
list xs, we have that

)−1

=

∀ (P : Rose → Set) ((k, k ∼ ) : (F̂ P → P )).
(k = in) → ∀(x : Rose). P x
′
πP ◦ fold ◦ Ψ

: F Rose → Set, and writing xs !! k for the k th component of a

F̂ P rs
= {z : F {P } | F πp z = rs}
= {cps : List {P } | List πP cps = rs}
= {cps : List {P } | ∀k < length cps. πP (cps !! k) = rs !! k}
An F̂ -algebra whose underlying F -algebra is in : F Rose → Rose is thus a pair of functions
(in, k∼ ), where k∼ has type
= ∀rs : List Rose.
{cps : List {P } | ∀k < length cps. πP (cps !! k) = rs !! k} → P (Node rs)
= ∀rs : List Rose. (∀k < length rs. P (rs !! k)) → P (Node rs)

GENERIC FIBRATIONAL INDUCTION

13

The last equality is due to surjective pairing for dependent products and the fact that
length cps = length rs. The type of k ∼ gives the hypotheses of the induction rule for rose
trees.
Although finite hereditary sets are defined in terms of quotients, and thus lie outside
the scope of previously known methods, they can be treated with ours.
Example 3. Hereditary sets are sets whose elements are themselves sets, and so are the
core data structures within set theory. The data type HS of finitary hereditary sets is µPf
for the finite powerset functor Pf . We can derive an induction rule for finite hereditary
sets as follows. If P : X → Set, then Pf πP : Pf (Σx : X.P x) → Pf X maps each set
{(x1 , p1 ), . . . , (xn , pn )} to the set {x1 , . . . , xn }, so that (Pf πP )−1 maps a set {x1 , . . . , xn } to
the set P x1 × . . . × P xn . A Pˆf -algebra with carrier P : HS → Set and first component in
therefore has as its second component a function of type
∀({s1 , . . . , sn } : Pf (HS)). P s1 × . . . × P sn → P (in{s1 , . . . , sn })
The induction rule for finite hereditary sets is thus
indHS :: (∀({s1 , . . . , sn } : Pf (HS)). P s1 × . . . × P sn → P (in{s1 , . . . , sn }))
→ ∀(s : HS).P s
4. Generic Fibrational Induction Rules
We can treat more general notions of predicates using fibrations. We motivate the use of
fibrations by observing that i) the semantics of data types in languages involving recursion
and other effects usually involves categories other than Set; ii) in such circumstances, the
notion of a predicate can no longer be taken as a function with codomain Set; and iii)
even when working in Set there are reasonable notions of “predicate” other than that in
Section 3. (For example, a predicate on a set X could be a subobject of X). Moreover,
when, in future work, we consider induction rules for more sophisticated classes of data
types such as indexed containers, inductive families, and inductive recursive families (see
Section 5), we will not want to have to develop an individual ad hoc theory of induction for
each such class. Instead, we will want to appropriately instantiate a single generic theory of
induction. That is, we will want a uniform axiomatic approach to induction that is widely
applicable, and that abstracts over the specific choices of category, functor, and predicate
giving rise to different forms of induction for specific classes of data types.
Fibrations support precisely such an axiomatic approach. This section therefore generalises the constructions of the previous one to the general fibrational setting. The standard
model of type theory based on locally cartesian closed categories does arise as a specific
fibration — namely, the codomain fibration over Set — and this fibration is equivalent
to the families fibration over Set. But the general fibrational setting is far more flexible.
Moreover, in locally cartesian closed models of type theory, predicates and types coexist in
the same category, so that each functor can be taken to be its own lifting. In the general fibrational setting, predicates are not simply functions or morphisms, properties and types do
not coexist in the same category, and a functor cannot be taken to be its own lifting. There
is no choice but to construct a lifting from scratch. A treatment of induction based solely
on locally cartesian closed categories would not, therefore, indicate how to treat induction
in more general fibrations.

14

N. GHANI, P. JOHANN, AND C. FUMEX

Another reason for working in the general fibrational setting is that this facilitates a
direct comparison of our work with that of Hermida and Jacobs [10]. This is important,
since their approach is the most closely related to ours. The main difference between
their approach and ours is that they use fibred products and coproducts to define provably
sound induction rules for polynomial functors, whereas we use left adjoints to reindexing
functors to define provably sound induction rules for all inductive functors. In this section
we consider situations when both approaches are possible and give mild conditions under
which our results coincide with theirs when restricted to polynomial functors.
The remainder of this section is organised as follows. In Section 4.1 we recall the
definition of a fibration, expand and motivate this definition, and fix some basic terminology
surrounding fibrations. We then give some examples of fibrations, including the families
fibration over Set, the codomain fibration, and the subobject fibration. In Section 4.2 we
recall a useful theorem from [10] that indicates when a truth-preserving lifting of a functor
to a category of predicates has an initial algebra. This is the key theorem used to prove
the soundness of our generic fibrational induction rule. In Section 4.3 we construct truthpreserving liftings for all inductive functors. We do this first in the codomain fibration, and
then, using intuitions from its presentation as the families fibration over Set, as studied
in Section 3, in a general fibrational setting. Finally, in Section 4.4 we establish a number
of properties of the liftings, and hence of the induction rules, that we have derived. In
particular, we characterise the lifting that generates our induction rules.
4.1. Fibrations in a Nutshell. In this section we recall the notion of a fibration. More
details about fibrations can be found in, e.g., [12, 20]. We begin with an auxiliary definition.
Definition 4.1. Let U : E → B be a functor.
(1) A morphism g : Q → P in E is cartesian over a morphism f : X → Y in B if U g = f ,
and for every g′ : Q′ → P in E for which U g′ = f ◦ v for some v : U Q′ → X there exists
a unique h : Q′ → Q in E such that U h = v and g ◦ h = g ′ .
(2) A morphism g : P → Q in E is opcartesian over a morphism f : X → Y in B if U g = f ,
and for every g′ : P → Q′ in E for which U g′ = v ◦ f for some v : Y → U Q′ there exists
a unique h : Q → Q′ in E such that U h = v and h ◦ g = g ′ .
It is not hard to see that the cartesian morphism fP§ over a morphism f with codomain U P
is unique up to isomorphism, and similarly for the opcartesian morphism f§P . If P is an

GENERIC FIBRATIONAL INDUCTION

15

object of E, then we write f ∗ P for the domain of fP§ and Σf P for the codomain of f§P . We
can capture cartesian and opcartesian morphisms diagrammatically as follows.
E

′

Q′ ◗◗◗
◗◗◗ ′
◗◗◗g
◗◗◗
h
◗◗◗

◗◗(
∗
/P
f P
§

♠6 Q
♠♠♠ O
g ′ ♠♠♠♠
♠
h
♠♠♠
♠♠♠
♠
♠
♠
/ Σf P
P
P

U Q′ ◗◗
◗◗◗
◗◗U◗ g′
◗◗◗
v
◗◗◗

◗◗(
/Y
X

❧6 U Q
O
❧❧❧
❧
❧
❧
❧
v
❧❧
❧❧❧
❧
❧
❧
/Y
X

fP

f§

U



B

f

′

U g′

f

Cartesian morphisms (opcartesian morphisms) are the essence of fibrations (resp., opfibrations). We introduce both fibrations and their duals now since the latter will prove useful
later in our development. Below we speak primarily of fibrations, with the understanding
that the dual observations hold for opfibrations.
Definition 4.2. Let U : E → B be a functor. Then U is a fibration if for every object P
of E, and every morphism f : X → U P in B there is a cartesian morphism fP§ : Q → P in
E above f . Similarly, U is an opfibration if for every object P of E, and every morphism
f : U P → Y in B there is an opcartesian morphism f§P : P → Q in E above f . A functor
U a bifibration if it is simultaneously a fibration and an opfibration.
If U : E → B is a fibration, we call B the base category of U and E the total category
of U . Objects of the total category E can be thought of as properties, objects of the base
category B can be thought of as types, and U can be thought of as mapping each property
P in E to the type U P of which P is a property. One fibration U can capture many different
properties of the same type, so U is not injective on objects. We say that an object P in
E is above its image U P under U , and similarly for morphisms. For any object X of B, we
write EX for the fibre above X, i.e., for the subcategory of E consisting of objects above X
and morphisms above id. If f : X → Y is a morphism in B, then the function mapping
each object P of E to f ∗ P extends to a functor f ∗ : EY → EX . Indeed, for each morphism
k : P → P ′ in EY , f ∗ k is the morphism satisfying k ◦ fP§ = fP§ ′ ◦ f ∗ k. The universal
property of fP§ ′ ensures the existence and uniqueness of f ∗ k. We call the functor f ∗ the
reindexing functor induced by f . A similar situation ensures for opfibrations, and we call
the functor Σf : EX → EY which extends the function mapping each object P of E to Σf P
the opreindexing functor.
Example 4. The functor U : P → Set defined in Section 3 is called the families fibration
over Set. Given a function f : X → Y and a predicate P : Y → Set we can define a
cartesian map fP§ whose domain f ∗ P is P ◦ f , and which comprises the pair (f, λx : X. id).
The fibre PX above a set X has predicates P : X → Set as its objects. A morphism in PX
from P : X → Set to P ′ : X → Set is a function of type ∀x : X. P x → P ′ x.
Example 5. Let B be a category. The arrow category of B, denoted B → , has the morphisms,
or arrows, of B as its objects. A morphism in B → from f : X → Y to f ′ : X ′ → Y ′ is a pair

16

N. GHANI, P. JOHANN, AND C. FUMEX

(α1 , α2 ) of morphisms in B such that the following diagram commutes:
α1

X

/ X′
f′

f





Y

α2

/ Y′

i.e., such that α2 ◦ f = f ′ ◦ α1 . It is easy to see that this definition indeed gives a category.
The codomain functor cod : B → → B maps an object f : X → Y of B → to the object
Y of B and a morphism (α1 , α2 ) of B → to α2 . If B has pullbacks, then cod is a fibration,
called the codomain fibration over B. Indeed, given an object f : X → Y in the fibre above
Y and a morphism f ′ : X ′ → Y in B, the pullback of f along f ′ gives a cartesian morphism
above f ′ as required. The fibre above an object Y of B has those morphisms of B that map
into Y as its objects. A morphism in (B → )Y from f : X → Y to f ′ : X ′ → Y is a morphism
α1 : X → X ′ in B such that f = f ′ ◦ α1 .
Example 6. If B is a category, then the category of subobjects of B, denoted Sub(B), has
monomorphisms in B as its objects. A monomorphism f : X ֒→ Y is called a subobject of
Y . A morphism in Sub(B) from f : X ֒→ Y to f ′ : X ′ ֒→ Y ′ is a pair of morphisms (α1 , α2 )
in B such that α2 ◦ f = f ′ ◦ α1 .
The map U : Sub(B) → B sending a subobject f : X ֒→ Y to Y extends to a functor. If
B has pullbacks, then U is a fibration, called the subobject fibration over B; indeed, pullbacks
again give cartesian morphisms since the pullback of a monomorphism is a monomorphism.
The fibre above an object Y of B has as objects the subobjects of Y . A morphism in
Sub(B)Y from f : X ֒→ Y to f ′ : X ′ ֒→ Y is a map α1 : X → X ′ in B such that f = f ′ ◦ α1 .
If such a morphism exists then it is, of course, unique.
4.2. Lifting, Truth, and Comprehension. We now generalise the notions of lifting,
truth, and comprehension to the general fibrational setting. We prove that, in such a setting,
if an inductive functor has a truth-preserving lifting, then its lifting is also inductive. We
then see that inductiveness of the lifted functor is sufficient to guarantee the soundness
of our generic fibrational induction rule. This subsection is essentially our presentation of
pre-existing results from [10]. We include it because it forms a natural part of our narrative,
and because simply citing the material would hinder the continuity of our presentation.
Recall from Section 3 that the first step in deriving an induction rule for a datatype
interpreted in Set is to lift the functor whose fixed point the data type is to the category P of
predicates. More specifically, in Definition 3.3 we defined a lifting of a functor F : Set → Set
to be a functor F̂ : P → P such that U F̂ = F U . We can use these observations to generalise
the notion of a lifting to the fibrational setting as follows.
Definition 4.3. Let U : E → B be a fibration and F be a functor on B. A lifting of F with
respect to U is a functor F̂ : E → E such that the following diagram commutes:
E

F̂

/E

U

U



B



F

/B

GENERIC FIBRATIONAL INDUCTION

17

In Section 3 we saw that if P : X → Set is a predicate over X, then F̂ P is a predicate over
F X. The analogous result for the general fibrational setting observes that if F̂ is a lifting
of F and X is an object of B, then F̂ restricts to a functor from EX to EF X .
By analogy with our results from Section 3, we further expect that the premises of a
fibrational induction rule for a datatype µF interpreted in B should constitute an F̂ -algebra
on E. But in order to construct the conclusion of such a rule, we need to understand how
to axiomatically state that a predicate is true. In Section 3, a predicate P : X → Set is
considered true if there is a morphism in P from K1 X, the truth predicate on X, to P that
is over id X . Since the mapping of each set X to K1 X is the action on objects of the truth
functor K1 : Set → P (cf. Definition 3.6), we actually endeavour to model the truth functor
for the families fibration over Set axiomatically in the general fibrational setting.
Modeling the truth functor axiomatically amounts to understanding its universal property. Since the truth functor in Definition 3.6 maps each set X to the predicate λx : x. 1, for
any set X there is therefore exactly one morphism in the fibre above X from any predicate
P over X to K1 X. This gives a clear categorical description of K1 X as a terminal object
of the fibre above X and leads, by analogy, to the following definition.
Definition 4.4. Let U : E → B be a fibration. Assume further that, for every object
X of B, the fibre EX has a terminal object K1 X such that, for any f : X ′ → X in B,
f ∗ (K1 X) ∼
= K1 X ′ . Then the assignment sending each object X in B to K1 X in E, and
§
each morphism f : X ′ → X in B to the morphism fK
in E defines the (fibred) truth
1X
functor K1 : B → E.
The (fibred) truth functor is sometimes called the (fibred) terminal object functor. With
this definition, we have the following standard result:
Lemma 4.5. K1 is a (fibred) right adjoint for U .
The interested reader may wish to consult the literature on fibrations for the definition
of a fibred adjunction, but a formal definition will not be needed here. Instead, we can
simply stress that a fibred adjunction is first and foremost an adjunction, and then observe
that the counit of this adjunction is the identity, so that U K1 = Id . Moreover, K1 is full
and faithful. One simple way to guarantee that a fibration has a truth functor is to assume
that both E and B have terminal objects and that U maps a terminal object of E to a
terminal object of B. In this case, the fact that reindexing preserves fibred terminal objects
ensures that every fibre of E indeed has a terminal object.
The second fundamental property of liftings used in Section 3 is that they are truthpreserving. This property can now easily be generalised to the general fibrational setting
(cf. Definition 3.7).
Definition 4.6. Let U : E → B be a fibration with a truth functor K1 : B → E, let F be
a functor on B, and let F̂ : E → E be a lifting of F . We say that F̂ is a truth-preserving
lifting of F if, for any object X of B, we have F̂ (K1 X) ∼
= K1 (F X).
The final algebraic structure we required in Section 3 was a comprehension functor
{−} : P → Set. To generalise the comprehension functor to the general fibrational setting
we simply note that its universal property is that it is right adjoint to the truth functor K1
(cf. Definition 3.8). We single out for special attention those fibrations whose truth functors
have right adjoints.

18

N. GHANI, P. JOHANN, AND C. FUMEX

Definition 4.7. Let U : E → B be a fibration with a truth functor K1 : B → E. Then U is
a comprehension category with unit if K1 has a right adjoint.
If U : E → B is a comprehension category with unit, then we call the right adjoint to K1
the comprehension functor and denote it by {−} : E → B. With this machinery in place,
Hermida and Jacobs [10] show that if U is a comprehension category with unit and F̂ is a
truth-preserving lifting of F , then F̂ is inductive if F is and, in this case, the carrier µF̂ of
the initial F̂ -algebra is K1 (µF ). This is proved as a corollary to the following more abstract
theorem.
Theorem 4.8. Let F : B → B, G : A → A, and S : B → A be functors. A natural
transformation α : GS → SF , i.e., a natural transformation α such that
AO
S

B

G

/A
O

❈❈❈❈❈❈α
%

S

/B

F

induces a functor
AlgF

Φ

/ AlgG

given by Φ (f : F X → X) = S f ◦ αX . Moreover, if α is an isomorphism, then a right
adjoint T to S induces a right adjoint
AlgF l

Φ
⊤

,

AlgG

Ψ

given by Ψ(g : GX → X) = T g ◦βX , where β : F T → T G is the image of G ǫ◦α−1
T : SF T →
∼
G under the adjunction isomorphism Hom(S X, Y ) = Hom(X, T Y ), and ǫ : ST → id is
the counit of this adjunction.
We can instantiate Theorem 4.8 to generalise Lemmas 3.9 and 3.10.
Theorem 4.9. Let U : E → B be a comprehension category with unit and F : B → B be a
functor. If F has a truth-preserving lifting F̂ then there is an adjunction Φ ⊣ Ψ : Alg F →
Alg F̂ . Moreover, if f : F X → X then Φf : F̂ (K1 X) → K1 X, and if g : F̂ P → P then
Ψg : F {P } → {P }.
Proof. We instantiate Theorem 4.8, letting E be A, F̂ be G, and K1 be S. Then α is an
isomorphism since F̂ is truth-preserving, and we also have that K1 ⊣ {−}. The theorem thus
ensures that Φ maps every F -algebra f : F X → X to an F̂ -algebra Φf : F̂ (K1 X) → K1 X,
and that Ψ maps every F̂ -algebra g : F̂ P → P to an F -algebra Ψg : F {P } → {P }.
Corollary 4.10. Let U : E → B be a comprehension category with unit and F : B → B be
a functor which has a truth-preserving lifting F̂ . If F is inductive, then so is F̂ . Moreover,
µF̂ = K1 (µF ).
Proof. The hypotheses of the corollary place us in the setting of Theorem 4.9. This theorem
guarantees that Φ maps the initial F -algebra in F : F (µF ) → µF to an F̂ -algebra with
carrier K1 (µF ). But since left adjoints preserve initial objects, we must therefore have that
the initial F̂ -algebra has carrier K1 (µF ). Thus, µF̂ exists and is isomorphic to K1 (µF ).

GENERIC FIBRATIONAL INDUCTION

19

Theorem 4.11. Let U : E → B be a comprehension category with unit and F : B → B
be an inductive functor. If F has a truth-preserving lifting F̂ , then the following generic
fibrational induction rule is sound:
genfibind
genfibind F P

: ∀ (F : B → B) (P : E). (F̂ P → P ) → (µF̂ → P )
= fold

An alternative presentation of genfibind is
genfibind
genfibind F P

: ∀ (F : B → B) (P : E). (F̂ P → P ) → (µF → {P })
= fold ◦ Ψ

We call genfibind F the generic fibrational induction rule for µF .
In summary, we have generalised the generic induction rule for predicates over Set
presented in Section 3 to give a sound generic induction rule for comprehension categories
with unit. Our only assumption is that if we start with an inductive functor F on the
base of the comprehension category, then there must be a truth-preserving lifting of that
functor to the total category of the comprehension category. In that case, we can specialise
genfibind to get a fibrational induction rule for any datatype µF that can be interpreted in
the fibration’s base category.
The generic fibrational induction rule genfibind does, however, look slightly different
from the generic induction rule for set-valued predicates. This is because, in Section 3, we
used our knowledge of the specific structure of comprehensions for set-valued predicates
to extract proofs for particular data elements from them. But in the fibrational setting,
predicates, and hence comprehensions, are left abstract. We therefore take the return type
of the general induction scheme genfibind to be a comprehension with the expectation that,
when the general theory of this section is instantiated to a particular fibration of interest, it
may be possible to use knowledge about that fibration to extract from the comprehension
constructed by genfibind further proof information relevant to the application at hand.
As we have previously mentioned, Hermida and Jacobs provide truth-preserving liftings
only for polynomial functors. In Section 4.3, we define a generic truth-preserving lifting for
any inductive functor on the base category of any fibration which, in addition to being a
comprehension category with unit, has left adjoints to all reindexing functors. This gives a
sound generic fibrational induction rule for the datatype µF for any functor F on the base
category of any such fibration.
4.3. Constructing Truth-Preserving Liftings. In light of the previous subsection, it is
natural to ask whether or not truth-preserving liftings exist. If so, are they unique? Or, if
there are many truth-preserving liftings, is there a specific truth-preserving lifting to choose
above others? Is there, perhaps, even a universal truth-preserving lifting? We can also ask
about the algebraic structure of liftings. For example, do truth-preserving liftings preserve
sums and products of functors?
Answers to some of these questions were given by Hermida and Jacobs, who provided
truth-preserving liftings for polynomial functors. To define such liftings they assume that
the total category and the base category of the fibration in question have products and
coproducts, and that the fibration preserves them. Under these conditions, liftings for
polynomial functors can be defined inductively. In this section we go beyond the results of
Hermida and Jacobs and construct truth-preserving liftings for all inductive functors. We
employ a two-stage process, first building truth-preserving liftings under the assumption

20

N. GHANI, P. JOHANN, AND C. FUMEX

that the fibration of interest is a codomain fibration, and then using the intuitions of
Section 3 to extend this lifting to a more general class of fibrations. In Section 4.4 we
consider the questions from the previous paragraph about the algebraic structure of liftings.
4.3.1. Truth-Preserving Liftings for Codomain Fibrations. Recall from Example 5 that if B
has pullbacks, then the codomain fibration over B is the functor cod : B → → B. Given a
functor F : B → B, it is trivial to define a lifting F → : B → → B → for this fibration. We can
define the functor F → to map an object f : X → Y of B → to F f : F X → F Y , and to map
a morphism (α1 , α2 ) to the morphism (F α1 , F α2 ). That F → is a lifting is easily verified.
If we further verify that codomain fibrations are comprehension categories with unit,
and that the lifting F → is truth-preserving, then Theorem 4.11 can be applied to them. For
the former, we first observe that the functor K1 : B → B → mapping an object X to id and
a morphism f : X → Y to (f, f ) is a truth functor for this fibration. (In fact, we can take
any isomorphism into X as K1 X; we will use this observation below.) If we let B → (U, V )
denote the set of morphisms from an object U to an object V in B → , then the fact that K1
is right adjoint to cod can be established via the natural isomorphism
B → (f : X → Y, K1 Z) = {(α1 : X → Z, α2 : Y → Z) | α1 = α2 ◦ f } ∼
= B(Y, Z) = B(cod f, Z)
We next show that the functor dom : B → → B mapping an object f : X → Y of B → to
X and a morphism (α1 , α2 ) to α1 is a comprehension functor for the codomain fibration.
That dom is right adjoint to K1 is established via the natural isomorphism
B → (K1 Z, f : X → Y ) = {(α1 : Z → X, α2 : Z → Y ) | α2 = f ◦ α1 } ∼
= B(Z, X) = B(Z, dom f )
Finally, we have that F → is truth-preserving because
F → (K1 Z) = F → id = F id = id = K1 (F Z)
A lifting is implicitly given in [16] for functors on a category with display maps. Such
a category is a subfibration of the codomain fibration over that category, and the lifting
given there is essentially the lifting for the codomain fibration restricted to the subfibration
in question.
4.3.2. Truth-Preserving Liftings for the Families Fibration over Set. In Section 3 we defined, for every functor F : Set → Set, a lifting F̂ which maps the predicate P to (F πP )−1 .
Looking closely, we realise this lifting decomposes into three parts. Given a predicate P ,
we first consider the projection function πP : {P } → U P . Next, we apply the functor F
to πP to obtain F πP : F {P } → F U P . Finally, we take the inverse image of F πP to get a
predicate over F U P as required.
Note that π is the functor from P to Set→ which maps a predicate P to the projection
function πP : {P } → U P (and maps a predicate morphism (f, f ∼ ) from a predicate P : X →
Set to P ′ : X ′ → Set to the morphism ({(f, f ∼ )}, f ) from πP to πP ′ ; cf. Definition 3.4). If
I : Set→ → P is the functor sending a function f : X → Y to its “inverse” predicate f −1
(and a morphism (α1 , α2 ) to the predicate morphism (α2 , ∀y : Y. λx : f −1 y. α1 x)), then
each of the three steps of defining F̂ is functorial and the relationships indicated by the

GENERIC FIBRATIONAL INDUCTION

21

following diagram hold:
π

P ❇l

❇❇
❇❇
❇❇
U ❇!

⊤
I

Set

,

Set→

✇✇
✇✇
✇
✇
{ ✇ cod
✇

Note that the adjunction I ⊣ π is an equivalence. This observation is not, however,
necessary for our subsequent development; in particular, it is not needed for Theorem 4.14.
The above presentation of the lifting F̂ of a functor F for the families fibration over Set
uses the lifting of F for the codomain fibration over Set. Indeed, writing F → for the lifting
of F for the codomain fibration over Set, we have that F̂ = IF → π. Moreover, since π and
I are truth-preserving (see the proof of Lemma 3.7), and since we have already seen that
liftings for codomain fibrations are truth-preserving, we have that F̂ is truth-preserving
because each of its three constituent functors is. Finally, since we showed in Section 3 that
the families fibration over Set is a comprehension category with unit, Theorem 4.11 can be
applied to it.
Excitingly, as we shall see in the next subsection, the above presentation of the lifting
of a functor for the families fibration over Set generalises to many other fibrations!
4.3.3. Truth-Preserving Liftings for Other Fibrations. We now turn our attention to the
task of constructing truth-preserving liftings for fibrations other than codomain fibrations
and the families fibration over Set. By contrast with the approach outlined in the conference
paper [9] on which this paper is based, the one we take here uses a factorisation, like that
of the previous subsection, through a codomain fibration. More specifically, let U : E → B
be a comprehension category with unit. We first define functors I and π, and construct an
adjunction I ⊣ π between E and B → such that the relationships indicated by the following
diagram hold:
π

E ❄k

❄❄
❄❄
❄
U ❄❄

⊤
I

,

B→

⑤
⑤⑤
⑤
⑤⑤
}⑤⑤ cod

B
We then use the adjunction indicated in the diagram to construct truth-preserving a lifting
for U from that for the codomain fibration over B.
To define the functor π : E → B → we generalise the definition of π : P → Set→
from Sections 3 and 4.3.2. This requires us to work with the axiomatic characterisation in
Definition 4.7 of the comprehension functor {−} : E → B as the right adjoint to the truth
functor K1 : B → E. The counit of the adjunction K1 ⊣ {−} is a natural transformation
ǫ : K1 {−} → Id. Applying U to ǫ gives the natural transformation U ǫ : U K1 {−} → U , but
since U K1 = Id, in fact we have that U ǫ : {−} → U . We can therefore define π to be U ǫ.
Then π is indeed a functor from E to B → , its action on an object P is πP , and its action
on a morphism (f, f ∼ ) is ({(f, f ∼ )}, f ).
We next turn to the definition of the left adjoint I to π. To see how to generalise the
inverse image construction to more general fibrations we first recall from Example 4 that, if
f : X → Y is a function and P : Y → Set, then f ∗ P = P ◦ f . We can extend this mapping

22

N. GHANI, P. JOHANN, AND C. FUMEX

to a reindexing functor f ∗ : EY → EX by defining f ∗ (id , h∼ ) = (id , h∼ ◦ f ). If we define the
action of Σf : EX → EY on objects by
]
Σf P = λy.
Px
{x|f x=y}

U

where denotes the disjoint union operator on sets, and its action on morphisms by taking
Σf (id , α∼ ) to be (id , ∀(y : Y ). λ(x : X, p : f x = y, t : P x). (x, p, α∼ x t)), then Σf is left
adjoint to f ∗ . Moreover, if we compute
]
Σf (K1 X) = λy.
K1 Xx
{x | f x=y}

and recall that, for any x : X, the set K1 X x is a singleton, then Σf (K1 X) is clearly
equivalent to the inverse image of f .
The above discussion suggests that, in order to generalise the inverse image construction
to a more general fibration U : E → B, we should require each reindexing functor f ∗ to have
the opreindexing functor Σf as its left adjoint. As in [10], no Beck-Chevalley condition is
required on these adjoints. The following result, which appears as Proposition 2.3 of [11],
thus allows us to isolate the exact class of fibrations for which we will have sound generic
induction rules.
Theorem 4.12. A fibration U : E → B is a bifibration iff for every morphism f in B the
reindexing functor f ∗ has left adjoint Σf .
Definition 4.13. A Lawvere category is a bifibration which is also a comprehension category
with unit.
We construct the left adjoint I : B → → E of π for any Lawvere category U : E → B as
follows. If f : X → Y is an object of B → , i.e., a morphism of B, then we define I f to be the
object Σf (K1 X) of E. To define the action of I on morphisms, let (α1 , α2 ) be a morphism
in B → from f : X → Y to f ′ : X ′ → Y ′ in B → . Then (α1 , α2 ) is a pair of morphisms in B
such that the following diagram commutes:
X

α1

/ X′
f′

f





Y

α2

/ Y′

We must construct a morphism from Σf (K1 X) to Σf ′ (K1 X ′ ) in E. To do this, notice
′
that f§′K1 X ◦ K1 α1 : K1 X → Σf ′ (K1 X ′ ) is above f ′ ◦ α1 , and that it is also above α2 ◦ f
′

since f ′ ◦ α1 = α2 ◦ f . We can then consider the morphism f§′K1 X ◦ K1 α1 and use the
universal property of the opcartesian morphism f§K1 X to deduce the existence of a morphism
h : Σf (K1 X) → Σf ′ (K1 X ′ ) above α2 . It is not difficult, using the uniqueness of the
morphism h, to prove that setting this h to be the image of the morphism (α1 , α2 ) makes
I a functor. In fact, since cod ◦ π = U , Result (i) on page 190 of [11] guarantees that,
for any Lawvere category U : E → B the functor I : B → → E exists and is left adjoint to
π : E → B→ .
We can now construct a truth-preserving lifting for any Lawvere category U : E → B
and functor F on B.

GENERIC FIBRATIONAL INDUCTION

23

Theorem 4.14. Let U : E → B be a Lawvere category and, for any functor F on B, define
the functor F̂ on E by
F̂ : E → E
F̂ = IF → π
Then F̂ is a truth-preserving lifting of F .
Proof. It is trivial to check that F̂ is indeed a lifting. To prove that it is truth-preserving, we
need to prove that F̂ (K1 X) ∼
= K1 (F X) for any functor F on B and object X of B. We do
this by showing that each of π, F → , and I preserves fibred terminal objects, i.e., preserves
the terminal objects of each fibre of the total category which is its domain. Then since
K1 X is a terminal object in the fibre EX , we will have that F̂ (K1 X) = I(F → (π(K1 X))) is
a terminal object in EF X , i.e., that F̂ (K1 X) ∼
= K1 (F X) as desired.
We first show that π preserves fibred terminal objects. We must show that, for any
object X of B, πK1 X is a terminal object of the fibre of B → over X, i.e., is an isomorphism
with codomain X. We prove this by observing that, if η : Id → {−}K1 is the unit of
the adjunction K1 ⊣ {−}, then πK1 X is an isomorphism with inverse ηX . Indeed, if ǫ
is the counit of the same adjunction, then the facts that U K1 = Id and that K1 is full
and faithful ensure that K1 ηX is an isomorphism with inverse ǫK1 X . Thus, ǫK1 X is an
isomorphism with inverse K1 ηX , and so πK1 X = U ǫK1 X is an isomorphism with inverse
U K1 ηX , i.e., with inverse ηX . Since K1 X is a terminal object in EX and πK1 X is a terminal
object in the fibre of B → over X, we have that π preserves fibred terminal objects.
It is not hard to see that F → preserves fibred terminal objects: applying the functor F
to an isomorphism with codomain X — i.e., to a terminal object in the fibre of B → over
X — gives an isomorphism with codomain F X — i.e., a terminal object in the fibre of B →
over F X.
Finally, if f : X → Y is an isomorphism in B, then Σf is not only left adjoint to f ∗ ,
but also right adjoint to it. Since right adjoints preserve terminal objects, and since K1 X
is a terminal object of EX , we have that If = Σf (K1 X) is a terminal object of EY . Thus I
preserves fibred terminal objects.
We stress that, to define our lifting, the codomain functor over the base B of the Lawvere
category need not be a fibration. In particular, B need not have pullbacks; indeed, all that
is needed to construct our generic truth-preserving lifting F̂ for a functor F on B is the
existence of the functors I and π (and F → , which always exists). We nevertheless present
the lifting F̂ as the composition of π, F → , and I because this presentation shows it can be
factored through F → . This helps motivate our definition of F̂ , thereby revealing parallels
between it and F → that would otherwise not be apparent. At the same time it trades the
direct, brute-force presentation of F̂ from [9] for an elegant modularly structured one which
makes good use, in a different setting, of general results about comprehension categories
due to Jacobs [11].
We now have the promised sound generic fibrational induction rule for every inductive
functor F on the base of a Lawvere category. To demonstrate the flexibility of this rule, we
now derive an induction rule for a data type and properties on it that cannot be modelled
in Set. Being able to derive induction rules for fixed points of functors in categories other
than Set is a key motivation for working in a general fibrational setting.
Example 7. The fixed point Hyp = µF of the functor F X = (X → Int) → Int is the data
type of hyperfunctions. Since F has no fixed point in Set, we interpret it in the category

24

N. GHANI, P. JOHANN, AND C. FUMEX

ωCP O⊥ of ω-cpos with ⊥ and strict continuous monotone functions. In this setting, a
property of an object X of ωCP O⊥ is an admissible sub-ωCP O⊥ P of X. Admissibility
means that the bottom element of X is in P and P is closed under least upper bounds of
ω-chains in X. This structure forms a Lawvere category [11, 12]; in particular, it is routine
to verify the existence of its opreindexing functor. In particular, Σf P is constructed for a
continuous map f : X → Y and an admisible predicate P ⊆ X, as the intersection of all
admissible Q ⊆ Y with P ⊆ f −1 (Q). The truth functor maps X to X, and comprehension
maps a sub-ωCP O⊥ P of X to P . The lifting F̂ maps a sub-ωCP O⊥ P of X to the least
admissible predicate on F X containing the image of F P . Finally, the derived induction
rule states that if P is an admissible sub-ωCP O⊥ of Hyp, and if F̂ (P ) ⊆ P , then P = Hyp.
4.4. An Algebra of Lifting. We have proved that in any Lawvere category U : E → B,
any functor F on B has a lifting F̂ on E which is truth-preserving, and thus has the following
associated sound generic fibrational induction rule:
genfibind
genfibind F P

: ∀ (F : B → B) (P : E). (F̂ P → P ) → (µF → {P })
= fold ◦ Ψ

In this final subsection of the paper, we ask what kinds of algebraic properties the lifting
operation has. Our first result concerns the lifting of constant functors.
Lemma 4.15. Let U : E → B be a Lawvere category and let X be an object of B. If FX is
the constantly X-valued functor on B, then Fc
X is isomorphic to the constantly K1 X-valued
functor on E.
Proof. For any object P of E we have
→
Fc
X P = (I(FX ) π)P = I(FX πP ) = ΣF

X πP

K1 FX {P } = Σid K1 X ∼
= K1 X

The last isomorphism holds because id ∗ ∼
= Id and Σid ⊣ id ∗ .
Our next result concerns the lifting of the identity functor. It requires a little additional
structure on the Lawvere category of interest.
Definition 4.16. A full Lawvere category is a Lawvere category U : E → B such that
π : E → B → is full and faithful.
b ∼
Lemma 4.17. In any full Lawvere category, Id
= Id

Proof. By the discussion following Definition 4.13, I ⊣ π. Since π is full and faithful, the
counit of this adjunction is an isomorphism, and so IπP ∼
= P for all P in E. We therefore
have that
bP
P ∼
= IπP = Σπ K1 {P } = ΣId π K1 (Id {P }) = (I Id → π)P = Id
p

p

bP ∼
i.e., that Id
= P for all P in E. Because these isomorphisms are clearly natural, we
b ∼
therefore have that Id
= Id.

GENERIC FIBRATIONAL INDUCTION

25

We now show that the lifting of a coproduct of functors is the coproduct of the liftings.
Lemma 4.18. Let U : E → B be a Lawvere category and let F and G be functors on B.
Then F\
+G∼
= F̂ + Ĝ.
Proof. We have
(F\
+ G)P = I((F + G)→ πP ) = I(F → πP + G→ πP ) ∼
= I(F → πP ) + I(G→ πP ) = F̂ P + ĜP
The third isomorphism holds because I is a left adjoint and so preserves coproducts.
Note that the statement of Lemma 4.18 does not assert the existence of either of the
two coproducts mentioned, but rather that, whenever both do exist, they must be equal.
Note also that the lemma generalises to any colimit of functors. Unfortunately, no result
analogous to Lemma 4.18 can yet be stated for products.
Our final result considers whether or not there is anything fundamentally special about
the lifting we have constructed. It is clearly the “right” lifting in some sense because it
gives the expected induction rules. But other truth-preserving liftings might also exist and,
if this is the case, then we might hope our lifting satisfies some universal property. In
fact, under a further condition, which is also satisfied by all of the liftings of Hermida and
Jacobs, and which we therefore regard as reasonable, we can show that our lifting is the only
truth-preserving lifting. Our proof uses a line of reasoning which appears in Remark 2.13
in [10].
Lemma 4.19. Let U : E → B be a full Lawvere category and let F be a truth-preserving
lifting of a functor F on B. If F preserves Σ-types — i.e., if (F )(Σf P ) ∼
= ΣF f (F )P
∼
— then F = F̂ .
Proof. We have
(F )P

∼
=
∼
=
∼
=
∼
=

b P)
(F )(Id
(F )(ΣπP K1 {P })
ΣF πP (F )K1 {P }
ΣF πP K1 F {P }

= F̂ P
Finally, we can return to the question of the relationship between the liftings of polynomial
functors given by Hermida and Jacobs and the liftings derived by our methods. We have seen
that for constant functors, the identity functor, and coproducts of functors our constructions
agree. Moreover, since Hermida and Jacobs’ liftings all preserve Σ-types, Lemma 4.19
guarantees that in a full Lawvere category their lifting for products also coincides with
ours.
5. Conclusion and future work
We have given a sound induction rule that can be used to prove properties of data structures
of inductive types. Like Hermida and Jacobs, we give a fibrational account of induction,
but we derive, under slightly different assumptions on fibrations, a generic induction rule
that can be instantiated to any inductive type rather than just to polynomial ones. This
rule is based on initial algebra semantics of data types, and is parameterised over both
the data types and the properties involved. It is also principled, expressive, and correct.

26

N. GHANI, P. JOHANN, AND C. FUMEX

Our derivation yields the same induction rules as Hermida and Jacobs’ when specialised to
polynomial functors in the families fibration over Set and in other fibrations, but it also
gives induction rules for non-polynomial data types such as rose trees, and for data types
such as finite hereditary sets and hyperfunctions, for which no fibrational induction rules
have previously been known to exist.
There are several directions for future work. The most immediate is to instantiate our
theory to give induction rules for more sophisticated data types, such as nested types. These
are exemplified by the data type of perfect trees given in Haskell-like syntax as follows:
data PTree a : Set where
PLeaf : a → PTree a
PNode : PTree (a, a) → PTree a
Nested types arise as least fixed points of rank-2 functors; for example, the type of perfect
trees is µH for the functor H given by HF = λX. X + F (X × X). An appropriate fibration
for induction rules for nested types thus takes B to be the category of functors on Set,
E to be the category of functors from Set to P, and U to be postcomposition with the
forgetful functor from Section 3. A lifting Ĥ of H is given by Ĥ P X (inl a) = 1 and
Ĥ P X (inr n) = P (X × X) n. Taking the premise to be an Ĥ-algebra gives the following
induction rule for perfect trees:
indP T ree : ∀ (P : Set → P).
(U P = PTree) → (∀(X : Set)(x : X). P (PLeaf x)) →
(∀(X : Set)(t : PTree (X × X). P (X × X) t → P (PNode t))) →
∀(X : Set)(t : PTree X). P X t
This rule can be used to show, for example, that P T ree is a functor.
Extending the above instantiation for the codomain fibration to so-called “truly nested
types” [15] and fibrations is current work. We expect to be able to instantiate our theory for
truly nested types, GADTs, indexed containers, dependent types, and inductive recursive
types, but initial investigations show care is needed. We must ascertain which fibrations can
model predicates on such types, since the codomain fibration may not give useful induction
rules, as well as how to translate the rules to which these fibrations give rise to an intensional
setting.
Matthes [15] gives induction rules for nested types (including truly nested ones) in an
intensional type theory. He handles only rank-2 functors that underlie nested types (while
we handle any functor of any rank with an initial algebra), but his insights may help guide
choices of fibrations for truly nested types. These may in turn inform choices for GADTs,
indexed containers, and dependent types.
Induction rules can automatically be generated in many type theories. Within the
Calculus of Constructions [4] an induction rule for a data type can be generated solely
from the inductive structure of that type. Such generation is also a key idea in the Coq
proof assistant [5]. As far as we know, generation can currently be done only for syntactic
classes of functors rather than for all inductive functors with initial algebras. In some
type theories induction schemes are added as axioms rather than generated. For example,
attempts to generate induction schemes based on Church encodings in the Calculus of
Constructions proved unsuccessful and so initiality was added to the system, thus giving the
Calculus of Inductive Constructions. Whereas Matthes’ work is based on concepts such as
impredicativity and induction recursion rather than initial algebras, ours reduces induction

GENERIC FIBRATIONAL INDUCTION

27

to initiality, and may therefore help lay the groundwork for extending implementations of
induction to more sophisticated data types.
Acknowledgement
We thank Robert Atkey, Pierre-Evariste Dagand, Peter Hancock, and Conor McBride for
many fruitful discussions.
References
[1] T. Altenkirch and P. Morris. Indexed Containers. Proceedings, Logic in Computer Science, pp. 277–285,
2009.
[2] R. S. Bird and O. De Moor. Algebra of Programming. Prentice Hall, 1997.
[3] R. Bird and L. Meertens. Nested Datatypes. Proceedings, Mathematics of Program Construction, pp.
52–67, 1998.
[4] T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation 76 (2-3), pp.
95–120, 1988.
[5] The Coq Proof Assistant. Available at coq.inria.fr
[6] P. Dybjer. A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory.
Journal of Symbolic Logic 65 (2), pp. 525–549, 2000
[7] N. Ghani, M. Abbott, and T. Altenkirch. Containers - Constructing Strictly Positive Types. Theoretical
Computer Science 341 (1), pp. 3–27, 2005.
[8] N. Ghani and P. Johann. Foundations for Structured Programming with GADTs. Proceedings, Principles
of Programming Languages, pp. 297–308, 2008.
[9] N. Ghani and P. Johann and C. Fumex. Fibrational Induction Rules for Initial Algebras. Proceedings,
Computer Science Logic, pp. 336–350, 2010.
[10] C. Hermida and B. Jacobs. Structural Induction and Coinduction in a Fibrational Setting. Information
and Computation 145 (2), pp. 107–152, 1998.
[11] B. Jacobs. Comprehension Categories and the Semantics of Type Dependency. Theoretical Computer
Science 107, pp. 169–207, 1993.
[12] B. Jacobs. Categorical Logic and Type Theory. North Holland, 1999.
[13] P. Johann and N. Ghani. Initial Algebra Semantics is Enough! Proceedings, Typed Lambda Calculus
and Applications, pp. 207–222, 2007.
[14] F. W. Lawvere. Equality in Hyperdoctrines and Comprehension Scheme as an Adjoint Functor. Applications of Categorical Algebra, pp. 1–14, 1970.
[15] R. Matthes. An Induction Principle for Nested Datatypes in Intensional Type Theory. Journal of Functional Programming 19 (3&4), pp. 439–468, 2009.
[16] N. P. Mendler. Predicative type universes and primitive recursion. Proceedings, Logic in Computer
Science, pp. 173–184, 1991.
[17] P. Morris. Constructing Universes for Generic Programming. Dissertation, University of Nottingham,
2007.
[18] E. Moggi. Notations of Computation and Monads. Information and Computation 93 (1), pp. 55–92,
1991.
[19] B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf ’s Type Theory. Oxford University Press, 1990.
[20] D. Pavlovič. Predicates and Fibrations. Dissertation, University of Utrecht, 1990.
[21] T. Sheard. Languages of the Future. SIGPLAN Notices 39 (10), pp. 116–119, 2004.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view
a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or
Eisenacher Strasse 2, 10777 Berlin, Germany

