nLab free topos

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Contents

Idea

Given a higher-order intuitionistic type theory 𝔏\mathfrak{L}, it is possible to construct a topos T(𝔏)T(\mathfrak{L}) out of the syntax of 𝔏\mathfrak{L}. The free topos T(𝔏 0)T(\mathfrak{L}_0) is the result of this construction when 𝔏 0\mathfrak{L}_0 is ‘pure’ type theory i.e. the only types are 1 (unit type), NN (natural numbers type), and Ω\Omega (type of propositions) lacking relations beyond the bare necessities.

As 𝔏 0\mathfrak{L}_0 is an initial object in the appropriate category of type theories, the free topos T(𝔏 0)T(\mathfrak{L}_0) is itself initial in the corresponding category of toposes (with a natural numbers object) and suitable logical morphisms and is, therefore, also known as the initial topos1.

Properties

The internal language of the free topos is precisely pure (intuitionistic) higher order type theory. In 1978, Jim Lambek and Phil Scott exploited this connection in order to prove properties of intuitionistic type theory by proof-theoretic means. It was observed by Peter Freyd then that the concept of a Freyd cover permits to give conceptual proofs of their findings. The following lemma and proposition is a replication of his ideas.

Lemma

For any category CC with a terminal object 1\mathbf{1}, the terminal object of the Freyd cover C^\widehat{C} is small-projective, i.e., the representable Γ=C^(1,):C^Set\Gamma = \widehat{C}(1, -) \colon \widehat{C} \to Set preserves any colimits that exist.

Proof

To check that Γ op:C^ opSet op\Gamma^{op} \colon \widehat{C}^{op} \to Set^{op} preserves limits, it suffices to check that the composite

C^ opΓ opSet op2 Set\widehat{C}^{op} \stackrel{\Gamma^{op}}{\to} Set^{op} \stackrel{2^-}{\to} Set

preserves limits, because the contravariant power set functor P=2 P = 2^- is monadic. But it is easily checked that this composite is the contravariant representable given by (2,1,2Γ(1))(2, \mathbf{1}, 2 \to \Gamma(\mathbf{1})).

Theorem

The terminal object in the free topos 𝒯\mathcal{T} is connected and projective in the sense that Γ=hom(1,):𝒯Set\Gamma = \hom(1, -) \colon \mathcal{T} \to Set preserves finite colimits.

Proof

We divide the argument into three segments:

  • The hom-functor preserves finite limits, so by general properties of Artin gluing, the Freyd cover 𝒯^\widehat{\mathcal{T}} is also a topos. Observe that 𝒯\mathcal{T} is equivalent to the slice 𝒯^/M\widehat{\mathcal{T}}/M where MM is the object (,1,Γ(1))(\emptyset, \mathbf{1}, \emptyset \to \Gamma(\mathbf{1})). Since pulling back to a slice is a logical functor, we have a logical functor

    π:𝒯^𝒯\pi \colon \widehat{\mathcal{T}} \to \mathcal{T}

    Since 𝒯\mathcal{T} is initial, π\pi is a retraction for the unique logical functor i:𝒯𝒯^i \colon \mathcal{T} \to \widehat{\mathcal{T}}.

  • We have maps 𝒯(1,)𝒯^(i1,i)𝒯^(1,i)\mathcal{T}(1, -) \to \widehat{\mathcal{T}}(i 1, i-) \cong \widehat{\mathcal{T}}(1, i-) (the isomorphism comes from i11i 1 \cong 1, which is clear since ii is logical), and 𝒯^(1,i)𝒯(π1,πi)𝒯(1,)\widehat{\mathcal{T}}(1, i-) \to \mathcal{T}(\pi 1, \pi i-) \cong \mathcal{T}(1, -) since π\pi is logical and retracts ii. Their composite must be the identity on 𝒯(1,)\mathcal{T}(1, -), because there is only one such endomorphism, using the Yoneda lemma and terminality of 11.

