Thursday 25 July 2019, 11:30, LSV library: Induction to fibred multicategory, Farzad Jafarrahmani (Master intern, ENS Cachan).

We study the induction proofs of predicates and inductively defined terms in a categorical setting based on the idea of the categorical logic and fibred category. This fibrational framework is considered on multi-categories, since those are similar to sequent calculus. This framework could be used to provide a denotational semantic of cyclic proofs. For instance, we will show the unique morphism form an inductive predicate over natural numbers such as even or odd predicate is a solution of the associated equation of a cyclic proof. Then we compare three different ways of defining inductive predicates. First way is by the initial algebra of a suitable bifunctor. The second is using the notion of pullback and pushforward, and the last is based on the same idea of the definition of natural numbers object by William Lawvere. At the end of this talk, we will fix a proof system based on the categorical setting, and will consider equivalence classes of proofs. Now one could show the crucial fact that the syntactical category corresponding to that proof system is free in an appropriate sense.