O Grupo de Lógica e Fundamentos da Matemática<http://dgp.cnpq.br/diretorioc/fontes/detalhegrupo.jsp?grupo=0021101GPX6Z9G> (Centro de Informática / Departamento de Matemática da UFPE) convida para a palestra do Prof Joachim Kock <http://mat.uab.es/~kock/> (Departament de Matemàtiques, Universitat Autònoma de Barcelona) a ser realizada:
Dia: 24/04/2014 (5a.feira) Hora: 10h Local: Anfiteatro do Centro de Informática da UFPE Todos são bem-vindos! Ruy ---- *Polynomial functors, infinity-groupoids, and homotopy type theory* Joachim Kock Polynomial functors are functors between slice categories, built from pullbacks and their adjoints, which are 'dependent sums' and 'dependent products', hence are intimately related to type theory. They make sense in locally cartesian closed (infinity)-categories. Already in sets there are many interesting aspects to the theory, and before moving on to infinity-groupoids, I would like to dwell a little bit on elementary aspects with digressions into algebra, combinatorics, and classical inductive data types. The cool thing about infinity-groupoids is that they work very much like sets --- just better! From the viewpoint of combinatorics, symmetries are taken care of automatically. From more abstract viewpoints (originating in geometry and topology), 'everything becomes representable', through the existence of a general object classifier. This feature of infinity-groupoids corresponds to the univalence axiom in homotopy type theory. Depending on time and interest, I can either go deeper into the theory of polynomial functors, or go in more abstract directions of higher topos theory. *Joachim Kock* fez doutorado em matemática na UFPE em 2000, depois fez postdocs em Stockholm, Nice e Montréal, e hoje é professor titular na Universitat Autònoma de Barcelona. Tem trabalhado em geometria algébrica, álgebra quântica, teoria de categorias e teoria de homotopia. _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