Finally, since 𝒯(1,)\mathcal{T}(1, -) is a retract of a functor 𝒯^(1,i)\widehat{\mathcal{T}}(1, i-) that preserves finite colimits (by the lemma, and the fact that the logical functor ii preserves finite colimits), it must also preserve finite colimits.

This is important because it implies that the internal logic of the free topos satisfies the following properties:

  • The disjunction property: if “P or Q” is provable in the empty context, then either P is so provable, or Q is so provable. (Note that this clearly fails in the presence of excluded middle.)

  • The existence property: if “there exists an xAx\in A such that P(x)P(x)” is provable in the empty context, then there exists a global element x:1Ax\colon 1\to A such that P(x)P(x) is provable in the empty context. (Again, this is clearly a constructivity property.)

  • The negation property: False is not provable in the empty context.

  • All numerals in the free topos are “standard”, i.e., the global sections functor Γ=hom(1,):𝒯Set\Gamma = \hom(1, -): \mathcal{T} \to Set preserves the natural numbers object NN (because NN can be characterized in terms of finite colimits and 11, by a theorem of Freyd).

Foundations

In the foundations of mathematics, Jim Lambek proposed to use the free topos as ambient world to do mathematics in; see (Lambek 2004). Being syntactically constructed, but universally determined, with higher-order intuitionistic type theory as internal language he saw it as a reconciliation of the three classical schools of philosophy of mathematics, namely formalism, platonism, and intuitionism. His latest views on this variant of categorical foundations can be found in (Lambek-Scott 2011).

Remark: Two properties of the free topos

Lambek and Scott mention in their 1986 monograph (pp.viii, 233, 250) two further remarkable properties of the free topos 𝒯\mathcal{T}:

  • All maps RRR\to R in the free topos represent continuous functions. Note that this is not the same as to say that Brouwer’s theorem (“all functions RRR\to R are continuous”) is true in the free topos, which is not the case.

  • The natural numbers object NN is an (external) projective object.

The first result is attributed to André Joyal, presumably unpublished, and for the second claim they refer to an unpublished manuscript by Michael Makkai and a manuscript by Friedman and Scedrov, presumably (1983).

References

The free topos was first constructed by H. Volger. A second construction appears in

  • Jim Lambek, From Types to Sets , JPAA 36 (1980) pp.113-164.

Freyd’s proof of the above properties appears first in

On the relation between the proof and the topos-theoretic techniques in the proof see

  • A. Scedrov, Phil Scott, A note on the Friedman Slash and Freyd Covers , pp. 443-452 in The LEJ Brouwer Centenary Symposium , North Holland Amsterdam 1982.

  • Jim Lambek, Phil Scott, New proofs of some intuitionistic principles , Zeit. für Math. Logik 29 (1983) pp. 493-504.

For textbook accounts of the free topos see

For dependent choice in intuitionistic type theory:

  • H. M. Friedman, A. Scedrov, Set existence property for intuitionistic theories with dependent choice , APAL 25 no.2 (1983) pp.129-140.

For J. Lambek’s views on the role of the free topos in foundations of mathematics see:

  • J. Couture, Jim Lambek, Philosophical Reflections on the Foundations of Mathematics , Erkenntnis 34 (1991) pp.187-209.

  • Jim Lambek, Are the traditional philosophies of mathematics really incompatible? , Math. Intelligencer 16

    (1994) pp.56–62.

  • Jim Lambek, What is the world of mathematics? , APAL 126 (2004) pp.149-158. (draft)

  • Jim Lambek, Phil Scott, Reflections on Categorical Foundations of Mathematics , pp.171-185 in Sommaruga (ed.), Foundational Theories of Classical and Constructive Mathematics, Springer New York 2011. (draft)


  1. This is not to be confounded with the gadget of the same name in SGA4 (1972, p.313) i.e. the topos sh()sh(\emptyset) of sheaves on the empty topological space aka the one point category, also called the empty topos there. In this context the appropriate maps are geometric morphisms.

Last revised on January 9, 2019 at 14:58:25. See the history of this page for a list of all contributions to it.