Hello, I am working on a subtyping calculus of constructions: https://github.com/jfaure/Nimzo, based on Algebraic Subtyping [1] The goal is to leverage the synthesis of subtyping with the CoC for general purpose programming, both for the usual correctness guarantees, but additionally exceptional type inference and powerful optimizations by using subtyping relations on dependent types. I spent the last year researching the theory and practice for this, and with the compiler at now just over 3000 lines of Haskell, I feel like I am no longer advancing as quickly as I would like, so if anyone is interested in helping create this language of the future, please get in touch ! [1]: https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/thesis.pdf James Faure (Discord: J4#0303)