报告人：Giuseppe Rosolini 教授

工作单位：Universitàdi Genova

举办单位：数学凯旋娱乐（中国）有限公司

报告人简介：Giuseppe Rosolini,professor and doctoral supervisor of Universitàdi Genova，received his Ph.D. from the University of Oxford, UK in 1986. His main research direction iscategorytheory.He published more than 80 high-quality papers inmathematics, andoften involved in the running of the International Conference on Category Theory.Currently, he serves as the editorial board member of Journal of Pure and Applied Algebra, Theory and Applications of Categories, Archimede, Scienza FA, Matematica Olimpica and Nuova Lettera Matematica.

（1）

报告时间：2023年10月27日（星期五）18:00-19:30

报告地点：Zoom会议：973 8265 9639, PIN:888

报告简介：We study the 2-category theory of Grothendieck fibrations in the 2-category of functorsCat². After redrawing a few general results in that context, we show that fibrations over a given base are pseudo-coalgebras for a 2-comonad on Cat/B. We use that result to explain how an arbitrary fibration is equivalent to one with a splitting.

（2）

报告时间：2023年10月28日（星期六）17:30-18:30

报告地点：腾讯会议：686-584-706

报告简介：In the categorical approach to logic proposed by Lawvere, which systematically uses adjoints to describe the logical operations, equality is presented in the form of a left adjoint to reindexing along diagonal arrows in the base. Taking advantage of the modular perspective provided by category theory, one can look at those Grothendieck fibrations which sustain just the structure of equality, the so-called elementary fibrations, aka fibrations with equality.

The present paper provides a characterisation of elementary fibrations which is a substantial generalisation of the one already available for faithful fibrations. The characterisation is based on a particular structure in the fibres which may be understood as proof-relevant equality predicates equipped with a principle of indiscernibility of identicals à la Leibniz. We exemplify this structure for several classes of fibrations, in particular, for fibrations used in the semantics of the identity type of Martin-Löf type theory. We close the paper discussing some fibrations related to Hofmann and Streicher’s groupoid model of the identity type and showing that one of them is elementary.

（3）

报告时间：2023年11月1日（星期三）17:30-18:30

报告地点：腾讯会议：368-722-267

报告简介：The present paper aims at stressing the importance of the Hofmann–Streicher groupoid model for Martin Löf Type Theory as a link with the first-order equality and its semantics via adjunctions. The groupoid model was introduced by Martin Hofmann in his Ph.D. thesis and later analysed in collaboration with Thomas Streicher. In this paper, after describing an algebraic weak factorisation system (L, R) on the cate gory C-Gpd of C-enriched groupoids, we prove that its fibration of algebras is elementary (in the sense of Lawvere) and use this fact to produce the factorisation of diagonals for (L, R) needed to interpret identity types.

（4）

报告时间：2023年11月3日（星期五）17:30-18:30

报告地点：腾讯会议：618-154-666

报告简介：Doctrines are categorical structures very apt to study logics of different nature within a unified environ ment: the 2-categoryDtnof doctrines. Modal interior operators are characterised as particular adjoints in the 2-categoryDtn. We show that they can be constructed from comonads inDtnas well as from adjunc tions in it, and we compare the two constructions. Finally we show the amount of information lost in the passage from a comonad, or from an adjunction, to the modal interior operator. The basis for the present work is provided by some seminal work of John Power.

（5）

报告时间：2023年11月6日（星期一）17:30-18:30

报告地点：腾讯会议：543-668-628

报告简介：We show that the two models of an extensional version of Martin Löf type theory, those given by the category of equilogical spaces and by the effective topos, are homotopical quotients of appropriate categories of 2-groupoids.