# Finite intersection property of polymorphic type families

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:

1. $\qquad \vdash a : \Phi(A)\quad \Longrightarrow \quad \vdash \varphi_{A,a} : \mu \Phi \to A$
2. $\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?

• What goes wrong if we define $\Phi(A)=\bot$ for all $A$? Then $\varphi_0$ should probably not exist...
– cody
Jul 6 '17 at 13:28
• I think that works! Jul 7 '17 at 14:40