## Math and Logic

### 2012

##### Abstract

We present a new model of computation, described in terms of monoidal
categories. It conforms the Church-Turing Thesis, and captures the
same computable functions as the standard models. It provides a
succinct categorical interface to most of them, free of their diverse
implementation details, using the ideas and structures that in the
meantime emerged from research in semantics of computation and
programming. The salient feature of the language of monoidal
categories is that it is supported by a sound and complete graphical
formalism, string diagrams, which provide a concrete and intuitive
interface for abstract reasoning about computation. The original
motivation and the ultimate goal of this effort is to provide a
convenient high level programming language for a theory of
computational resources, such as one-way functions, and trapdoor
functions, by adopting the methods for hiding the low level
implementation details that emerged from practice. Only a modest first
step towards this ambitious goal is presented.

### 2008

##### Abstract

We show that an orthogonal basis for a
finite-dimensional Hilbert space can be equivalently characterised as
a commutative dagger-Frobenius monoid in the category FHilb, which
has finite-dimensional Hilbert spaces as objects and continuous linear
maps as morphisms, and tensor product for the monoidal structure. The
basis is normalised exactly when the corresponding commutative
dagger-Frobenius monoid is special. Hence orthogonal and orthonormal
bases can be axiomatised in terms of composition of operations and
tensor product only, without any explicit reference to the underlying
vector spaces. This axiomatisation moreover admits an operational
interpretation, as the comultiplication copies the basis vectors and
the counit uniformly deletes them. That is, we rely on the distinct
ability to clone and delete classical data as compared to quantum data
to capture basis vectors. For this reason our result has important
implications for categorical quantum mechanics.

### 1996

##### Abstract

