# Type-theoretic interpretation of Skolemization

What is the type-theoretic interpretation / equivalent of Skolemization?

Skolemization converts some formula into Skolem normal form. The two formulae are equisatisfiable with each other.

Or, to say it in type-theoretic terms: There is a program having some type iff there is a program having this type in Skolem normal form.

How do these programs relate to each other?

• In fact I learned first about skolemization when programming in Haskell with existential types. – Turion Aug 15 '19 at 7:04

Skolemization corresponds to the so-called type theoretic axiom of choice, which is briefly discussed in section 1.6 of the HoTT book.

This provides an equivalence along which we can swap $$\Sigma$$ and $$\Pi$$ types. Assuming $$A : U$$, $$B : A \to U$$ and $$C : \prod_{a : A} B\,a \to U$$, we have an equivalence:

$$ac : \Big(\prod_{a : A}\sum_{b : B\,a}\,C\,a\,b\Big) \simeq \Big(\sum_{(b : \prod_{a : A} B\,a)} \prod_{a : A} C\,a\,(b\, a)\Big)$$

The proof of this very simple, e.g. in Agda we have the following (proving isomorphism instead of equivalence for simplicity now):

open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

iso : Set → Set → Set
iso A B =
∃₂ λ (f : A → B)(g : B → A) → (∀ x → f (g x) ≡ x) × (∀ x → g (f x) ≡ x)

ac : ∀ {A : Set}{B : A → Set}{C : ∀ a → B a → Set}
→ iso ((a : A) → Σ (B a) λ b → C a b)
(Σ ((a : A) → B a) λ b → (a : A) → C a (b a))
ac = (λ f → proj₁ ∘ f , proj₂ ∘ f)
, (λ {(b , c) a → b a , c a})
, (λ _ → refl)
, (λ _ → refl)


Going from left to right along the equivalence, we convert an existential variable into a function abstracting over the universal variable in scope. We can also use this iteratively, to move all $$\Sigma$$-s from a mixed-quantifier type to a prefix.

From a more operational perspective, this corresponds to lambda lifting, a program transformation used in compilers, which lifts definitions into an outer scope by adding extra function parameters for bound variables.