public inbox for
 help / color / mirror / Atom feed
* ItaCa Fest - Coraglia and Kock - 19 May
@ 2022-05-16 10:30 Ivan Di Liberti
  0 siblings, 0 replies; only message in thread
From: Ivan Di Liberti @ 2022-05-16 10:30 UTC (permalink / raw)
  To: categories

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:
While the Fest website is this one:

Join us (and bring a friend)!

Beppe, Ivan, Edoardo, Fosco, Paolo.


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.

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: ]

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2022-05-16 10:30 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-16 10:30 ItaCa Fest - Coraglia and Kock - 19 May Ivan Di Liberti

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox