University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Impredicative encodings in HoTT

  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

Impredicative encodings in HoTT

Download to your calendar using vCal

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

BPRW01 - Computer-aided mathematical proof

We investigate the prospects for impredicative encodings of inductive types (including higher inductive types) in HoTT.  It is well-known that encoding inductives using higher-order quantification provides a potential theoretical and practical simplification of the system.  Using the further resources available in HoTT allows for a sharpening of the familiar System F style impredicative encodings of inductive types, but this begs the question of whether impredicativity is formally compatible with univalence.  We give a realizability model using a combination of topos-theoretic, homotopical, and recent cubical methods.  Joint work with Jonas Frey and Pieter Hofstra.

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

2d to 3d equation sets and implication of super massive blackholes Bateman Auditorium, Gonville & Caius Horizon: Bioengineering

Other talks

Title to be confirmed Group Work Rothschild Public Lecture: The Quantum Centenary: from Order to Chaos The Importance of Teaching about Science and Religion in a Time of Global Uncertainty Morning Tea and Coffee Human monogamy in mammalian context
 

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