You can actually do much better than mere embeddings. Using program translations similar to what Haskell users routinely perform when using the do-notation for

You can actually do much better than mere embeddings. Using program translations similar to what Haskell users routinely perform when using the do-notation for monads, you can actually extend your type theory with new reasoning principles. See for instance the parametric exceptional theory [1], which adds well-behaved exceptions and allows to extend Coq with the independence of premises, i.e. (¬A → ∃n:ℕ. P n) → ∃n:ℕ. (¬A → P n). [1] https://hal.inria.fr/hal-01840643/document https://hal.inria.fr/hal-01840643/document