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?
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.
