10:00 to 11:00
Lecture

Type theory models and the principle of univalence

Thierry Coquand
Dependent type theory and mathematical formalization
10:00 to 11:00
    Mireille-Delmas-Marty Amphitheater, Marcelin-Berthelot Site
    Open to all, subject to availability
    -

    Lecture outline:

    • voevodsky model of simplicial sets and non-effectiveness of these models;
    • effective models with cubic sets;
    • application of a Quillen model structure definition to certain prebeam models;
    • constructive definition of homotopy types of topological spaces.

    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