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

Seminário Doutoral III, no âmbito do Doutoramento em Biologia de Ciências ULisboa (Especialidade de Biologia Molecular), por Sofia Maria Sentieiro Neves.

Logótipo dos prémios

Muitos parabéns aos docentes e investigadores de Ciências premiados!

Colóquio no âmbito do projeto WineClimAdapt, que conta com participação de Ciências ULisboa.

Banner do Ciclo de Palestras

Ciclo de Palestras de Outono, promovidas pelo GAPsi - Gabinete de Apoio Psicológico.

Banner do Ciclo de Palestras

Ciclo de Palestras de Outono do GAPsi.

Colóquio de Matemática, por Bruno Loff (University of Porto).

Lisbon Workshop Series - AI Aesthetics and Philosophy of Technology.

Banner do Ciclo de Palestras

Ciclo de Palestras de Outono do GAPsi.

Currently, climate changes or alterations are known to be reflected on the stable isotope ratios of Hydrogen, Nitrogen, Carbon, Oxygen and Sulphur present in atmospheric gas forms, fresh or ocean water, as well as in plants and animals and organic matter in the soil.

Ação de formação para docentes.

Banner do Ciclo de Palestras

Ciclo de Palestras de Outono do GAPsi.

Cartaz da campanha

A campanha visa recolher o maior número possível de pilhas, baterias, lâmpadas, tinteiros e equipamentos elétricos usados.

Pormenor de mapa do continente europeu

Candidaturas online de 1 a 31 de dezembro de 2022.

The objective of this course is to acquire knowledge regarding bioinformatic tools available to predict nucleic acid (RNA, DNA or Nucleic Acids Mimics) and protein three-dimensional structure, as well as autonomy and critical thinking in the use of those tools.

Science is increasingly more present in our everyday decisions, with a fundamental role in global problems. Scientists, as the main actors in the production of scientific knowledge, have the responsibility of having an active voice in communicating this knowledge.

The course aims at introducing attendants to an updated state of the art of diversity of the soil biota and the functional roles played by soil organisms in key ecological processes.

Symbiosis is a key strategy for life on Earth. Nevertheless, although many research groups have long been committed to the study of symbiosis, its definition and functioning are not fully understood, and its ecological role and relevance are still underestimated.

This 5-day course offers to the participants a light microscopy course focusing on fluorescence microscopy techniques applied to the detection of proteins and glycans in tissue samples and cell cultures.

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.

The objective of this course is to provide students with basic knowledge of R programming, allowing them to manipulate and visualize data with R.

The objective of this course is to provide students with statistical knowledge and tools to manipulate, analyze and visualize biological data with R. Introduction to modeling, simulations and Bayesian statistics.

Under the general framework of Global Change Ecology, the goal of this course is to provide the participants with the most recent and practical knowledge on the use of Functional Diversity. This includes the selection of functional traits and calculation of Functional Diversity Indexes.

The course provides essential skills and knowledge that enable the participants to develop climate change adaptation strategies.

Logótipo do evento

Abstract submission will close on 14 November 2022.

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.