Combined 2-01 and 2-08 write-up

More 2-01

Judgments and Logical Frameworks

On Zulip

I found the signature v. judgment distinction confusing, and spent much of the meeting last week discussing it. A particular point about this was raised in this Mastodon thread, about “why [Sterling’s thesis does not] include Pi types of signatures over signatures?”

TODO

More 2-08

Topos-Logie

Where are we with this? Topoi as spatial objects?

Sites, Sheaves, and Makkai and Reyes

One of the reference books for the logic seminar is Makkai and Reyes, First Order Categorical Logic. Topoi are often (analytically?) constructed as categories of sheaves? So I was trying to finally work through the construction.

To define a category of sheaves over a site, which apparently becomes a topos, we have to define a Grothendieck topology for a site. Makkai and Reyes presents the two classic descriptions– one in terms of covering families, and one in terms of sieves/cribles.

The definition in terms of covering families reads like an axiomatized version of the “typical” definition of sheaves, but the sieve definition??

I have some shallow questions about this material:

  • The covering family definition of a sheaf in terms of compatible presheaves1, which is given by a nice commutative diagram. (Diagram for compatible presheaf difficult to typeset.)

    For reference the definition is: “A presheaf \(F\) is a (set-valued) sheaf for the site \(\mathcal{C}\) if whenever \(A∈\mathcal{C}_0\), \((f_i : A_i → A)_{i∈I} ∈ Cov(A)\) and \((ξ_i : A_i → A)_i\) is a compatible family from \((f_i)_I\), then there is a unique morphism \(ξ: A → F\) such that \(∀i∈I. ξ_i = ξ∘f_i\)” (p 16).

    This definition seems to “require” the Yoneda lemma, and I was wondering if that is indeed the case, and why the diagrammatic definition feels inside out (or outside in?).

  • There’s a mechanical calculation that the covering family definition of a Grothendieck topology is equivalent to the sieve definition, but I fail to see in what sense the sieve definition captures the same data

    • A sieve is a subobject of \(YA ∈ Set^{\mathcal{C}^{op}}\), for an object of the site
    • Then the collection of covering families \(Cov(A)\) are replaced by collections of sieves \(J(A)\), where each \(J(A)\) is a filter, when the subobjects are partially ordered (by pointwise set inclusion).
    • The definition vaguely reads like a logical relation…?

Uemura’s LF

I will very briefly summarize what I’ve skimed from Uemura’s thesis, with priority for

  1. What I can understand
  2. What seems most relevant to where I am in Sterling’s thesis

In the introduction, the view is taken that a type theory in general is just a formal system for building and deriving judgments. There is no explicit bias about the type of judgment. Uemura then sign posts that “The semantics of type theories defined in a logical framework, however, has not received much attention.” This begs the question

  • Why do want to define type theories in logical frameworks, anyways?

I’d have to read something like the Twelf paper for a proper answer, but some partial reasons:

  • (From the Twelf wiki) To mechanize new type theories
  • To formalize (new) type theories
  • (Based on the introduction to Sterling’s thesis) To give a precise account of the type theory’s metatheoretic definition, in the style2 of Martin-Löf
    • Does this afford any bona fide technical advantages? The answer seems like it’s supposed to be yes, but I don’t see it.

In any case, Uemura continues on the need for a more general logical framework, observing that previous conceptions (Bauer et al, Essentially Algebraic Theories) are inadequate (in the colloquial, not LF sense). So Uemura follows the long line of functorial semantics and defines type theories as algebraic objects, by introducing the notions of categories with representable maps and second-order generalized algebraic theories.

The notion of categories with representable maps (CwR) is supposedly based on Awodey’s notion of natural model, which is supposedly equivalent to Categories with Families?

A type theory is then defined to just be a CwR.

A nat. trans. of presheaves \(α : F' → F\) is representable if every fiber is representable, ie \(∀A ∈ \mathcal{C}. ∀x ∈ F(A). ∃B ∈ \mathcal{C}. ∃t : B → A. ∃x'∈ F'(B).\) pullback square.

Awodey explicitly states(!) that we’re using the Yoneda lemma here to identify \(x ∈ F(A)\) with \(x : YA → F\).

In Uemura’s words, a map of presheaves \(f : B → A\) is representable iff for any section \(a : Yx → A\), the pulled back map \(a^*B\) is representable.

The intended(?) interpretation is as a CwF, whereby over a category of contexts \(\mathcal{C}\), a presheaf \(U'\) is the (set of) terms for each context, a presheaf \(U\) is the (set of) types for each context, and a representable map \(p : U' → U\) comes with the components \(p_{Γ ∈ \mathcal{C}_0} : U'(Γ) → U(Γ)\) assigns a type to each term, under context.

The naturality and functoriality ensure notions of substitution as usual, which I should check, and representability ensures TODO.

For simplicity, let’s assume \(\mathcal{C}\) has all finite products, or even all finite limits and enough exponentials?

Uemura works with discrete fibrations instead, while I’ll have to skip right now– running out of time.

The class of representable maps then has nice closure properties (id, comp, pullbacks), and (fast forward) plays well with notions in type theory like Beck-Chevalley.

Then a type theory is a CwR, and a model of a type theory is a CwR morphism into the category of discrete fibrations over a fixed category (with terminal object). This \(DFib_{M}\) is itself a CwR with more structure?

A morphism of models (of a given theory) is then a functor of the base/context categories, and a map of each ??

Then we can present a type theory as a CwR (ie given a representable map, we can construct the free CwR with relations).

That is, to present a type theory, you need to supply

  • a representable map for the base dependent type theory
  • and maybe more, for more complicated type theories??

But the point of all of this is to internalize/reify judgments as objects in the CwR. Which is to say, we do judgments-as-types, but as judgment-forms-as-objects, which lets one study multiple type theories and variants of a given type theory of the same footing?

Logic Seminar

We talked about simple Lawvere theories for a purely equational language yesterday.

  • I was thinking after, and while reading the introduction to Uemura’s Ch. 3: Is the “only”/crucial difference between a Lawvere theory and simple (eg) internal group object, that the group object has no way to enforce (in the sense of functorial semantics) “higher equations” eg associativity?

    And thus, you really do need all finite products?

I’ll be presenting on hyperdoctrines for Horn theories on Wednesday.

  1. I’m paraphrasing. The full notion is of a compatible family of morphisms from a covering to a presheaf. ↩

  2. By style, I do not mean mathematically– or pre-mathematically– in the sense of “tradition” or “à la”, but rather in the vaguely constructivist and austere sense. ↩