Mathematical Logic Webinar

A Constructive Proof of the Univalence Axiom (Part II)

Videoconferência

Por Clarence Protin.

The homotopy type theory/univalent foundations program aims at providing a type theory for proof assistants and proof checkers suitable for formalising mathematics and in particular homotopy theory.

The original version of homotopy type theory/univalent foundations is based on dependent type theory to which are added axioms for function extensionality and univalence. The basic idea is that concepts of homotopy theory are applied to the treatment of equality types. Roughly speaking, the univalence axiom gives formal justification for the standard mathematical practice of "identifying isomorphic structures."

Voevodsky gave a model of homotopy type theory based on simplicial sets. However this model made essential use of classical logic. Furthermore in the original version univalence is introduced via a postulated constant with no computational interpretation. Since the constructive nature of type theories is a major philosophical and practical advantage an important task in subsequent research has been to give a computational interpretation to the axioms and to find a constructive model.

Since the first cubical set model was proposed around 2014 by Bezem and Coquand required additional operations on cubical sets (such as Kan operations and contraction) have been brought to light as well as the necessity of extending the original syntax of homotopy type theory with new constructors to express these operations. Such systems are called cubical type theories. The most promising model has been the cubical set model presented in the paper of Cohen, Coquand, Huber and Mörtberg (2018) which is based on free De Morgan algebras over names. In the associated cubical type theory function extensionality and the univalence axiom actually become theorems.

In these talks we give a leisurely elementary introduction to the syntactical aspects of cubical type theory as found in the paper of Cohen et al. and present in detail the proof of the univalence axiom using Glue types. We also attempt to explain some of the geometric and topological intuitions behind the use of De Morgan algebras over names. Our presentation does not require any background in category theory or homotopy theory, only some acquaintance with natural deduction and type theory. Finally we touch briefly upon some ideas for actual implementations of cubical type theory which might address some of the efficiency problems.


Transmissão via Zoom.

16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Logótipo do concurso e das entidades envolvidas

Rui Agostinho, Professor Jubilado de CIÊNCIAS, integra o júri do concurso.

Título "Hoje quem manda sou eu" e mapa de Portugal

Palestra por Jorge Buescu (Ciências ULisboa), no âmbito da iniciativa "Hoje quem manda sou eu", promovida pela Ciência Viva.

Luz a atravessar nuvens

O concerto integra o programa Música na Universidade de Lisboa, numa parceria com a Orquestra Académica da Universidade de Lisboa, naquele que é o Concerto Final de Temporada.

Representação de programação R

Este curso tem como objetivo dotar os alunos de conhecimentos estatísticos e ferramentas para manipular, analisar e visualizar dados biológicos com o R. Introdução à modelação, simulações e estatística Bayesiana.

Logótipo do Verão na ULisboa, sobre um fundo azul

Uma iniciativa da Universidade de Lisboa que proporciona a oportunidade única, aos alunos do 8.º ao 12.º anos de estudo, ou que tenham já concluído o 12.º ano, de ficar a conhecer e experimentar o ritmo e o espírito da vida académica na Universidade.

Composição de imagens relativas ao voluntariado

30 de junho - Apresentações relativas ao 2.º semestre do ano letivo 2024/2025.

Título/data/local do evento e fotografia do espaço

Até onde te atreves a ir? O Programa de Verão do IA é o teu portal para o Espaço.

Workshop organizado pelo CEMS.UL - Centro de Estudos Matemáticos e pelo CAMGDS - Centro de Análise Matemática, Geometria e Sistemas Dinâmicos.

Seminário do Instituto de Biossistemas e Ciências Integrativas, por Vera Inácio (BioISI).

Lâmpada a originar um fogo de artifício

Projetos de Investigação e Desenvolvimento no âmbito dos Concursos Internos de Projetos de Investigação e Inovação de CIÊNCIAS.

Estátua representativa da biodiversidade do planeta Terra

Seminário Doutoral III (Doutoramento em Biologia - Especialidade de Biologia Evolutiva), por João Miguel Moreno.

Logótipo, data e local do evento

Com o tema “Ciência, Inovação e Sociedade”, o encontro será um palco de promoção e discussão do impacto científico, social, cultural e económico da investigação em Portugal.

Horta Solar

E se fosse possível experimentar um curso universitário antes de concorrer ao ensino superior? Agora já é!

Título e local do evento

O evento visa promover o diálogo interdisciplinar sobre estruturas de proteínas, doenças conformacionais e tecnologias baseadas em proteínas.

Computabilidade na Europa (CiE) - uma série interdisciplinar de conferências internacionais organizada pela Associação Computabilidade na Europa (ACiE).

Título/data do evento e vários objetos museológicos

Este curso visa fornecer uma visão atualizada do potencial das coleções museológicas para a investigação da biodiversidade. Mais especificamente, pretende apresentar estudos de caso sobre o valor dos museus e a utilização de coleções e espécimes no século XXI, utilizando novas tecnologias e métodos analíticos.

Título e datas do programa de estágios

Preparados para explorar a investigação de perto?

Águas subterrâneas

Curso acreditado para efeitos de progressão na carreira dos professores na dimensão cientifico-pedagógica dos grupos 420 e 520.

Um workshop com o objetivo de reunir académicos que abordam a história da ecologia - e a evolução da própria disciplina - a partir de uma variedade de perspetivas.

A 10.ª edição do Ser Cientista realiza-se entre 21 e 25 de julho - vem investigar connosco!

Pormenor de lâmpada

Candidaturas a decorrer de 01 a 30 de setembro.

Microplásticos no ocerano

O curso procura dar formação sobre a problemática da contaminação por detritos de plástico dos nossos ecossistemas, bem como alertar para os potenciais efeitos deletérios nos organismos, utilizando uma abordagem de ensino científico, com um discurso adequado a formandos sem formação científica - candidaturas até 03 de agosto.

Logótipo do evento, sobre fotografia dos Açores

Um simpósio internacional que reúne investigadores especializados em várias disciplinas (taxonomia, ecologia da vegetação, biogeografia, filogeografia, paleoecologia ou conservação da biodiversidade), focados na flora e vegetação terrestre e marinha da região da Macaronésia (Açores, Madeira, Selvagens, Canárias e Cabo Verde).

Quatro investigadores num laboratório

O curso visa capacitar investigadores, docentes e técnicos para integrar os princípios da economia circular em ambientes laboratoriais académicos - candidaturas até 17 de setembro.

Três investigadores num laboratório

O curso visa capacitar profissionais para aplicar os princípios da economia circular em ambientes laboratoriais industriais, promovendo práticas sustentáveis e eficientes - candidaturas até 17 de setembro.

Páginas