Let $\Phi$ be a type functor definable in polymorphic lambda calculus:$$ \alpha : * \vdash \Phi(\alpha) : * $$$$ f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$Suppose further that $\Phi$-types form a filter:$$ \vdash \cap^{A,B}_\Phi(x,y) : \Phi(A) \to \Phi(B) \to \Phi(A \land B) $$Does there exist a type $\mu \Phi$ with the following properties:$\qquad \vdash a : \Phi(A)\quad \Longrightarrow \quad \vdash \varphi_{A,a} : \mu \Phi \to A$$\qquad \vdash \varphi_0 : \Phi(\mu \Phi)$(Intuitively, the denotation of $\mu\Phi$ should be $\bigcap \{ [\![A]\!] \mid \Phi(A) \}$.)If we put $\mu\Phi := \forall \alpha. (\Phi(\alpha) \to \alpha)$, then the first condition obtains via $\varphi_{A,a} = \lambda m. m A a$.  Is it always possible to satisfy the second condition too?  Or is there a counterexample?
Finite intersection property of polymorphic type families
lo.logic;lambda calculus;type systems;polymorphism