1. In his two earlier talks, Patrick defined the category of presheaves on a small category, and within this category the subcategory of sheaves for a given Grothendieck topology. Both of these categories, presheaves and sheaves, are examples of topoi, but this fact was only stated and not proved in his earlier lectures. In this lecture and its sequel, Patrick will prove that these categories form topoi.

    The lecture notes are available here: therisingsea.org/notes/ch2018-lecture10.pdf.

    For the general seminar webpage see therisingsea.org/post/seminar-ch/.

    # vimeo.com/277558756 Uploaded 6 Plays 0 Comments
  2. The goal of the seminar in S1 of 2018 is to understand classifying topoi. These are topoi which have a universal property with respect to a particular geometry theory, and they are constructed as categories of sheaves on a site, the underlying category of which is defined in terms of the language of the theory. We have just had two lectures by Patrick Elliott on categories of sheaves, so it is time to look more closely at the relationship between topoi and higher-order logic. This talk by Will Troiani is an introduction to this theme. He explains how to think about predicates in general topoi, and uses that as a way to introduce elementary topoi and prove that this definition is an equivalent characterisation of topoi within all categories.

    The lecture notes are available here: therisingsea.org/notes/ch2018-lecture8.pdf.

    For the general seminar webpage see therisingsea.org/post/seminar-ch/.

    # vimeo.com/269326119 Uploaded 33 Plays 0 Comments
  3. The most important examples of topoi are categories of sheaves of sets on a small category. Patrick Eilliott introduced this class of examples over two talks, of which is the second. In this talk he defines Grothendieck topologies and the category of sheaves on a site, and develops the example of the Zariski topos. This example will return later as the classifying topos of the theory of local rings.

    The lecture notes are available here: therisingsea.org/notes/ch2018-lecture7.pdf.

    For the general seminar webpage see therisingsea.org/post/seminar-ch/.

    # vimeo.com/268205555 Uploaded 20 Plays 0 Comments
  4. The most important examples of topoi are categories of sheaves of sets on a small category. Patrick Eilliott introduced this class of examples over two talks, of which is the first. In this talk he defines presheaves and sheaves on a topological space, and explains using the Yoneda lemma how to think about the sheaf condition in terms of sieves on objects in a category. This is preparation for his second lecture, where he defines sheaves with respect to a Grothendieck topology.

    The lecture notes are available here: therisingsea.org/notes/ch2018-lecture6.pdf.

    For the general seminar webpage see therisingsea.org/post/seminar-ch/.

    # vimeo.com/268009512 Uploaded 9 Plays 0 Comments
  5. A topos is a Cartesian closed category with all finite limits and a subobject classifier. In his two seminar talks (of which this is the second) James Clift will explain all of these terms in detail. In his first talk he defined products, pullbacks, general limits, and exponentials and in Part 2 he explains subobject classifiers.

    The lecture notes are available here: therisingsea.org/notes/ch2018-lecture4.pdf.

    For the general seminar webpage see therisingsea.org/post/seminar-ch/.

    # vimeo.com/264398841 Uploaded 16 Plays 0 Comments

Curry-Howard seminar

Daniel Murfet Business

Seminar at the University of Melbourne on the mathematics of logic, categories, and programs.

Browse This Channel

Shout Box

Heads up: the shoutbox will be retiring soon. It’s tired of working, and can’t wait to relax. You can still send a message to the channel owner, though!

Channels are a simple, beautiful way to showcase and watch videos. Browse more Channels.