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
Pintura abstrata em tons de azul, laranja e amarelo

Seminário do Centro de Física Teórica e Computacional, por Mariana Oliveira (ICECO - Aveiro Institute of Materials, University of Aveiro, Portugal).

Logótipo C-Academy

Combinando teoria e prática, o curso prepara os alunos para compreenderem a infraestrutura digital moderna e aplicarem esses conhecimentos em cenários reais, com foco em arquiteturas robustas, deteção de erros e soluções para redes de alto desempenho.

Representação de folhas de árvores

Concerto no âmbito do programa Música na Universidade de Lisboa.

Alunos de CIÊNCIAS

Uma iniciativa gratuita, dirigida aos estudantes do 1.º e 2.º ciclo de estudos de CIÊNCIAS, com inscrições até 20 de março.

Seminário do Departamento de Física de Ciências ULisboa, por Masahiro Takagi (Kyoto Sangyo University, Kyoto, Japan).

Título/data/local do evento e fotografia do orador

Talk @DI, por João Pedro Carvalho.

Data da edição de 2025 da Futurália

CIÊNCIAS vai estar presente, uma vez mais, no stand da Universidade de Lisboa.

Título "Cybersecurity Executive Program Edição 2025", sobre um fundo em tons de verde

Adotar boas medidas e práticas de Cibersegurança é fundamental nos dias de hoje, para qualquer empresa, para proteger a integridade, confidencialidade e disponibilidade de dados sensíveis e pessoais, reduzindo o risco de ataques e fraudes.

Seminário do Instituto de Astrofísica e Ciências do Espaço, por Edmund J. Copeland.

Título/data/local do evento e representação de floresta

Esta é a altura certa para fazer os últimos preparativos para uma agrofloresta viçosa e produtiva que nos dará fruta, biodiversidade e sombra nos meses mais quentes.

Fotografia de criança a observar plantas com uma lupa

This course aims to explore ways of communicating science to non-specialized audiences, such as policy makers, industry, general public (including students and teachers), through their engagement and participation in citizen science activities.

Logótipo da Semana da Sustentabilidade

O foco da da SDS’25 é abrir espaço à reflexão sobre como as nossas ações, hoje, poderão influenciar o amanhã, sendo, assim, o lema desta Edição “Pelo Futuro, o Amanhã começa Hoje“.

Conferência por António Vidigal (Consultor Independente e Representante do Conselho Consultivo Industrial no Conselho Diretivo do Programa UT Austin Portugal).

Reitoria da ULisboa

O ato eleitoral decorrerá nos dias 31 de março e 01 de abril de 2025.

Sala de aula

Curso creditado para efeitos de progressão na carreira dos professores do Ensino Secundário dos grupos 500 e 550, com candidaturas até 25 de março.

Fotografia de coleção de insetos

The course includes several case studies of insect adaptation, and the most recent overview on insect evodevo, plasticity, ecophysiological responses and conservation under global change.

Título/data/local do evento e fotografia aérea de vias urbanas

Conferência da redeMOV, por Gabriel Costa Valença.

Logótipos do evento/Ciências ULisboa/AEFCL e data do evento, sobre fotografia de edição anterior

O maior evento de empregabilidade de CIÊNCIAS, a decorrer nos dias 08 e 09 de abril.

A leading venue for presenting and discussing the latest research, industrial practice and innovations in dependable and secure computing.

Título do evento

A collaborative initiative supported by five Portuguese research centers, aimed at strengthening and connecting the geometry research community in Portugal.

Título/data/local do evento e fotografia da cidade de Lisboa

The conference aims to bring together students and young researchers working in Mathematics, Statistics, and Applications with a view to fostering discussions and collaborations amongst participants.

Título "Para um ensino humanista das ciências" e logótipos das entidades organizadoras

O evento tem como tema principal "Para um ensino humanista das ciências" e conta com a participação de vários professores de CIÊNCIAS.

Microplásticos em suspensão no oceano

O curso tem como objetivo 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 - candidaturas até 22 de março.

Banner do Dia de Ciências 2025

A 29 de abril assinalamos o 114.º aniversário de CIÊNCIAS.

Junte-se a nós no Grande Auditório de CIÊNCIAS para uma tarde de celebração que reúne toda a comunidade da Faculdade.

Páginas