** Next:** From informal proofs to
** Up:** Theorem-proving in Agda
** Previous:** Theorem-proving in Agda
** Contents**
** Index**

The is an implementation of dependent type theory due to
Per Martin-Löf. Type theory is used as a
logical framework:
Different theories can be represented in type theory. In this section,
we represent several logical systems via interpretation due to
Heyting.
This is called a *shallow embedding*. We shall formalize
proofs in dependent type theory, and then express them in .

**Subsections**

Agda distribution team