Pith. sign in

REVIEW

Chu representations of categories related to constructive mathematics

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2106.01878 v1 pith:FGQ7K2OA submitted 2021-06-03 math.CT

classification math.CT
keywords categorycomplementedconstructionbishopclosedconstructiverepresentationsubsets
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original 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.

Discussion (0). Continue with ORCID to comment.

Pith tools