Agda code accompanying "Typal Heterogeneous Equality Types" (updated)
Repository URI
Repository DOI
Change log
Authors
Pitts, Andrew https://orcid.org/0000-0001-7775-3471
Description
Updated Agda code (source code and html) for the paper "Typal Heterogeneous Equality Types" in ACM Trans. Comput. Logic 21, 3, Article 25 (March 2020). This dataset replaces https://doi.org/10.17863/CAM.47902
Version
Software / Usage instructions
Compiles with Agda version 2.6.0.1
Keywords
type theory, equality types, heterogeneous equality