nLab local geometric morphism

Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Discrete and concrete objects

Contents

Definition

Local geometric morphism and relative local topos

Definition

A local geometric morphism f:ESf : E \to S between toposes E,SE,S is

  • a geometric morphism

    (f *f *):Ef *f *S (f^* \dashv f_*) \colon E \stackrel{\overset{f^*}{\leftarrow}}{\underset{f_*} {\to}} S
  • such that a further right adjoint f !:SEf^! : S \to E exists

    (f *f *f !):Ef !f *f *S (f^* \dashv f_* \dashv f^!) : E \stackrel{\overset{f^*}{\longleftarrow}}{\stackrel{\underset{f_*}{\longrightarrow}}{\underset{f^!}{\longleftarrow}}} S
  • and such that one, hence all, of the following equivalent conditions hold:

    1. The right adjoint f !f^! is an SS-indexed functor.
    2. ff is connected, i.e. f *f^* is fully faithful.
    3. The right adjoint f !f^! is fully faithful.
    4. The right adjoint f !f^! is cartesian closed.

When we regard EE as a topos over SS, so that ff is regarded as its global section geometric morphism in the category of toposes over SS, then we say that EE is a local SS-topos. In this case we may label the functors involved as

(DiscΓCodisc):ECodiscΓDiscS (Disc \dashv \Gamma \dashv Codisc) : E \stackrel{\overset{Disc}{\longleftarrow}}{\stackrel{\underset{\Gamma}{\longrightarrow}}{\underset{Codisc}{\longleftarrow}}} S

to indicate that if we think of Γ\Gamma as sending a space to its underlying SS-object of points by forgetting cohesion, then DiscDisc creates the discrete space/discrete object and CodiscCodisc the codiscrete space/codiscrete object on an object in SS.

This is especially common when S=S= Set, in which case the final condition is automatic since all functors are SetSet-indexed. Hence in that case we have the following simpler definition.

Local topos

Definition

A sheaf topos 𝒯\mathcal{T} is a local topos if the global section geometric morphism 𝒯ΓLConstSet\mathcal{T} \stackrel{\overset{LConst}{\leftarrow}}{\underset{\Gamma}{\to}} Set has a further right adjoint CoDiscCoDisc, making an adjoint triple (LConstΓCoDisc)(LConst \dashv \Gamma \dashv CoDisc)

CoDisc:Set𝒯. CoDisc \colon Set \hookrightarrow \mathcal{T}.

(As just stated, it is automatic in the case over SetSet that this is furthermore a full and faithful functor.)

Remark

Another way of stating this is that a Grothendieck topos is local if and only if the terminal object 11 is connected and projective (since this means precisely that Γ=hom(1,)\Gamma = \hom(1, -) preserves colimits, and therefore has a right adjoint by virtue of an adjoint functor theorem). Another term for this: we say 11 is tiny (atomic). Notice the similarity to the concept of amazing right adjoint (the difference being that this is a right adjoint not to the external but to the internal hom out of 1.)

Note also that in an infinitary-extensive category an object is connected as soon as hom(X,)\hom(X,-) preserves binary coproducts (see connected object). Moreover, a coproduct-preserving functor between toposes preserves coequalizers as soon as it preserves epimorphisms, since any coequalizer can be constructed as the quotient of an equivalence relation generated using images and countable coproducts and quotients of equivalence relations are effective. Thus, we can say that a Grothendieck topos is local iff hom(1,)\hom(1,-) preserves binary coproducts and epis. Moreover, a cospan ACBA \to C \leftarrow B in a topos is a coproduct diagram iff AA and BB are disjoint monos whose union is all of CC; thus hom(1,)\hom(1,-) preserves binary coproducts as soon as it preserves the initial object and binary unions. This leads to the following equivalent form of “locality” that makes sense even for elementary toposes:

Definition

An elementary topos EE is local if the terminal object 11 is

  • nonempty: 101\ncong 0,

  • connected: 1=pq1 = p \vee q implies 1=p1 = p or 1=q1 = q, and

  • projective: every epi U1U \to 1 admits a section t:1Ut: 1 \to U.

Remark

