You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (Mar 19 2021 at 20:04):Friday, 23:00 UTC
Tim Hosgood (Mar 19 2021 at 20:04):Abstract:
Dependent type theory is sometimes described categorically as a Category with Families (CwF). In [1], it was shown that the notion of a CwF can conveniently be reformulated as a so-called "natural model", which is simply a representable natural transformation p : U. → U over an arbitrary index category C of "contexts". Such a model of type theory admits dependent sums and a terminal type just if it is a (pseudo-)monad, when regarded as a polynomial endofunctor P : Ĉ → Ĉ on the category of presheaves on C. Moreover, dependent products correspond to a P-algebra structure. The logical Propositions-as-Types conception is then modelled by a retraction of polynomial monads relating the type theoretic and the topos-theoretic interpretations of predicate logic.
[1] Awodey, S., Natural models of homotopy type theory, Math. Stru. Comp. Sci., 2018.