I think this is great. I think you should write a paper on it. I suspect it might need some kind of commutative diagram proof, i.e. if you express things in Co

I think this is great. I think you should write a paper on it. I suspect it might need some kind of commutative diagram proof, i.e. if you express things in CoC formalized within BLC you will get the same result as when you express in BLC formalized within CoC, I am not sure from the top of my head. (Kind of similar to showing that self-interpreting quoted interpreter on quoted program is the same as quoting the result of running the interpreter on the program.) And of course, this proof of equivalence should have formalization both in CoC (Lean?) and BLC. My hope is eventually someone writing a book on logic where the metalogic will be just untyped lambda calculus. Proofs will be just beta-reduction and judgemental equality. And everything will be in the form, let's study properties of these lambda terms that I came up with (the terms will of course represent some other logic such as CoC, simply typed LC, or even LC itself etc.).