Title: Fibered Yoneda Lemma in Lean 4 Abstract: In this talk, I would like to give you a sense of what it’s like to do category theory in a computer. I use an interactive theorem prover called Lean4, a complex piece of software based on dependent type theory. In the first part, I will give a quick […]
Title: Huber pairs
Title: Calculus of fractions for quasicategories Abstract: A central object of interest in abstract homotopy theory is the localization of marked categories. One case of interest is when the marked category admits a "calculus of fractions". This condition was introduced by P. Gabriel and M. Zisman to construct better-behaved models for the localization. For instance, […]
Title: Liquid & gaseous modules
Title: Six functor formalism and the !-topology
Title: The simply typed 2λ-calculus Abstract: 2λ-calculus is a language with three levels: types, terms, and rewrites. I will explore their properties and give categorical description of the equational theory on the rewrites of the 2λ-calculus
Title: Analytic stacks
Title: An introduction to pretorsion theories (based on the collaboration with Alberto Facchini, Carmelo Finocchiaro, Francis Borceux, Federico Campanini, Aline Michel and Walter Tholen) Abstract: The notion of pretorsion theory is a natural extension of the classical notion of torsion theory in an abelian category. The idea is to associate, with any pair (T , F) […]