Claudio Hermida

PREPRINTS:

• indeter.pdf Monoidal indeterminates and categories of possible worlds (with R.D.Tennent)
  presented at MFPS XXV, Oxford, April 2009, extended version to apper in special issue of Theoretical Computer Science, 2011.
  Abstract: Given any symmetric monoidal category $C$, a small symmetric monoidal category $\Sigma$ and a strong monoidal functor $j:\Sigma \to C$, it is shown how to construct $C[x:j\Sigma ]$, a polynomial such category, the result of freely adjoining to $C$ a system $x$ of monoidal indeterminates for every object $j(w)$ with $w\in \Sigma$ satisfying a naturality constraint with the arrows of $\Sigma$. As a special case, we show how to construct the free co-affine category (symmetric monoidal category with initial unit) on a given small symmetric monoidal category. It is then shown that all the known categories of "possible worlds" used to treat languages that allow for dynamic creation of "new" variables, locations, or names are in fact instances of this construction and hence have appropriate universality properties.

• fib.pdf A fibrational framework for possible-world semantics of ALGOL-like langauges (with R.D.Tennent)
  revised version in TCS, 375 (1-3), p. 3-19, 2007
  We reorganize a functor category [W,S] into a fibration over W using slices, and extend the construction to a fibration of fibrations, in line with the general setting for the relational parametric semantics of polymorphic lambda calculi.

• roadmap.ps /pdf A roadmap to the unification of weak categorical structures: transformations and equivalences among the various notions of pseudo-algebra (June 2004)
  A quick tour of the constructions/equivalences monoidal category :: representable multicategory :: covariantly fibrant multicategory :: pseudo-monoid in Cat, and their general pseudo-algebra versions.

• paracategories-2.ps /pdf Paracategories II: Adjunctions, fibrations and examples from probabilistic automata theory by C. Hermida and P. Mateus
  revised version in Theoretical Computer Science, 311, 71-103, 2004.
  Abstract: In this sequel to Paracategories I, we explore some of the global aspects of the category of paracategories. We establish its (co)completeness and cartesian closure. From the closed structure we derive the relevant notion of transformation for paracategories. We set up the relevant notion of adjunction between paracategories and apply it to define (co)completeness and cartesian closure, exemplified by the paracategory of bivariant functors and dinatural transformations. We introduce partial multicategories to account for partial tensor products. We also consider fibrations for paracategories and their indexed-paracategory version. Finally, we instantiate all these concepts in the context of probabilistic automata.

• paracategories-1.ps /pdf Paracategories I: Internal Paracategories and Saturated Partial Algebras by C. Hermida and P. Mateus (revised version in Theoretical Computer Science, 309, 125-156 2003 ).
  Abstract: Based on the monoid classif{i}er, we give an alternative axiomatization of Freyd's paracategories, which can be interpreted in any bicategory of partial maps. Assuming furthermore a free-monoid monad T in our ambient category, and coequalisers satisfying some exactness conditions, we give an abstract envelope construction, putting paramonoids (and paracategories) in the more general context of partial algebras. We introduce for the latter the crucial notion of saturation, which characterises those partial algebras which are isomorphic to the ones obtained from their enveloping lgebras. We also set up a factorisation system for partial algebras, via epimorphisms and (monic) Kleene morphisms and relate the latter to saturation.

• 2-descent.pdf Descent on 2-fibrations and 2-regular 2-categories (revised version in Applied Categorical Structures, 12(5-6), 427--459, 2004).

  Abstract: We consider pseudo-descent in the context of 2-fibrations. A 2-category of descent data is associated to a 3-truncated simplicial object in the base 2-category. A morphism q in the base induces (via comma-objects and pullbacks) an internal category whose truncated nerve allows the definition of the 2-category of descent data for q. When the 2-fibration admits direct images, we provide the analogous of the Beck-Benabou-Roubaud theorem, identifying the 2-category of descent data with that of pseudo-algebras for the pseudo-monad q^*Σ_q. We introduce a notion of 2-regularity for a 2-category R, so that its basic 2-fibration of internal fibrations cod: Fib(R)→Radmits direct images. In this context, we show that essentially-surjective-on-objects morphisms, defined by a certain lax colimit, are of effective descent by means of a Beck-style pseudo-monadicity theorem.

