<p>Skolemization corresponds to the so-called type theoretic axiom of choice, which is briefly discussed in section 1.6 of the <a href="https://hott.github.io/book/nightly/hott-online-1212-g0d25f68.pdf" rel="noreferrer">HoTT book</a>.</p>

<p>This provides an equivalence along which we can swap <span class="math-container">$\Sigma$</span> and <span class="math-container">$\Pi$</span> types. Assuming <span class="math-container">$A : U$</span>, <span class="math-container">$B : A \to U$</span> and <span class="math-container">$C : \prod_{a : A} B\,a \to U$</span>, we have an equivalence:</p>

<p><span class="math-container">$$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)$$</span></p>

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

<pre><code>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)
</code></pre>

<p>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 <span class="math-container">$\Sigma$</span>-s from a mixed-quantifier type to a prefix.</p>

<p>From a more operational perspective, this corresponds to <a href="https://en.wikipedia.org/wiki/Lambda_lifting" rel="noreferrer">lambda lifting</a>, a program transformation used in compilers, which lifts definitions into an outer scope by adding extra function parameters for bound variables.</p>

CC BY-SA 4.0
2019-08-14T18:24:55.353Z
2019-08-14T19:25:33.980Z
2019-08-14T19:25:33.980Z
András Kovács
<p>What is the type-theoretic interpretation / equivalent of Skolemization?</p>

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

<p>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.</p>

<p>How do these programs relate to each other?</p>

CC BY-SA 4.0
2019-08-15T07:04:27.187Z
In fact I learned first about skolemization when programming in Haskell with existential types.
Turion
<type-theory><curry-howard>
Type-theoretic interpretation of Skolemization
Manuel Jacob
# Type-theoretic interpretation of Skolemization

(Asked by: username_0 on 2019-08-14)

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?

**Tags:** type-theory, curry-howard
> **Comments:**
> **username_1**: In fact I learned first about skolemization when programming in Haskell with existential types.  

---

## 1 answers

### Answer by username_2 on 2019-08-14. Score: 10

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.


---

