Remove last vestiges of meta language in derived definitions.

Need to have elimUnit and elimPair as primitives because our type theory
does not currently assume eta-equality.

Also I'm technically still using an Agda dependent record here, but
only because Agda's module system makes it so nice to namespace things.
Turning the record into a nested Sigma and manually defining functions
parameterized by those records is a minor translation.