Some authors have instead used the term “local” to refer just to the condition that 11 is connected; note this is equivalent to Sub E(1)Sub_E(1) being a local rig. In his thesis, Steve Awodey upgraded this, saying that a topos is hyperlocal if both connectivity and projectivity are satisfied. As argued above, for a Grothendieck topos this is slightly weaker than locality, although the difference is only in the inclusion of the trivial topos (for if 101\cong 0 then E1E\simeq 1). Note that a local elementary topos, as defined above, is constructively well-pointed if and only if 11 is additionally a generator.

Example

The free topos is a local elementary topos.

Properties

Equivalent characterizations

Proposition

A geometric morphism f:ESf : E \to S is local precisely if

  1. there exists a geometric morphism c:SEc : S \to E such that fcidf \circ c \simeq id;

  2. for every other geometric morphism g:GSg : G \to S the composite cgc\circ g is an initial object in the hom-category Topos /S(g,f)Topos_{/S}(g,f) of the slice 2-category of Topos over SS.

This is (Johnstone, theorem 3.6.1 vi)).

Remark

In particular this means that the category of topos points of a local topos has a contractible nerve.

General

Proposition

The global section geometric morphism of any local 𝒮\mathcal{S}-topos (over a base topos 𝒮\mathcal{S}) is a Grothendieck fibration and a Grothendieck opfibration.

This appears in (Shulman).

Proposition

The Freyd cover of a topos is a local topos, and in fact freely so. Every local topos is a retract of a Freyd cover.

This appears as (Johnstone, lemma C3.6.4).

Homotopy dimension

Proposition

In a local sheaf topos over Set, every inhabited object is globally inhabited:

every object XX for which the unique morphism X*X \to * to the terminal object is an epimorphism has a global point *X* \to X.

Proof

Since in a local topos the global section functor Γ\Gamma is a left adjoint, it preserves epimorphisms. Since it is a right adjoint it preserves the terminal object. Therefore Γ(X)Γ(*)*\Gamma(X) \to \Gamma(*) \simeq * is an epimorphism in Set, hence a surjection, meaning that Γ(X)\Gamma(X) is inhabited. Since Γ(X)Hom(*,X)\Gamma(X) \simeq Hom(*,X) (see global section geometric morphism), the claim follows.

Remark

In a topos every epimorphism is an effective epimorphism. Therefore X*X \to * being an epi means that XX is a (-1)-connected object. Therefore the above statement says in terms of (infinity,1)-category theory that a non-trivial local topos has homotopy dimension 0.

The same is true for any local (infinity,1)-topos.

Concrete sheaves

Every local topos Γ:ES\Gamma : E \to S comes with a notion of concrete sheaves, a reflective subcategory Conc Γ(E)EConc_\Gamma(E) \hookrightarrow E which factors the topos inclusion of SS:

SCodiscΓConc Γ(E)ConcE S \stackrel{\overset{\Gamma}{\leftarrow}}{\underset{Codisc}{\hookrightarrow}} Conc_\Gamma(E) \stackrel{\overset{Conc}{\leftarrow}}{\hookrightarrow} E

and is a quasitopos. See concrete sheaf for details.

Homotopy equivalence

Since a local geometric morphism has a left adjoint in the 2-category Topos, it is necessarily a homotopy equivalence of toposes.

Elementary Axiomatization

For any local topos Γ:𝒮\Gamma \colon \mathcal{E} \to \mathcal{S}, the base topos 𝒮\mathcal{S} is equivalent to the category of sheaves for a Lawvere-Tierney topology jj on \mathcal{E}. A sound and complete elementary axiomatization of local maps of (bounded) toposes can be given in terms of properties of topos EE and topology jj (AwodeyBirkedal)

We discuss first

and then

themselves.

The setup

Let \mathcal{E} be an elementary topos equipped with a Lawvere-Tierney topology j:ΩΩj : \Omega \to \Omega.

Write VVV \mapsto \sharp V for the jj-closure operation on subobjects VXV \hookrightarrow X, the sharp modality

V * V * X χ V Ω j Ω \array{ V &\to& {*} \\ \downarrow && \downarrow \\ \sharp V &\to& &\to& {*} \\ \downarrow && \downarrow && \downarrow \\ X &\stackrel{\chi_V}{\to}& \Omega &\stackrel{j}{\to}& \Omega }

Write

(ΓcoDisc):Sh j()coDiscΓ (\Gamma \dashv coDisc) : Sh_j(\mathcal{E}) \stackrel{\overset{\Gamma}{\leftarrow}}{\underset{coDisc}{\to}} \mathcal{E}

