Contents

# Contents

## Idea

A notion of equality in type theory involving the notion of judgement. In homotopy type theory it is used synonymously with definitional equality as contrasted with propositional equality.

## 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)

Last revised on August 24, 2020 at 10:08:20. See the history of this page for a list of all contributions to it.