<p>the existence of dependent type theory implies the existence of codependent type theory</p>