[pt] 2-CATEGORIA E TEORIA DA PROVA - CECILIA GONCALVES REIS ENGLANDER (2010)
[pt] Dedução Natural para a lógica intuicionista tem sido relacionada à Teoria das Categorias através do que agora é conhecido por Lógica Categórica. Essa relação é fortemente baseada no isomorfismo de Curry-Howard entre Dedução Natural e (lambda)-Cálculo Tipado. Esta dissertação descreve alguns aspectos dessa relação com o objetivo de propor uma visão 2-categórica da Lógica Categórica. Mostramos que mesmo numa visão 2-cateórica algumas desvantagens conhecidas na Teoria das Categorias continuam valendo. Concluímos essa dissertação discutindo as vantagens de uma visão 2-categórica a partir de premissas mais fracas.