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
    Salle 5, Site Marcelin Berthelot
    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

    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