Mathematical Logic Webinar

A Constructive Proof of the Univalence Axiom (Part II)


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.

CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Logótipo da Rede Campus Sustentável

A iniciativa tem como objetivo promover uma reflexão coletiva alargada sobre o futuro que queremos para a Rede Campus Sustentável (RCS).

Inscrições até 24 de junho de 2022.

Logótipo da iniciativa e respetivas datas

Candidaturas a Monitores até 21 de junho.

Novas datas: 04 a 08 julho 2022.

Philosophical metatheories have had a great development in recent times. They have been used to reconstruct theories in many different scientific fields, from physics to biology to the social sciences. However, they lack means to systematically test the adequacy of their products.

Seminário do Centro de Física Teórica e Computacional, por Artem Ryabov (Charles University, Prague, Czech Republic).


Um programa dirigido aos alunos de Licenciatura e de 1.º ano de Mestrado.

Cognitive sciences have approached social cognition from two complementary perspectives. On one hand, social psychology and behavioural economics have mostly emphasized mentalizing, social perception, and our ability to model other minds. On the other hand, developmental psychology and motor neuroscience have more focused on imitating, social interaction, and our propensity to coordinate with others’ behaviour. 

The course aims at enabling the participants to use different methods to measure the impacts of pollutants on ecosystems. Basic knowledge will be provided through theoretical and practical lessons on how to select and use the most suitable metrics based on the analysis of multiple compartments of the ecosystems.

O evento visa reunir investigadores interessados na aplicação de isótopos estáveis em estudos ecológicos e na utilização de dados históricos de biodiversidade disponíveis em coleções museológicas.

Logótipo e data do evento

“There is often a considerable difference between what we think people need and what people want to use”. This is our perspective on how technology should be developed and will serve as the motto of this event.

Título e data do evento, sobre uma fotografia da Ponte Vasco da Gama (Lisboa)

O evento decorre de 12 a 14 de julho de 2022, sob o lema CHEMISTRY: Forging bonds, e destina-se a todos os investigadores e alunos da ULisboa.

Banner do evento

The program will consist of plenary lectures, oral, flash and poster communications, and a round table about Science Communication.

This course offers an overview of the different ways to measure biodiversity, and provides tips for the stratification of primary biodiversity data and the construction of variables that describe its various facets. It also includes an in-depth review of the different types of data used to measure biodiversity and their problems and limitations.

Banner do evento

Estaremos hoje habilitados a prever o impacto da atividade humana no clima e a inferir daí a insustentabilidade do nosso modo de vida?

Logótipo do programa

Após 2 anos de interregno, o programa Ser Cientista está de regresso!

Fotografia de campo agrícola e parque eólico

Submissão de iniciativas até 30 de agosto de 2022.

Fotografia de trator em campo agrícola

Submissão de iniciativas até 30 de agosto de 2022.

Fotografia representativa de agricultura sustentável

Submissão de iniciativas até 30 de agosto de 2022.

Programa a disponibilizar futuramente.