Interesting work making some ideas around embedding domain-specific type theories in a broader language.
