Mathematical Logic Webinar

A Constructive Proof of the Univalence Axiom

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

Seminário do Laboratório de Instrumentação e Física Experimental de Partículas, por Jonathan Hollar (LIP).

This colloquium seeks to debate ideas from the arts, humanities and sciences on the process of empathy.

Neuroscience and Neuromodeling Seminar, por Athanasios Vourvopoulos (LaSEEB, ISR, IST-ULisboa).

Banner do evento

No dia 6 de outubro, a ULisboa dá as boas-vindas aos seus estudantes na Cidade Universitária!

Geodiversidade

Palestra no âmbito das comemorações do Dia Internacional da Geodiversidade, por Carlos Marques da Silva (DG Ciências ULisboa).

Banner do evento

Celebrando o início de um novo Ano Académico, esta sessão solene é um importante marco na vida académica da ULisboa e junta toda a sua Comunidade.

Imagem ilustrativa do curso, acompanhada de diversas informações

Um curso dirigido ao público geral e estudantes de arte ou ciência (a partir dos 16 anos), com interesse em desenho de observação, ilustração, e biologia, com ou sem experiência em desenho.

Banner do evento

Talk @LASIGE, por Bruno Loff (Faculdade de Ciências, Universidade do Porto).

Logótipo do evento

The main goal of this annual conference is to expose students, engineers, scientists and the overall academic and scientific communities to the greatest recent advances in the fields of Technology, Health and Biomedical Engineering taking place in some of the most prestigious research institutions.

Banner do evento

Participe até 12 de outubro / Submit you application until 12 October.

Banner do evento

Ciências ULisboa estará presente, de 13 a 16 de outubro, no Festival Internacional de Ciência - FIC.A

Seminário Permanente de Filosofia das Ciências, por James Ladyman (University of Bristol).

Logótipo da iniciativa, sobre imagem alusiva à cibersegurança

A ciência rege-se por diferentes escalas de tempo. Diferentes áreas do conhecimento estudam processos a diferentes escalas: dos nanossegundos aos milhões de anos. Quais são os Andamentos da Ciência?

Cartaz do evento

Um evento repleto de atividades científicas, culturais e educativas, com jogos, demonstrações, palestras, entre muitas outras atividades. 

Research at the Faculty of Sciences

Join us on 26 October 2022 for the 4th edition of Ciências Research Day.