Chu representations of categories related to constructive mathematics

TL;DR

This paper explores Chu representations of categories related to constructive mathematics, establishing embeddings of complemented subsets and Bishop spaces into Chu categories, and generalizing the Chu construction for various categorical contexts.

Contribution

It demonstrates Chu representations of complemented subsets and Bishop spaces, and generalizes the Chu construction to broader categorical frameworks in constructive mathematics.

Findings

Chu representation of complemented subsets into Chu(Set, X×X)

Chu representation of Bishop spaces into Chu(Set, R)

Generalization of Chu construction over cartesian closed categories

Abstract

If C is a closed symmetric monoidal category, the Chu category Chu(C, g) over C and an object g of it was defined by Chu, as a *-autonomous category generated from C. Bishop introduced the category of complemented subsets of a set, in order to overcome the problems generated by the use of negation in constructive measure theory. Shulman mentions that Bishop's complemented subsets correspond roughly to the Chu construction. In this paper we explain this correspondence by showing that there is a Chu representation (a full embedding) of the category of complemented subsets of a set X into Chu(Set, X x X). A Chu representation of the category of Bishop spaces into Chu(Set, R) is shown, as the constructive analogue to the standard Chu representation of the category of topological spaces into Chu(Set, 2). In order to represent the category of predicates (with objects pairs (X, A), where A is a subset of X, and the category of complemented predicates (with objects pairs (X, A), where A is a complemented subset of X, we generalise the Chu construction by defining the Chu category over a cartesian closed category C and an endofunctor on C. Finally, we introduce the antiparallel Grothendieck construction over a product category and a contra-variant Set-valued functor on it of which the Chu construction is a special case, in case C is a locally small, cartesian closed category.