28 May 2020, 16:00, online

Speaker

Stephan Spahn

Title

Reduction of mixed-variance recursion schemes via two-sided fibrations

Abstract

Categorical models of type theories with open terms traditionally have the form of a (Grothendieck) fibration of a total category whose objects interpret types and whose morphism interpret terms fibered over a base category whose objects interpret contexts keeping track of the free variables occurring in types. Defined types (as opposed to type variables) are then interpreted by appropriate universal properties. One particularly convenient such universal property is that of an initial algebra for an endofunctor because the latter can (under certain conditions) be constructed via the initial sequence of the defining ``signature’’ endofunctor. The problem with this is that type definitions in which variables occur with negative variance a priori do not give rise to endofunctors.

As a remedy, several partial solutions to the problem have been proposed: imposing syntactical constraints on the signature endofunctor (cf (strict) positivity), allowing for mixed variance by modifying the notion of algebra but restricting the class of categories containing the model (e.g. to Freyd’s algebraically closed/compact categories), and accommodating mixed variance by using certain dinatural transformations called Mendler algebras [Uustalu] syntactical equivalents to which had been introduced earlier by N.P. Mendler to shape recursion schemes in polymorphic lambda calculus.

We follow Uustalu’s approach to overcome the limitations of earlier attempts to model mixed-variance definitions. In [Uustalu] it was also given a reduction (under certain conditions) of Mendler algebras to algebras for endofunctors; this is important since there is (to our knowledge) no feasible construction of free (including initial) objects in this category of Mendler algebras itself. However, no conceptual reason why this reduction works was given, and this solution -excluding some Mendler-style algebras of more recent interest- seemed specific to Mendler algebras of a certain shape . We show that it is not by giving a definition of generalised Mendler algebras; we take these to be certain indexed dinatural transformations. These form a category appearing as a subcategory (the ‘diagonal’) of a category of diindexed (doubly indexed) dinatural transformations. The latter category has the structure of a two-sided fibration over a base category of carriers, and we show that this fibered structure together with the assumption of fibered initial objects gives rise to a reduction to algebras for an endofunctor on the base category. We observe also that more generally the ‘diagonal’ of every two-sided fibration with fibered initial object is isomorphic to a category of algebras.