
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
science.

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 0cells, operad
bimodules as 1cells and operad bimodule maps as 2cells, 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 homotopyinitial algebra. This notion is
defined by a purely typetheoretic contractibility condition which replaces the
standard, categorytheoretic universal property involving the existence and
uniqueness of appropriate morphisms. Our main result characterises the types
that are equivalent to Wtypes as homotopyinitial algebras.

Homotopy type theory is an interpretation of MartinL\"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 theorybased proof assistants such as Coq.
The present work investigates inductive types in this setting. Modified rules
for inductive types, including types of wellfounded trees, or Wtypes, 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
research.

We characterize double adjunctions in terms of presheaves and universal
squares, and then apply these characterizations to free monads and
EilenbergMoore objects in double categories. We improve upon our earlier
result in "Monads in Double Categories", JPAA 215:6, pages 11741197, 2011, to
conclude: if a double category with cofolding admits the construction of free
monads in its horizontal 2category, then it also admits the construction of
free monads as a double category. We also prove that a double category admits
EilenbergMoore objects if and only if a certain parameterized presheaf is
representable. Along the way, we develop parameterized presheaves on double
categories and prove a doublecategorical Yoneda Lemma.

We extend the basic concepts of Street's formal theory of monads from the
setting of 2categories 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 2category 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 pseudomonads, the analogue
for pseudomonads of the formal theory of monads. One of the main achievements
of the theory is a satisfactory axiomatisation of the notion of a
pseudodistributive law between pseudomonads.

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
LawvereTierney 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 topostheoretic results.

We show that the classifying category C(T) of a dependent type theory T with
axioms for identity types admits a nontrivial 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.