University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Schemas and semantics for Higher Inductive Types

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Schemas and semantics for Higher Inductive Types

Download to your calendar using vCal

If you have a question about this talk, please contact INI IT .

BPRW01 - Computer-aided mathematical proof

Higher inductive types are now an established tool of homotopy type theory, but many important questions about them are still badly-understood, including:can we set out a scheme defining “general HITs”, analogously to how CIC defines “general inductive types”?can we find a small specific collection of HITs from which one can construct “all HITs”, analogously to how the type-formers of MLTT suffice for inductive types?how can we model HITs (specific or general) in interesting homotopical settings?I will survey these questions and present what I know of progress on them (in particular, the cell monads semantics of Lumsdaine/Shulman https://arxiv.org/abs/1705.07088); I will also open the floor for interested audience members to briefly present other current work on these topics.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

The Goodman Centre Average on weekdays: 9007.0984456 kWh Anglia Ruskin University, HEL 310 (Helmore building - main campus entrance).

Other talks

Morning Break The rise of local cartography in Europe, 12th-14th century Title TBC Synthesizing Diverse Policies for Multi-Agent Coordination TBC Paediatric Medicine and Rheumatology
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity