Higher inductive types are inductive types that include nontrivial higher-dimensional structure, represented as identifications that are not reflexivity. While work proceeds on type theories with a computational interpretation of univalence and higher inductive types, it is convenient to encode these structures in more traditional type theories with mature implementations. However, these encodings involve a great deal of error-prone additional syntax. We present a library that uses Agda’s metaprogramming facilities to automate this process, allowing higher inductive types to be specified with minimal additional syntax.
Mon 5 Nov
|08:30 - 09:00|
Paventhan VivekanandanIndiana University BloomingtonFile Attached
|09:00 - 09:30|
|09:30 - 10:00|