University of Cambridge > Talks.cam > Logic & Semantics for Dummies > The encode-decode method for equality types

The encode-decode method for equality types

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Alex Rice.

Identity types in Martin-Lof type theory are a powerful tool for reasoning about programs and mathematics. While induction on this type easily allows us to define lots of operations, it can be harder to give a concrete characterisation of the identity type. The encode-decode method is a generic technique for solving this problem.

I will give a recap of the definition of the identity type, describe the encode-decode method and give some examples of it on some basic types before giving a more involved example using univalence.

This talk is part of the Logic & Semantics for Dummies series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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