In categorical proof theory, propositions and proofs are presented as
objects and arrows in a category. It thus embodies the strong
constructivist paradigms of propositions-as-types and
proofs-as-constructions, which lie in the foundation of computational
logic. Moreover, in the categorical setting, a third paradigm arises,
not available elsewhere: logical-operations-as-adjunctions. It offers
an answer to the notorious question of the equality of proofs. Diagram
chasing comes about in algebra of proofs.
On the basis of these ideas, the present paper investigates proof
theory of regular logic: the {\and,\exists}-fragment of the
first order logic with equality. The corresponding categorical
structure is regular fibration. The examples include stable
factorisations, sites, triposes. Regular logic is exactly what is
needed to talk about maps, as total and single-valued relations.
However, when enriched with proofs-as-arrows, this familiar concept
must be supplied with an additional conversion rule, connecting the
proof of the totality with the proof of the single-valuedness. We
explain the logical meaning of this rule, and then determine precise
conditions under which a regular fibration supports the principle of
function comprehension (that each map corresponds to a unique function
viz arrow in the base), thus lifting a basic theorem from regular
categories (that Map(Rel(C) = C), which was recently relativized to
factorisation systems. The obtained results open an interesting
possibility of extending the P-set construction from triposes to
non-posetal fibrations.

### 1995

##### Abstract

The 4-Colour Theorem has been proved in the late seventies , after
more than a century of fruitless efforts. But the proof has provided
very little new information about the map colouring itself. While
trying to understand this phenomenon, we analyze colouring in terms of
universal properties and adjoint functors.
It is well known that the 4-colouring of maps is equivalent to the
3-colouring of the edges of some graphs. We show that every slice of
the category of 3-coloured graphs is a topos. The forgetful functor
to the category of graphs is cotripleable; every loop-free graph is
covered by a 3-coloured one in a universal way. In this context, the
4-Color Theorem becomes a statement about the existence of coalgebra
structure on graphs.

In a sense, this approach seems complementary to the known
combinatorial colouring procedures.

##### Abstract

The simple connection of completeness and cocompleteness of lattices
grows in categories into the Adjoint Functor Theorem. The connection
of completeness and cocompleteness of Boolean algebras - even simpler
- is similarly related to Pare's Theorem for toposes. We explain
these relations and then study the fibrational versionso of both
theorems, for small complete categories. They can be interpreted as
definability results in logic with proofs-as-constructions, and
transferred into type theory.

##### Abstract

Originally, categorical calculus of relations was developed using the
canonical factorisations in regular categories. More recently,
relations restricted to a proper factorisation systems have been
studied by several authors. In the present paper, we consider the
general situation, where relations are induced by an arbitrary stable
factorisation. This extension of the calculus of relations is
necessary for categorical development of strongly constructivist
logic, and of semantics of computation, where non-monic relations come
about naturally.
In this setting we analyze the correspondence of * maps*,
i.e. the total, single-valued relations, and *functions*, as
given by the arrows of the underlying category.

### 1993

##### Abstract

We study three comonads derived from the comma construction. The
induced coalgebras correspond to the three concepts displayed in the
title of the paper. The comonad that yields the cofree *-autonomous
categories is, in essence, the Chu construction, which has recently
awaken much interest in computer science. We describe its couniversal
property. It is right adjoint to the inclusion of *-autonomous
categories among autonomous categories, with lax structure-preserving
morphisms. Moreover, this inclusion turns out to be comonadic:
*-autonomous categories are exactly the Chu-coalgebras.

### 1992

##### Abstract

Paradox is a logical phenomenon. Usually, it
is produced in type theory, over a type of "truth values". A formula
p, as a term p:Prop is constructed, such that p is equivalent to its
negation - whereupon everything can be proved. We describe a general
pattern which many constructions of the formula follow: for example,
the well known arguments of Cantor, Russell, and Goedel. We generalize
their common underlying structure, and prove that Reynolds'
construction of the type isomorphic to its second power type, contrary
to his conjecture, cannot be extended to give a fixed point of every
variable type derived from exponentiation. In particular, for
contravariant types, such a fixed point would lead to a paradox.

### 1991

##### Abstract

In this paper, Coquand and Huet's Theory of
Constructions is reinterpreted as a type theory of "sets" and
"predicates". Following some set-theoretical intuitions, this popular
type system is modified at two points: (1) a simple new operation is
added - to represent a constructive version of the comprehension
principle; (2) a restriction on contexts is imposed - "sets" must not
depend on "proofs" of "predicates". The resulting theory is called
Theory of Predicates. Sufficiently constructive arguments from naive
set theory can be directly written down in it. On the other hand,
modification (2) is relevant from a computational point of view, since
it corresponds to a necessary condition of the modular approach to
programming.
Our main result tells that, despite (2), Theory of Predicates is
as expressive as Theory of Constructions: the type constructors
preempted by (2) are recovered in an isomorphic form using (1). In
fact, Theory of Constructions is equivalent to a quotient of Theory of
Predicates.

### 1990

##### Abstract

Fibred categories have been introduced by
Grothendieck (1959, 1970) as the setting for his theory of
descent. The present paper contains (in section 4) a characterisation
of the effective descent morphisms under an arbitrary fibred
category. This essentially geometric result complements a logical
analysis of the Beck-Chevalley property (presented in section 1). This
property was crucial in the well-known theorem on sufficient
conditions for the descent under bifibrations, due to Benabou and
Roubaud (1970) and Beck (unpublished). We describe the notion of
*interpolant* as the common denominator of the concepts of
descent and the Beck-Chevalley property.

##### Abstract

The commonplace simplification of constructivist logic as a logic
without the excluded middle conceals a more authentic idea of
constructivism: that proofs are constructive functions, while the
quantifiers should be sums and products. An exact realisation of this
idea requires a very special mathematical setting. Expressed
categorically, the idea is that there is a small category (of
"propositions" and "proofs"), with all small sums and products (as
"quantifiers"). In ordinary category theory (or over a Grothendieck
topos) such a category must be a preorder, and there can be at most
one "proof" leading from one "proposition" to another. In Hyland's
Effective Topos, however, a nondegenerate small complete category has
been discovered recently. It can be regarded as the first mathematical
model of logic with constructive proofs. On the other hand, a
significant impluse to a formal development of such logics came from
Computer Science, especially through the work of Coquand, Huet and
their collaborators on the Calculus of Constructions.
In this thesis, we consider two mathematical formulations of
constructivist logic: a type theoretical and a category
theoretical. In the end, the former is completely interpreted in the
latter. The purpose of such a connection is to yield a
characterisation of type theoretic *structures* by categorical *properties*.