It causes trouble for non-constructive logics, too. Any logic with an identity principle will be made inconsistent with the inclusion of `fix : forall a . (a -&gt; a) -&gt; a`.<p>By yours are you referring to `forall a . a -&gt; a`? I don&#x27;t see how that principle is troubling at all.