Definitions allow for reuse of code. Dependently typed programming languages can automatically unfold definitions as part of the type-checking process, but excessive unfolding can lead to types that are hard to read, or performance issues. This problem can be mitigated through the use of opaque definitions, which can be selectively unfolded. However, subject reduction fails to hold for certain designs.

We study the meta-theory of a type theory with opaque definitions, inspired by Agda. We give typing and reduction rules and show that the type theory enjoys properties like subject reduction, normalization, consistency, and decidability of conversion. The development is fully mechanized in Agda.