• rep-mult.ps Representable multicategories (version June 8, 1999 , Revised in Advances in Mathematics 151, p.164-225).
  Abstract: We introduce the notion of representable multicategory, which stands in the same relation to that of monoidal category as fibration does to contravariant pseudofunctor (into Cat). We give an abstract reformulation of multicategories as monads in a suitable Kleisli bicategory of spans. We describe representability in elementary terms via universal arrows. We also give a doctrinal characterisation of representability based on a fundamental monadic adjunction between the 2-category of multicategories and that of strict monoidal categories. The first main result is the coherence theorem for representable multicategories, asserting their equivalence to strict ones, which we establish via a new technique based on the above doctrinal characterisation. The other main result is a 2-equivalence between the 2-category of representable multicategories and that of monoidal categories and strong monoidal functors. This correspondence extends smoothly to one between bicategories and a localised version of representable multicategories.
  
• coh-univ.ps From coherent structures to universal properties (version March, 2000; final version in in Journal of Pure and Applied Algebra 165 (1),7-61,2001).
  Abstract: Given a 2-category K admitting a calculus of bimodules, and a 2-monad T on it compatible with such calculus, we construct a 2-category L with a 2-monad S on it such that: i) S has the adjoint-pseudo-algebra property. ii) The 2-categories of pseudo-algebras of S and T are equivalent. Thus, coherent structures (pseudo-T-algebras) are transformed into universally characterised ones (adjoint-pseudo-S-algebras). The 2-category L consists of lax algebras for the pseudo-monad induced by T on the bicategory of bimodules of K. We give an intrinsic characterisation of pseudo-S-algebras in terms of {\em representability\/}. Two major consequences of the above transformation are the classifications of lax and strong morphisms, with the attendant coherence result for pseudo-algebras. We apply the theory in the context of internal categories and examine monoidal and monoidal globular categories (including their {\em monoid classifiers\/}) as well as pseudo-functors into Cat

• jpaa.ps.gz Some Properties of Fib as a fibred 2-category (revised version in Journal of Pure and Applied Algebra 134 (1), 83-109, 1999).
  Abstract: We consider some basic properties of the 2-category Fib of fibrations over arbitrary bases, exploiting the fact that it is fibred over Cat . We show a factorisation property for adjunctions in Fib, which has direct consequences for fibrations, eg. a characterisation of limits and colimits for them. We also consider oplax colimits in Fib, with the construction of Kleisli objects as a particular example. All our constructions are based on an elementary characterisation of Fib as a 2-fibration.
  

• Inf-and-Comp.ps Structural Induction and Coinduction in a fibrational setting by C. Hermida and B. Jacobs (revised version in Information and Computation 145 (2), 107--152, 1998).
  Abstract: We present a categorical logic formulation of induction and coinduction principles for reasoning about inductively and coinductively defined types. Our main results provide sufficient criteria for the validity of such principles: in the presence of comprehension, the induction principle for initial algebras is admissible, and dually, in the presence of quotient types, the coinduction principle for terminal coalgebras is admissible. After giving an alternative formulation of induction in terms of binary relations, we combine both principles and obtain a mixed induction/coinduction principle which allows us to reason about minimal solutions $X\cong\sigma(X)$ where $X$ may occur both positively and negatively in the type constructor $\sigma$. We further strengthen these logical principles to deal with contexts and prove that such strengthening is valid when the (abstract) logic we consider is contextually/functionally complete. All the main results follow from a basic result about adjunctions between `categories of algebras' (inserters).

• comp-fact.ps A note on comprehensive factorisation (after Pare, Street and Walters)

• sat-sim-IandC.pdf (DRAFT) A categorical outlook on relational modalities and simulations presented at IMLA'02.(extended version invited for special issue of Information and Computation on Intuitionistic Modal Logics and Applications, 2011 )
  Abstract: We characterise bicategories of spans, relations and partial maps universally in terms of factorisations involving maps . We apply this universal characterisation to show that the standard modalities $\square$ and $◊$ arise canonically as extensions of a predicate logic from functions to (abstract) relations . When relations and partial maps are representable, we exhibit logical predicates for the power-object and partial-map-classifier monads. We also show that the $\square$ modality produces the relevant pullbacks of subobjects in the internal logic of categories of partial maps. Organizing modal formulae fibrationally, we exhibit an intrinsic relationship between their satisfaction relative to transition systems and the notion of (op)simulation. In this setting, we use the biclosed nature of the bicategory of relations to give a new proof that observational (op)similarity implies (op)similarity.

• col-dec.ps (DRAFT) Colimit decomposition for diagrams indexed by a cofibred category
  Abstract: We characterise small cocompleteness for a category as a 2-adjoint. We apply this to give a colimit decomposition for diagrams indexed by a cofibration.