YoVDO

Discrete and Codiscrete Modalities in Cohesive HoTT

Offered By: Hausdorff Center for Mathematics via YouTube

Tags

Type Theory Courses Topology Courses Differential Geometry Courses Homotopy Type Theory Courses

Course Description

Overview

Explore discrete and codiscrete modalities in Cohesive Homotopy Type Theory (HoTT) through this in-depth tutorial lecture. Delve into recent developments in modal extensions of homotopy type theory, examining their applications in synthetic formalizations of topology, differential geometry, and spectra. Gain insights into internal language presentations of cubical models of HoTT. Learn about the fibrational framework for modal simple and dependent type theories, the shape modality in real-cohesive HoTT, and covering spaces. Discover the intricacies of discrete and codiscrete modalities in cohesive HoTT, and explore differential cohesive HoTT. Benefit from the collaborative research efforts of experts in the field, including Jacob Gross, Max S. New, Ian Orton, Jennifer Paykin, Andrew M. Pitts, Egbert Rijke, Mitchell Riley, Urs Schreiber, Michael Shulman, and Bas Spitters.

Syllabus

Tutorial 3 Dan Licata: Discrete and Codiscrete Modalities in Cohesive HoTT


Taught by

Hausdorff Center for Mathematics

Related Courses

Introduction to programming with dependent types in Scala
Stepik
Georges Gonthier - Computer Proofs - Teaching Computers Mathematics, and Conversely
International Mathematical Union via YouTube
A Fibrational Framework for Modal Dependent Type Theories
Hausdorff Center for Mathematics via YouTube
A Fibrational Framework for Modal Simple Type Theories
Hausdorff Center for Mathematics via YouTube
Discrete and Codiscrete Modalities in Cohesive HoTT, II
Hausdorff Center for Mathematics via YouTube