Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Homotopy Type Theory

In course

MATH-225: Topology II - fundamental groups

On étudie des notions de topologie générale: unions et quotients d'espaces topologiques; on approfondit les notions de revêtements et de groupe fondamental,et d'attachements de cellules et on démontre le Théorème de Seifert-van Kampen. Des exemples de surf ...

Description

This lecture introduces the concept of homotopy type theory, focusing on equivalences and contractible spaces. It covers examples of homotopy equivalences, pushouts, and applications of homotopy type theory. The lecture also explores defining spawned versions and paths in homotopy type theory.

Instructors (2)

Jérôme Scherer

Dimitri Stelio Wyss

Official source

Related concepts (30)

Homotopy theory

In mathematics, homotopy theory is a systematic study of situations in which maps can come with homotopies between them. It originated as a topic in algebraic topology but nowadays is studied as an independent discipline. Besides algebraic topology, the theory has also been used in other areas of mathematics such as algebraic geometry (e.g., A1 homotopy theory) and (specifically the study of ). In homotopy theory and algebraic topology, the word "space" denotes a topological space.

Homotopy type theory

In mathematical logic and computer science, homotopy type theory (HoTT hɒt) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies. This includes, among other lines of work, the construction of homotopical and models for such type theories; the use of type theory as a logic (or internal language) for abstract homotopy theory and ; the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible); and the formalization of each of these in computer proof assistants.

Homotopy group

In mathematics, homotopy groups are used in algebraic topology to classify topological spaces. The first and simplest homotopy group is the fundamental group, denoted which records information about loops in a space. Intuitively, homotopy groups record information about the basic shape, or holes, of a topological space. To define the n-th homotopy group, the base-point-preserving maps from an n-dimensional sphere (with base point) into a given space (with base point) are collected into equivalence classes, called homotopy classes.

Homotopy

In topology, a branch of mathematics, two continuous functions from one topological space to another are called homotopic (from ὁμός "same, similar" and τόπος "place") if one can be "continuously deformed" into the other, such a deformation being called a homotopy (həˈmɒtəpiː, ; ˈhoʊmoʊˌtoʊpiː, ) between the two functions. A notable use of homotopy is the definition of homotopy groups and cohomotopy groups, important invariants in algebraic topology. In practice, there are technical difficulties in using homotopies with certain spaces.

Stable homotopy theory

In mathematics, stable homotopy theory is the part of homotopy theory (and thus algebraic topology) concerned with all structure and phenomena that remain after sufficiently many applications of the suspension functor. A founding result was the Freudenthal suspension theorem, which states that given any pointed space , the homotopy groups stabilize for sufficiently large. In particular, the homotopy groups of spheres stabilize for . For example, In the two examples above all the maps between homotopy groups are applications of the suspension functor.

Related lectures (32)

Homotopy Theory: Cylinders and Path Objects

Covers cylinders, path objects, and homotopy in model categories.

Fundamental Groups

Explores fundamental groups, homotopy classes, and coverings in connected manifolds.

Understanding Lifting Properties in Homotopy Theory

Focuses on lifting properties in homotopy theory of chain complexes.

The Whitehead Lemma: Homotopy Equivalence in Model Categories

Explores the Whitehead Lemma, showing when a morphism is a weak equivalence.

Homotopy Theory of Chain Complexes