for the reflective subcategory of j-sheaves.

Definition

We say that jj is an essential topology if for all objects XX the closure operation :Sub(X)Sub(X)\sharp : Sub(X) \to Sub(X) on posets of subobjects has a left adjoint \flat \dashv \sharp :

(UV)(UV). (U \hookrightarrow \sharp V) \Leftrightarrow (\flat U \hookrightarrow V) \,.

This appears under the term “principal” in (Awodey-Birkedal, def. 2.1).

Remark

We use the notation “\flat” and “\sharp ” oppositely to the use on p.14 of Awodey-Birkedal. Our convention is such that it harmonizes with the terminology at cohesive topos and cohesive (infinity,1)-topos, where it makes interpretational sense to pronounce “\flat” as “flat”.

Observation

The left adjoints :Sub(X)Sub(X)\flat : Sub(X) \to Sub(X) for all XX \in \mathcal{E} extend to a functor :\flat : \mathcal{E} \to \mathcal{E} on all of \mathcal{E}.

Proof

(…)

Proposition

A Lawvere-Tierney topology jj is essential, ()(\flat \dashv \sharp ), precisely if for all objects XX there exists a least \sharp -dense subobject U XXU_X \hookrightarrow X.

This appears as (AwodeyBirkedal, lemma 2.3).

Proof

By the discussion at category of sheaves we have that \sharp is given by the composite

:ΓSh j()coDisc, \sharp : \mathcal{E} \stackrel{\Gamma}{\to} Sh_j(\mathcal{E}) \stackrel{coDisc}{\hookrightarrow} \mathcal{E} \,,

where the first morphism is sheafification and the second is full and faithful.

If now the left adjoint \flat exists, it follows that this comes from a left adjoint DiscDisc to Γ\Gamma as

:ΓDiscSh j()coDiscΓ:. \flat : \mathcal{E} \stackrel{\overset{Disc}{\hookleftarrow}}{\underset{\Gamma} {\to}} Sh_j(\mathcal{E}) \stackrel{\overset{\Gamma}{\leftarrow}}{\underset{coDisc}{\hookrightarrow}} \mathcal{E} : \sharp \,.

Therefore the (DiscΓ)(Disc \dashv \Gamma)-counit provides morphisms

(XX)=(XU xX), (\flat X \to X) = (\flat X \to U_x \hookrightarrow X) \,,

whose image factorization U xXU_x \hookrightarrow X we claim provides the least dense subobjects.

To show that U XU_X is dense it is sufficient to show that

(XX)=(coDiscΓDiscΓcoDiscΓX) \sharp (\flat X \to X) = (coDisc \Gamma Disc \Gamma \to coDisc \Gamma X)

is an isomorphism.

Composing this morphism with CoDiscCoDisc of the (DiscΓ)(Disc \dashv\Gamma)-unit on ΓX\Gamma X (which is an isomorphism since DiscDisc is a full and faithful functor by the discussion at fully faithful adjoint triples) and using the (DiscΓ)(Disc \dashv \Gamma) triangle identity we have

coDisc(ΓXΓDiscΓXΓX)=coDisc(ΓXIdΓX). coDisc( \Gamma X \stackrel{\simeq}{\to} \Gamma Disc \Gamma X \stackrel{}{\to} \Gamma X ) = coDisc ( \Gamma X \stackrel{Id}{\to} \Gamma X) \,.

Using that also coDisccoDisc is full and faithful and then 2-out-of-3 for isomorphisms it follows that coDiscΓDiscΓXcoDiscΓXcoDisc \Gamma Disc \Gamma X \stackrel{\simeq}{\to} coDisc \Gamma X hence

XX \sharp \flat X \stackrel{\simeq}{\to} \sharp X

is indeed an isomorphism.

Moreover, by one of the equivalent characterizations of reflective subcategories we have (…)

Definition

An object XX \in \mathcal{E} is called discrete if for all Γ\Gamma-local isomorphisms f:ABf : A \to B the induced morphism

(X,A)(X,B) \mathcal{E}(X,A) \to \mathcal{E}(X,B)

is an isomorphism (of sets, hence a bijection).

Definition

An object XX \in \mathcal{E} is called o-discrete if XX\flat X \simeq X.

