# Topos Theory and Constructive Logic Papers

## Andreas Blass

Papers on linear logic are on a separate
page.

The interaction between category theory and set theory (in
"Mathematical Applications of Category Theory," edited by J. Gray,
Contemporary Mathematics 30 (1984) 5--29)

PDF
This paper is based on a lecture about the various connections between
category theory and set theory. Some interactions arise from set
theory's foundational role in mathematics. Others arise from
category theory's role of clarifying and unifying concepts in many
areas of mathematics. We also discuss categories with set-theoretic
structure, primarily topoi, and some suggestive but not fully
understood connections between particular topics in set theory and
category theory.

I thank Dave Childs for producing an electronic version of this
paper.

An induction principle and pigeonhole principle for K-finite sets
(J. Symbolic Logic 59 (1995) 1186--1193)

PostScript
or
PDF

We establish a course-of-values induction principle for K-finite sets
in intuitionistic type theory. Using this principle, we prove a
pigeonhole principle conjectured by Benabou and Loiseau. We also
comment on some variants of this pigeonhole principle.

Seven trees in one (J. Pure Appl. Alg. 103 (1995) 1-21)

PostScript
or
PDF

Following a remark of Lawvere, we explicitly exhibit a
particularly elementary bijection between the set T of
finite binary trees and the set T^7 of seven-tuples of
such trees. "Particularly elementary" means that the
application of the bijection to a seven-tuple of trees
involves case distinctions only down to a fixed depth
(namely four) in the given seven-tuple. We clarify how
this and similar bijections are related to the free
commutative semiring on one generator X subject to
X=1+X^2. Finally, our main theorem is that the
existence of particularly elementary bijections can be
deduced from the provable existence, in intuitionistic
type theory, of any bijections at all.

Topoi and Computation (Bull. European Assoc. Theoret. Comp. Sci. 36
(1988) 57-65)

PostScript
or
PDF

This is the written version of a talk given at the C.I.R.M. Workshop
on Logic in Computer Science at Marseille in June, 1988. Its
purpose is to argue that there is a close connection between the
theory of computation and the geometric side of topos theory. We
begin with a brief outline of the history and basic concepts of topos
theory.