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

Esta é a pergunta que estamos a fazer a alumni de Ciências ULisboa. A resposta interessa-vos?

Seminário Doutoral, por Rita Sousa.

No dia 26 de maio, a comunidade de Ciências, em conjunto com especialistas de diferentes grupos taxonómicos, inventaria e regista toda a biodiversidade que consiga observar.

Seminário Helena Avelar de Astronomia e Astrologia Antiga, por Jeffrey Kotyk (University of British Columbia).

The main purpose of this course is to present new recent developments in integrated nested Laplace approximation (INLA) that is a method for approximate Bayesian inference.

In 2022, CQE Days will be held on the 26th and 27th of May at Ciências campus.

Um debate sobre o papel da bioinspiração no Design, na Arquitetura e no Planeamento Urbano.

Um ciclo de entrevistas com o objetivo de conhecer melhor os docentes do Departamento de Matemática de Ciências ULisboa. Gracinda Gomes é a entrevistada.

Candidaturas de 16 a 27 de maio de 2022.

Evento no âmbito do Ciclo de Conferências "Conversas à 6.ª", promovido pela redeMOV da Universidade de Lisboa.

Formação de Comunicação em Ciência(s), por Luís Morgado (Science Communication Office ITQB NOVA).

Sessão de apresentação dos Mestrados do Departamento de Informática.

Ação de formação para docentes, por Sofia Sá.

The objective of this course is to provide participants with basic knowledge on a) the fundamental aspects of experimental design and b) workflows, platforms and tools to increase reproducibility at all scientific levels.

A sessão conta com a presença do coordenador, docentes e alunos do Mestrado.

O National Geographic Summit está finalmente de volta!

Concurso de fotografia no âmbito do projeto "MigraWebs: Migradores como modeladores ecológicos sazonais das comunidades e funções ecossistémicas de áreas costeiras temperadas e tropicais", com candidaturas de 18 de abril a 31 de maio de 2022.

The course aims to provide a better understanding of how to use and customize NIMBLE's statistical algorithms.

Ação de formação para docentes, por Sofia Sá.

Seminários doutorais no âmbito do Doutoramento em Biologia de Ciências ULisboa.

The goal of this event is to allow PhD students from our research unit / faculty (LASIGE / FCUL), and other institutions, to disseminate their work and fostering knowledge sharing and cross-institution student collaborations.

Encontro de Comunicação de Ciência(s), por Diogo Veríssimo (Universidade de Oxford), Maria Vicente (Plataforma de Ciência Aberta) e Milene Matos (BioLiving; Município de Lousada).

As perspetivas epistemológicas acerca do arquivo, entendido enquanto realidade mas também como metáfora, sofreram transformações assinaláveis nos últimos anos.

Geometry Seminar, por Daniel Barlet (Institut Elie Cartan, Géométrie, Université de Lorraine, Nancy).

Sessão de apresentação de e-book no âmbito do projeto HOUSE (Hábitos e AlimentaçãO dos Universitários na SaúdE).