Finally, we can escape the dreaded sigma types. DEVOID is still a bit picky (mostly about dependent pattern matching), but we still get functions and proofs for an entire class of dependent types for free from proofs about non-dependent versions of those types.
This looked a bit different from other classes of lifting. The details are a bit hairy at times. I hope to clear this up much more when I finish the formalization of the generalized algorithm.
Finally, we can escape the dreaded sigma types. DEVOID is still a bit picky (mostly about dependent pattern matching), but we still get functions and proofs for an entire class of dependent types for free from proofs about non-dependent versions of those types.
This looked a bit different from other classes of lifting. The details are a bit hairy at times. I hope to clear this up much more when I finish the formalization of the generalized algorithm.