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

Apresentação dos trabalhos desenvolvidos no âmbito do programa Estágios de Verão CEAUL - Sê Investigador.

Logótipo do EVM 2024

Por Giosuè Muratore (DM Ciências ULisboa e CMAFcIO).

Título do programa, sobre mosaico de fotografias de jovens cientistas

As candidaturas encontram-se encerradas. Obrigada aos quase 80 candidatos/as!

Logótipo do EVM 2024

Por Pedro Duarte (DM Ciências ULisboa, CMAFcIO).

Seminário do Centro de Matemática, Aplicações Fundamentais e Investigação Operacional, por Baptiste Claustre (aluno ENS Lyon, estagiário CMAFcIO).

Fotografia de ilha

Seminários Doutorais no âmbito da disciplina de Projeto de Investigação (Doutoramento em Ciências do Mar).

Logótipo do EVM 2024

Por Maria Manuel Torres (DM Ciências ULisboa e CMAFcIO).

Titulo e data do evento, com imagem de ponte sobre o tejo

Um evento organizado no âmbito da Ação COST EURO-MIC, de cujo Comitê de Gestão Elisabete Silva, líder do Bioactive and Multifunctional Materials Lab do BioISI, faz parte.

Logótipo do EVM 2024

Por: Jorge Buescu (DM Ciências ULisboa e CMAFcIO).

Logótipo do EVM 2024

Por Jean-Baptiste Casteras (DM Ciências ULisboa e CMAFcIO).

Chegou a hora: os participantes do Programa Ser Cientista vão apresentar os projetos que desenvolveram ao longo de uma semana, acompanhados por docentes e investigadores de CIÊNCIAS. E todos podem assistir!

Imagem do evento

Extended enrolement date until July 12th.

Logótipo do evento, sobre um fundo branco

Um evento de reunião da comunidade nacional nas diversas vertentes da informática, com a ambição de ser o fórum de eleição para a divulgação, discussão e reconhecimento de trabalhos científicos.

Are you ready for this year's edition?

Imagem do evento - título, local e data do evento

Investigação Ecológica ao Serviço da Conservação

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