The encode-decode method for equality types

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

• Alex Rice (University of Cambridge)
• Thursday 03 March 2022, 11:00-12:00
• FW09 - William Gates Building.

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.

This talk is included in these lists:

• FW09 - William Gates Building
• Logic & Semantics for Dummies
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.