Dear all, The next date of the ItaCa Fest will be May 19, 2022 at 3 pm (Italian time): - G. Coraglia, - J. Kock. The zoom link is the following: https://stockholmuniversity.zoom.us/j/68792232558 While the Fest website is this one: https://progetto-itaca.github.io/pages/fest22.html Join us (and bring a friend)! Cheers, Beppe, Ivan, Edoardo, Fosco, Paolo. ———————————————————————————————————— Coraglia. Title: Comonads for dependent types Abstract: In exploring the relation between a classical model of dependent types (comprehension categories) and a new one (judgemental dtts) we pin-point the comonadic behaviour of weakening and contraction. We describe three different 2-categories and show that they are 2-equivalent, then proceed to analyze the benefits of each of the three. The fact that one can precisely relate such different perspectives allows, for example, for a swift and cleaner treatment of type constructors: we show how certain categorical models for dependent types come inherently equipped with some due to the choices one makes in introducing tools to interpret context extension. Kock. Title: Decomposition spaces, right fibrations, and edgewise subdivision Abstract: Decomposition spaces are simplicial infinity-groupoids subject to an exactness condition weaker than the Segal condition. Where the Segal condition expresses composition, the weak condition expresses decomposition. The motivation for studying decomposition spaces is that they have incidence coalgebras and Möbius inversion. The most important class of simplicial maps for decomposition spaces are the CULF maps (standing for 'conservative' and 'unique-lifting-of-factorisation'), first studied by Lawvere; they induce coalgebra homomorphisms. The theorem I want to arrive at in the talk says that the infinity-category of (Rezk-complete) decomposition spaces and CULF maps is locally an infinity-topos. More precisely for each (Rezk-complete) decomposition space D, the slice infinity-category Decomp/D is equivalent to PrSh(Sd(D)), the infinity-topos of presheaves on the edgewise subdivision of D. Most of the talk will be spent on explaining preliminaries, though. This is joint work with Philip Hackney. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]