YoVDO

A Fibrational Framework for Modal Dependent Type Theories

Offered By: Hausdorff Center for Mathematics via YouTube

Tags

Mathematics Courses Computer Science Courses Homotopy Type Theory Courses

Course Description

Overview

Explore a comprehensive lecture on modal dependent type theories within the Hausdorff Trimester Program: Types, Sets and Constructions. Delve into recent developments in homotopy type theory extensions, their design frameworks, and applications in real-cohesive and differential-cohesive HoTT. Learn about the fibrational framework for modal simple and dependent type theories, shape modality in real-cohesive HoTT, covering spaces, and discrete and codiscrete modalities in cohesive HoTT. Examine the intricate relationships between unary type theory, structural rules, mode theories, parameterized spectra, and dependency. Gain insights into the subtle aspects of mode theory for simple and dependent types, as well as the complexities of modalities and modal dependent type theories. This lecture, part of a series, presents collaborative work by renowned researchers in the field of type theory and its applications to topology, differential geometry, and spectra.

Syllabus

Intro
Analogy
Unary type theory
Structural Rules
Mode theories
Parametrized spectra
Dependency
Simple type theory
Dependent type theory
Subtle Parts
Mode Theory for Simple Types
Mode Theory for Dependent Types
Modalities
Modal dependent type theories


Taught by

Hausdorff Center for Mathematics

Related Courses

Probabilistic Graphical Models 1: Representation
Stanford University via Coursera
Computer Security
Stanford University via Coursera
Intro to Computer Science
University of Virginia via Udacity
Introduction to Logic
Stanford University via Coursera
Internet History, Technology, and Security
University of Michigan via Coursera