Lemma

Every discrete object is o-discrete.

The axioms

Definition

On \mathcal{E} a elementary topos with Lawvere-Tierney topology jj consider the following axioms.

Theorem

These axioms characterize local geometric morphisms Sh j()D j()\mathcal{E} \to Sh_j(\mathcal{E}) \simeq D_j(\mathcal{E}).

If GG is fixed to be the terminal object (in which case Axiom 2 b becomes empty), then they characterize local and localic geometric morphisms.

This is (Awodey-Birkedal, theorem 3.1) together with the discussion around remark 3.7.

Examples

Easy examples

Example

If CC is a small category with a terminal object *C* \in C, then the presheaf topos [C op,Set][C^{op},Set] is a local topos.

Proof

Notice that Set[*,Set]Set \simeq [*,Set] is the presheaf topos over the point category, the category with a single object and a single morphism. Therefore the constant presheaf functor

Const:Set[C op,Set] Const : Set \to [C^{op}, Set]

can be thought of as sending a set SSetS \in Set, hence a functor S:*SetS : * \to Set to the composite functor

Const(S):C*SSet. Const(S) \colon C \to * \stackrel{S}{\to} Set \,.

Notice that in the presence of a terminal object in CC, ConstConst is a full and faithful functor: a natural transformation Const(S 1)Const(S 2)Const(S_1) \to Const(S_2) has components

S 1= Const(S 1)(*) f Const(S 2)(*) =S 2 id id Const(S 1)(U) Const(S 2)(U) \array{ S_1 = & Const(S_1)(*) &\stackrel{f}{\to}& Const(S_2)(*) & = S_2 \\ & \downarrow^{\mathrm{id}} && \downarrow^{\mathrm{id}} \\ & Const(S_1)(U) &\to& Const(S_2)(U) }

where the vertical morphisms are Const(U*)Const(U \to *), the point being that they exist for every UCU \in C given the presence of the terminal object. It follows that such a natural transformation is given by any and one and the same function f:S 1S 2f \colon S_1 \to S_2.

The functor ConstConst has a left adjoint and a right adjoint, and these are – essentially by definition – the colimit and the limit operations

(limConstlim) (\underset{\rightarrow}{\lim} \vdash Const \vdash \underset{\leftarrow}{\lim})

which send a presheaf/functor F:C opSetF \colon C^{op} \to Set to its colimit limFSet\underset{\rightarrow}{\lim} F \in Set or limit limFSet\underset{\leftarrow}{\lim} F \in Set, respectively.

Since adjoints are essentially unique, it follows that the global section functor Γ:[C op,Set]\Gamma \colon [C^{op}, Set] is given by taking the limit, Γlim\Gamma \simeq \underset{\leftarrow}{\lim}.

Observe that the terminal object *C* \in C is the initial object in the opposite category C opC^{op}. But the limit over a diagram with initial object is given simply by evaluation at that object, and so we have for any F[C op,Set]F \in [C^{op}, Set] that

Γ(F) limF F(*)Set \begin{aligned} \Gamma(F) & \simeq \underset{\leftarrow}{\lim} F \\ & \simeq F(*) \in Set \end{aligned}

hence that the global section functor is simply given by evaluating a presheaf on the terminal object of CC.

Limits and colimit in a presheaf category [C op,Set][C^{op}, Set] are computed objectwise over CC (see at limits and colimits by example). Therefore evaluation at any object in CC preserves in limits and colimits, and in particular evaluation at the terminal object does. Therefore Γ\Gamma preserves all colimits. Hence by the adjoint functor theorem it has a further right adjoint CoDiscCoDisc.

We can compute it explicitly by the Yoneda lemma and using the defining Hom-isomorphism of adjoints to be the functor CoDisc:Set[C op,Set]CoDisc \colon Set \to [C^{op}, Set] such that for SSetS \in Set the presheaf CoDisc(S)CoDisc(S) is given over UCU \in C by

CoDisc(S)(U) YonedaHom [C op,Set](U,CoDisc(S)) adjunctionHom Set(Γ(U),S). \begin{aligned} CoDisc(S)(U) & \underoverset{Yoneda}{\simeq}{\to} Hom_{[C^{op}, Set]}(U,CoDisc(S)) \\ & \underoverset{adjunction}{\simeq}{\to} Hom_{Set}(\Gamma(U), S) \,. \end{aligned}

