UF IAS 2012 Archive Categorical Semantics WG

Currently [as of late Jan 2013] meeting Tuesdays, 4:00, Simonyi 2013

Notes from meetings follow below; various details are missing, so please feel free to fill them in!

Notes from meeting, Thu 24 Jan

(Mike Shulman leading)

Review: high-level picture of what categorical models are.

Syntax of type theory

<—> [Standard techniques, very well-understood, very close equivalence]

Categories with attributes, etc.

<—> [type-theoretic coherence theorems; see below]

1-categorical settings (eg LCCCs, Quillen model cats, fibration categories, etc.)

<—> [homotopy-theoretic theorems]

infinity-categorical settings (infinity-toposes, etc.)

Review: coherence theorems we have so far, and their examples.

[todo: add this! at least photo]

Future desiderata

• better univalent universes
• constructions on models: sheaves, gluing, realizability…
• constructive completeness
• better notion of morphism/equivalence of models
• elementary, easily comprehensible models
• directed paths, other weakenings/variations of the type theory.

Notes from meeting, Tue 28 Jan

(Mike Shulman leading)

Overview: what kinds of goals could we have?

1. Do what we already do, but better.
2. Change the type theory (to fit more closely with the desired models)
3. More radical notions of model (eg in derivators; partial models; depart further from categorical semantics)

Specifics.

SA: models defined only up to equivalence? Instead of functors, use anafunctors, etc. Idea: look at the concrete, Tarskian, Kripke-Joyal style unwinding, and see if we can see how to weaken it there. Recall: definition of anafunctor.

AJ: distributors; the collage of a distributor. Collage gives an equivalence between distributors and categories over the arrow category $I$. Perhaps suitably considered, this could allow us to define a weak model = weak structure-preserving functor = ?? suitably-structured category over $I?$

PL: a possibly application of a more radical notion of model: looking for notion of morphism/homotopy/equivalence of models (i.e. model of the same theory in the same category). Idea: a homotopy between two models [structure-preserving functors] C(T) —> E^I as a model C(T) —> E^I (seems to need to be weak since E^I doesn’t strictly carry the right structure.) MS: use Reedy fibrant spans, or something like that. (More details.)

AJ: Modifying the type theory… to what extent can we extend the theory to allow us to consider something like maps of structures (eg reflexive graphs) that preserve structure (eg the reflexivity). Various discussion about how to do this, and to what kinds of extent one can talk about this.

BS: question about the homotopy hypothesis. Many answers, including summary from MS, AJ; question from BS: how much, and in what sense(s), should we expect models of TT based on (internal) (semi-)simplicial sets and on globular weak ω-groupoids (and maybe also opetopes) to be the same? and, AJ: ?

To do next.

Eric Finster may continue next week from his seminar talk on Thursday. For some future meeting, SA will work out the presheaf semantics over a V-universe, toward giving a K-J style recursive definition of validity.