arXiv subjects

Edward Morehouse

Publications and source records attributed to Edward Morehouse.

5 recordsLinked to original sources

arXiv2026

Dinaturality for Double Categories

In this paper we extend the concept of dinaturality to the setting of double categories. We introduce the dinatural versions of double-categorical transformations and modifications, and show that ordinary natural transformations and modifications correspond to dinatural ones between dummy functors. Although dinatural transformations don't generally compose with each other, they do compose with natural transformations, and we investigate the algebra of this composition. In our motivating example of dinaturality for double categories, we derive the caps and cups of Eilenberg-Kelly graphs for extranatural transformations as dinatural transformation components, and the corresponding adjunction laws as (di)modification components. In an appendix we extend the surface diagram calculus for the locally cubical Gray category of small double categories to include dinatural constructions.

math.CT↗

arXiv2023

Cartesian Gray-Monoidal Double Categories

In this paper we present cartesian structure for symmetric Gray-monoidal double categories. To do this we first introduce locally cubical Gray categories, which are three-dimensional categorical structures analogous to classical, locally globular, Gray categories. The motivating example comprises double categories themselves, together with their functors, transformations, and modifications. A one-object locally cubical Gray category is a Gray-monoidal double category. Braiding, syllepsis, and symmetry for these is introduced in a manner analogous to that for 2-categories. Adding cartesian structure requires the introduction of doubly-lax functors of double categories to manage the order of copies. The resulting theory is algebraically rather complex, largely due to the bureaucracy of linearizing higher-dimensional boundary constraints. Fortunately, it has a relatively simple and compelling representation in the graphical calculus of surface diagrams, which we present.

math.CT↗

arXiv2022

$2$-Categories from a Gray Perspective

In this paper we present $2$-category theory from the perspective of Gray-categories using the graphical calculus of separated surface diagrams. As an extended example we consider cones and limits of $2$-functors. Then we use the canonical adjunction between $2$-computads and $2$-categories to interpret the comparison structure of lax functors and extend the surface diagram calculus with compositor sheets in order to represent and reason about them.

math.CT↗

arXiv2019

Recurrence Extraction for Functional Programs through Call-by-Push-Value (Extended Version)

The main way of analyzing the complexity of a program is that of extracting and solving a recurrence that expresses its running time in terms of the size of its input. We develop a method that automatically extracts such recurrences from the syntax of higher-order recursive functional programs. The resulting recurrences, which are programs in a call-by-name language with recursion, explicitly compute the running time in terms of the size of the input. In order to achieve this in a uniform way that covers both call-by-name and call-by-value evaluation strategies, we use Call-by-Push-Value (CBPV) as an intermediate language. Finally, we use domain theory to develop a denotational cost semantics for the resulting recurrences.

cs.PL↗

arXiv2017

Varieties of Cubical Sets

We define a variety of notions of cubical sets, based on sites organized using substructural algebraic theories presenting PRO(P)s or Lawvere theories. We prove that all our sites are test categories in the sense of Grothendieck, meaning that the corresponding presheaf categories of cubical sets model classical homotopy theory. We delineate exactly which ones are even strict test categories, meaning that products of cubical sets correspond to products of homotopy types.

math.CT↗