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

    Type theory, from Russell to de Bruijn
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Natural deduction and models
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Universe, paradoxes and standardization
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Type theory and set theory
    Thierry Coquand

    Lecture
    10:00 to 11:30

    The mystery of equality; the notion of type as a generalization of the notion of …
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Type theory models and the principle of univalence
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Eilenberg-MacLane spaces and cohomology
    Thierry Coquand

    Lecture
    10:00 to 11:00

    Modalities and models of type theory
    Thierry Coquand

    Lecture
    10:00 to 11:00

    See also

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