10:00 to 11:00
Lecture

The mystery of equality; the notion of type as a generalization of the notion of set

Thierry Coquand
Dependent type theory and mathematical formalization
10:00 to 11:00
    Salle 5, Site Marcelin Berthelot
    Open to all, subject to availability
    -

    Lecture outline:

    • how to represent the notion of equality in type theory;
    • Voevodsky stratification of types;
    • a uniform definition of the notion of equivalence;
    • principle of univalence;
    • application of mathematical structures to the notion of equality and comparison with set theory.

    Documents and media

    Speaker(s)

    Thierry Coquand

    Professor of Computer Science, University of Gothenburg, Sweden

    Events

    Lecture
    10:00 to 11:00
    Thierry Coquand

    Type theory, from Russell to de Bruijn
    Lecture
    10:00 to 11:00
    Thierry Coquand

    Natural deduction and models
    Lecture
    10:00 to 11:00
    Thierry Coquand

    Universe, paradoxes and standardization
    Lecture
    10:00 to 11:30
    Thierry Coquand

    Type theory and set theory
    Lecture
    10:00 to 11:00
    Thierry Coquand

    The mystery of equality; the notion of type as a generalization of the notion of …
    Lecture
    10:00 to 11:00
    Thierry Coquand

    Type theory models and the principle of univalence
    Lecture
    10:00 to 11:00
    Thierry Coquand

    Eilenberg-MacLane spaces and cohomology
    Lecture
    10:00 to 11:00
    Thierry Coquand

    Modalities and models of type theory

    See also

    Thierry Coquand, chair Computer Sciences and Digital Technologies
    Dependent type theory and mathematical formalization