nLab
judgmental equality

Contents

Context

Type theory

Equality and Equivalence

Contents

Idea

A notion of equality in type theory involving the notion of judgement.

References

  • Robin Adams, Pure type systems with judgemental equality, Journal of Functional Programming, Volume 16 Issue 2(2006) (web)

  • Vincent Siles, Hugo Herbelin, Equality is typable in semi-full pure type systems (pdf)

Created on September 18, 2012 at 21:32:22. See the history of this page for a list of all contributions to it.