We introduce the notion of a relative pseudomonad, which generalises the
notion of a pseudomonad, and define the Kleisli bicategory associated to a
relative pseudomonad. We then present an efficient method to define pseudomonas
on the Kleisli bicategory of a relative pseudomonad. The results are applied to
define several pseudomonads on the bicategory of profunctors in an homogeneous
way, thus providing a uniform approach to the definition of bicategories that
are of interest in operad theory, mathematical logic, and theoretical computer
We develop further the theory of weak factorization systems and algebraic
weak factorization systems. In particular, we give a method for constructing
(algebraic) weak factorization systems whose right maps can be thought of as
(uniform) fibrations and that satisfy the (functorial) Frobenius condition. As
applications, we obtain a new proof that the Quillen model structure for Kan
complexes is right proper, avoiding entirely the use of topological realization
and minimal fibrations, and we solve an open problem in the study of
Voevodsky's simplicial model of type theory, proving a constructive version of
the preservation of Kan fibrations by pushforward along Kan fibrations. Our
results also subsume and extend work by Coquand and others on cubical sets.
We develop further the theory of operads and analytic functors. In
particular, we introduce a bicategory that has operads as 0-cells, operad
bimodules as 1-cells and operad bimodule maps as 2-cells, and prove that this
bicategory is cartesian closed. In order to obtain this result, we extend the
theory of distributors and the formal theory of monads.
We investigate inductive types in type theory, using the insights provided by
homotopy type theory and univalent foundations of mathematics. We do so by
introducing the new notion of a homotopy-initial algebra. This notion is
defined by a purely type-theoretic contractibility condition which replaces the
standard, category-theoretic universal property involving the existence and
uniqueness of appropriate morphisms. Our main result characterises the types
that are equivalent to W-types as homotopy-initial algebras.
Homotopy type theory is an interpretation of Martin-L\"of's constructive type
theory into abstract homotopy theory. There results a link between constructive
mathematics and algebraic topology, providing topological semantics for
intensional systems of type theory as well as a computational approach to
algebraic topology via type theory-based proof assistants such as Coq.
The present work investigates inductive types in this setting. Modified rules
for inductive types, including types of well-founded trees, or W-types, are
presented, and the basic homotopical semantics of such types are determined.
Proofs of all results have been formally verified by the Coq proof assistant,
and the proof scripts for this verification form an essential component of this
We characterize double adjunctions in terms of presheaves and universal
squares, and then apply these characterizations to free monads and
Eilenberg--Moore objects in double categories. We improve upon our earlier
result in "Monads in Double Categories", JPAA 215:6, pages 1174-1197, 2011, to
conclude: if a double category with cofolding admits the construction of free
monads in its horizontal 2-category, then it also admits the construction of
free monads as a double category. We also prove that a double category admits
Eilenberg--Moore objects if and only if a certain parameterized presheaf is
representable. Along the way, we develop parameterized presheaves on double
categories and prove a double-categorical Yoneda Lemma.
We extend the basic concepts of Street's formal theory of monads from the
setting of 2-categories to that of double categories. In particular, we
introduce the double category Mnd(C) of monads in a double category C and
define what it means for a double category to admit the construction of free
monads. Our main theorem shows that, under some mild conditions, a double
category that is a framed bicategory admits the construction of free monads if
its horizontal 2-category does. We apply this result to obtain double
adjunctions which extend the adjunction between graphs and categories and the
adjunction between polynomial endofunctors and polynomial monads.
We study polynomial functors over locally cartesian closed categories. After
setting up the basic theory, we show how polynomial functors assemble into a
double category, in fact a framed bicategory. We show that the free monad on a
polynomial endofunctor is polynomial. The relationship with operads and other
related notions is explored.
We survey the development of the formal theory of pseudo-monads, the analogue
for pseudo-monads of the formal theory of monads. One of the main achievements
of the theory is a satisfactory axiomatisation of the notion of a
pseudo-distributive law between pseudo-monads.
We present a solution to the problem of defining a counterpart in Algebraic
Set Theory of the construction of internal sheaves in Topos Theory. Our
approach is general in that we consider sheaves as determined by
Lawvere-Tierney coverages, rather than by Grothendieck coverages, and assume
only a weakening of the axioms for small maps originally introduced by Joyal
and Moerdijk, thus subsuming the existing topos-theoretic results.
We show that the classifying category C(T) of a dependent type theory T with
axioms for identity types admits a non-trivial weak factorisation system. We
provide an explicit characterisation of the elements of both the left class and
the right class of the weak factorisation system. This characterisation is
applied to relate identity types and the homotopy theory of groupoids.