[ADP-3153] Add fine-types-core package with Agda proofs

[HeinrichApfelmus]

This pull request adds a fine-types-core package which defines the core types Typ, Value and which implements embeddings such as A x (B + C) → (A x B) + (A x C).

Importantly, the definitions are written in Agda and exported to Haskell using agda2hs. The main properties are proven, in particular:

• Embeddings map the Typ as claimed.
• An embedding can be applied to a Value if the type checks (using hasTyp).

Issue number

ADP-3153