So in conclusion we have an adjoint triple (ConstΓCoDisc)(Const \vdash \Gamma \vdash CoDisc) where ConstConst is a full and faithful functor. By the discussion at fully faithful adjoint triples it follows then that also CoDiscCoDisc is full and faithful.

Proposition

The converse to prop. is true if CC is Cauchy complete.

Example

If XX is a topological space, or more generally a locale, then Sh(X)Sh(X) is local (over Set) iff XX has a focal point xx, i.e. a point whose only neighborhood is the whole space. In this case, the extra right adjoint f !:SetSh(X)f^! : Set \to Sh(X) to the global sections functor f *:Sh(X)Setf_* : Sh(X) \to Set is given by the functor which computes the stalk at xx. This can also be given without reference to xx, by the formula

Γ(U,f !(M))=Hom({|U=X},M){M, U=X, {}, UX, \Gamma(U, f^!(M)) = Hom(\{\star|U=X\}, M) \cong \begin{cases} M, & U = X, \\ \{\star\}, & U \neq X, \end{cases}

for sets MM and open subsets UXU \subseteq X.

Sheaves on a local site

For CC a local site, the category of sheaves Sh(C)Sh(C) is a local topos over SetSet.

For instance CartSp is a local site. Objects in Sh(C)Sh(C) are generalized smooth spaces such as diffeological spaces. The further right adjoint

Codisc:SetSh(CartSp) Codisc : Set \to Sh(CartSp)

is the functor that sends a set to the diffeological space on that set with codiscrete smooth structure (every map of sets is smooth).

Relative Realizability

Let AA be a partial combinatory algebra and let AAA\sharp\subseteq A be a sub partial combinatory algebra of AA. Then there is a (localic) local geometric morphism from the relative realizability topos? RT(A,A)\mathrm{RT}(A,A\sharp) to the standard realizability topos RT(A)\mathrm{RT}(A\sharp).

Localization

Let LocToposLocTopos denote the 2-category of local Grothendieck toposes (over Set) with all geometric morphisms between them. Let PToposPTopos denote the 2-category whose objects are pointed toposes? (i.e. (Grothendieck) toposes EE equipped with a geometric morphism s:SetEs\colon Set\to E), and whose morphisms are pairs (f,α)(f,\alpha) such that f:EEf\colon E\to E' is a geometric morphism and α:sfs\alpha\colon s'\to f s is a (not necessarily invertible) geometric transformation.

Note that if EE is a local topos with global sections geometric morphism e *e *e^*\dashv e_*, then the adjunction e *e !e_*\dashv e^! is also a geometric morphism SetESet\to E. In this way we have a functor LocToposPToposLocTopos \to PTopos, which is a full embedding, and turns out to have a right adjoint: this right adjoint is called the localization of a pointed topos at its specified point. For example:

Proposition

If CC is a small category and UU is an object of CC, then the localization of the presheaf topos [C op,Set][C^{op},Set] at the point induced by U:1CU\colon 1\to C can be identified with the presheaf topos [(C/U) op,Set][(C/U)^{op},Set] over the over category of CC over UU. By the general properties of over toposes, this is equivalently the over-topos PSh(C)/UPSh(C)/U (where UU is regarded in PSh(C)PSh(C) by the Yoneda embedding).

Proposition

If X=Spec(A)X=Spec(A) is the Zariski spectrum of a commutative ring AA, and PAP\subset A is a prime ideal of AA (i.e. a point of XX), then the localization of Sh(X)Sh(X) at P:1XP\colon 1\to X can be identified with Sh(Spec(A P))Sh(Spec(A_P)), where A PA_P denotes the localization of AA at PP. Of course, this is the origin of the terminology.

A similar construction is possible for bounded toposes over any base (not just Set).

Local over-toposes

Proposition

For \mathcal{E} a Grothendieck topos and XX \in \mathcal{E} an object, the over topos /X\mathcal{E}/X is local if XX is a tiny object (atomic object).

Proof

We check that the global section geometric morphism Γ:/XSet\Gamma : \mathcal{E}/X \to Set preserves colimits. It is given by the hom-functor out of the terminal object of /X\mathcal{E}/X, which is (XIdX)(X \stackrel{Id}{\to} X):

Γ:(AfX)Hom /X(Id X,f). \Gamma : (A \stackrel{f}{\to} X) \mapsto Hom_{\mathcal{E}/X}(Id_X, f) \,.

The hom-sets in the over category are fibers of the hom-sets in \mathcal{E}: we have a pullback diagram

Hom /X(Id X,(AX)) Hom (X,A) f * * Id x Hom (X,X). \array{ Hom_{\mathcal{E}/X}(Id_X, (A \to X)) &\to& Hom_{\mathcal{E}}(X,A) \\ \downarrow && \downarrow^{f_*} \\ * &\stackrel{Id_x}{\to}& Hom_{\mathcal{E}}(X,X) } \,.

Moreover, overserve that colimits in the over category are computed in \mathcal{E}.

lim i(A if iX)(lim iA i)X. {\lim_{\to}}_i (A_i \stackrel{f_i}{\to} X) \simeq ({\lim_\to}_i A_i) \to X \,.

If XX is a tiny object then by definition we have

Hom (X,lim iA i)lim iHom (X,A i), Hom_{\mathcal{E}}(X, {\lim}_i A_i) \simeq {\lim_\to}_i Hom_{\mathcal{E}}(X, A_i) \,,

Inserting all this into the above pullback gives the pullback

Hom /X(Id X,lim i(A iX)) lim iHom (X,A i) f * * Id x Hom (X,X). \array{ Hom_{\mathcal{E}/X}(Id_X, {\lim_\to}_i (A_i \to X)) &\to& {\lim_\to}_i Hom_{\mathcal{E}}(X, A_i) \\ \downarrow && \downarrow^{f_*} \\ * &\stackrel{Id_x}{\to}& Hom_{\mathcal{E}}(X,X) } \,.

By universal colimits in the topos Set, this pullback of a colimit is the colimit of the separate pullbacks, so that

Γ(lim i(A iX)))Hom /X(Id X,lim i(A iX))lim iHom /X(Id X,(A iX))lim iΓ(A iX). \Gamma({\lim_\to}_i (A_i \to X))) \simeq Hom_{\mathcal{E}/X}(Id_X, {\lim_\to}_i (A_i \to X)) \simeq {\lim_\to}_i Hom_{\mathcal{E}/X}(Id_X,(A_i \to X)) \simeq {\lim_\to}_i \Gamma(A_i \to X) \,.

So Γ\Gamma does commute with colimits if XX is tiny. By the adjoint functor theorem then the right adjoint :Set/X\nabla : Set \to \mathcal{E}/X does exist and so /X\mathcal{E}/X is a local topos.

Remark

As a special case this reproduces the above statement that slices PSh(C)/j(U)PSh(C)/j(U) of presheaf toposes over objects in the image of the Yoneda embedding are local: every representable functor is tiny (see there).

Gros toposes

Let AA be a commutative ring (such as \mathbb{Z} or a field), let SpecASpec A be the prime spectrum of AA, and let 𝒵 A\mathcal{Z}_A be the big Zariski topos for AA (i.e. the classifying topos for local A A -algebras). For each element aa of AA, we have an open subset D(a)={𝔭SpecA:a𝔭}D (a) = \{ \mathfrak{p} \in Spec A : a \notin \mathfrak{p} \}, and these open subsets constitute a basis for the topology on SpecASpec A. The full subcategory of the frame of open subsets of SpecASpec A spanned by these basic open subsets admits a contravariant full embedding in the category of finitely-presented AA-algebras via the functor D(a)A[a 1]D (a) \mapsto A [a^{-1}] (the well-definedness of this functor requires a non-trivial check!), and this functor moreover has the cover lifting property, so induces a local geometric morphism 𝒵 ASh(SpecA)\mathcal{Z}_A \to Sh (Spec A).

and

References

Standard references include

and Chapter C3.6 of

A completely internal characterization of local toposes is discussed in

This is based on part 2 of

  • Lars Birkedal, Developing Theories of Types and

    Computability via Realizability_ PhD Thesis (pdf)

Free local constructions are considered in

Notions of local topos, with a view to logical completeness theorems, appear in Steve Awodey’s thesis:

  • Steve Awodey, Logic in topoi: functorial semantics for higher-order logic, Thesis, University of Chicago (1997).

Last revised on November 3, 2021 at 21:24:01. See the history of this page for a list of all contributions to it.