# Existential quantification

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2022-02-08.

module foundation.existential-quantification where

Imports
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.logical-equivalences
open import foundation.propositional-extensionality
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.propositions


## Idea

Given a family of propositions P over A, the existential quantification of P over A is the proposition ∃ A P asserting that there is an element a : A such that P a holds. We use the propositional truncation to define the existential quantification,

  ∃ (x : A), (P x) := ║ Σ (x : A), (P x) ║₋₁


because the Curry-Howard interpretation of the existential quantification as Σ A P does not guarantee that existential quantifications are interpreted as propositions.

The universal property of existential quantification states that it is the least upper bound on the family of propositions P in the locale of propositions, by which we mean that for every proposition Q we have the logical equivalence

  (∀ (x : A), (P x ⇒ Q)) ⇔ ((∃ (x : A), (P x)) ⇒ Q).


## Definitions

### Existence of structure

Given a structure B : A → 𝒰 on a type A, the propositional truncation

  ║ Σ (x : A), (B x) ║₋₁


satisfies the universal property of the existential quantification

  ∃ (x : A), ║ B x ║₋₁


and is thus equivalent to it. Therefore, we may reasonably call this construction the existential quantification of structure. It is important to keep in mind that this is not a generalization of the concept but rather a conflation, and should be read as the statement the type of elements x : A equipped with y : B x is inhabited.

Existence of structure is a widely occurring notion in univalent mathematics. For instance, the condition that an element y : B is in the image of a map f : A → B is formulated using existence of structure: The element y is in the image of f if the type of x : A equipped with an identification f x = y is inhabited.

Because subtypes are a special case of structure, and Agda can generally infer structures for us, we will continue to conflate the two in our formalizations for the benefit that we have to specify the subtype in our code less often. For instance, even though the introduction rule for existential quantification intro-exists is phrased in terms of existential quantification on structures, it equally applies to existential quantification on subtypes.

module _
{l1 l2 : Level} (A : UU l1) (B : A → UU l2)
where

exists-structure-Prop : Prop (l1 ⊔ l2)
exists-structure-Prop = trunc-Prop (Σ A B)

exists-structure : UU (l1 ⊔ l2)
exists-structure = type-Prop exists-structure-Prop

is-prop-exists-structure : is-prop exists-structure
is-prop-exists-structure = is-prop-type-Prop exists-structure-Prop


### Existential quantification

module _
{l1 l2 : Level} (A : UU l1) (P : A → Prop l2)
where

exists-Prop : Prop (l1 ⊔ l2)
exists-Prop = exists-structure-Prop A (type-Prop ∘ P)

exists : UU (l1 ⊔ l2)
exists = type-Prop exists-Prop

abstract
is-prop-exists : is-prop exists
is-prop-exists = is-prop-type-Prop exists-Prop

∃ : Prop (l1 ⊔ l2)
∃ = exists-Prop


### The introduction rule for existential quantification

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
where

intro-exists : (a : A) (b : B a) → exists-structure A B
intro-exists a b = unit-trunc-Prop (a , b)


Note. Even though the introduction rule is formalized in terms of existential quantification on structures, it equally applies to existential quantification on subtypes. This is because subtypes are a special case of structure. The benefit of this approach is that Agda can infer structures for us, but not generally subtypes.

### The universal property of existential quantification

module _
{l1 l2 l3 : Level} (A : UU l1) (B : A → UU l2) (S : Prop l3)
where

universal-property-exists-structure : UUω
universal-property-exists-structure =
{l : Level} (Q : Prop l) →
(type-Prop S → type-Prop Q) ↔ ((x : A) → B x → type-Prop Q)

module _
{l1 l2 l3 : Level} (A : UU l1) (P : A → Prop l2) (S : Prop l3)
where

universal-property-exists : UUω
universal-property-exists =
universal-property-exists-structure A (type-Prop ∘ P) S


## Properties

### The elimination rule of existential quantification

The universal property of existential quantification states ∃ A P is the least upper bound on the predicate P in the locale of propositions.

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
where

ev-intro-exists :
{C : UU l3} → (exists-structure A B → C) → (x : A) → B x → C
ev-intro-exists H x p = H (intro-exists x p)

elim-exists :
(Q : Prop l3) →
((x : A) → B x → type-Prop Q) → (exists-structure A B → type-Prop Q)
elim-exists Q f = map-universal-property-trunc-Prop Q (ind-Σ f)

abstract
is-equiv-ev-intro-exists :
(Q : Prop l3) → is-equiv (ev-intro-exists {type-Prop Q})
is-equiv-ev-intro-exists Q =
is-equiv-has-converse
( function-Prop (exists-structure A B) Q)
( Π-Prop A (λ x → function-Prop (B x) Q))
( elim-exists Q)


### The existential quantification satisfies the universal property of existential quantification

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
where

up-exists :
universal-property-exists-structure A B (exists-structure-Prop A B)
up-exists Q = (ev-intro-exists , elim-exists Q)


### Propositions that satisfy the universal property of a existential quantification are equivalent to the existential quantification

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (Q : Prop l3)
(up-Q : universal-property-exists-structure A B Q)
where

forward-implication-iff-universal-property-exists :
exists-structure A B → type-Prop Q
forward-implication-iff-universal-property-exists =
elim-exists Q (forward-implication (up-Q Q) id)

backward-implication-iff-universal-property-exists :
type-Prop Q → exists-structure A B
backward-implication-iff-universal-property-exists =
backward-implication (up-Q (exists-structure-Prop A B)) intro-exists

iff-universal-property-exists :
exists-structure A B ↔ type-Prop Q
iff-universal-property-exists =
( forward-implication-iff-universal-property-exists ,
backward-implication-iff-universal-property-exists)


### Existential quantification of structure is the same as existential quantification over its propositional reflection

We proceed by showing that the latter satisfies the universal property of the former.

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
where

universal-property-exists-structure-exists-trunc-Prop :
universal-property-exists-structure A B (exists-Prop A (trunc-Prop ∘ B))
universal-property-exists-structure-exists-trunc-Prop Q =
( λ f a b → f (unit-trunc-Prop (a , unit-trunc-Prop b))) ,
( λ f → rec-trunc-Prop Q (λ (a , |b|) → rec-trunc-Prop Q (f a) |b|))

compute-exists-trunc-Prop : exists-structure A B ↔ exists A (trunc-Prop ∘ B)
compute-exists-trunc-Prop =
iff-universal-property-exists
( exists-Prop A (trunc-Prop ∘ B))
( universal-property-exists-structure-exists-trunc-Prop)


### Taking the cartesian product with a proposition distributes over existential quantification of structures

module _
{l1 l2 l3 : Level} (P : Prop l1) {A : UU l2} {B : A → UU l3}
where

map-distributive-product-exists-structure :
type-Prop P × exists-structure A B →
exists-structure A (λ x → type-Prop P × B x)
map-distributive-product-exists-structure (p , e) =
elim-exists
( exists-structure-Prop A (λ x → type-Prop P × B x))
( λ x q → intro-exists x (p , q))
( e)

map-inv-distributive-product-exists-structure :
exists-structure A (λ x → type-Prop P × B x) →
type-Prop P × exists-structure A B
map-inv-distributive-product-exists-structure =
elim-exists
( P ∧ exists-structure-Prop A B)
( λ x (p , q) → (p , intro-exists x q))

iff-distributive-product-exists-structure :
( type-Prop P × exists-structure A B) ↔
( exists-structure A (λ x → type-Prop P × B x))
iff-distributive-product-exists-structure =
( map-distributive-product-exists-structure ,
map-inv-distributive-product-exists-structure)

eq-distributive-product-exists-structure :
P ∧ exists-structure-Prop A B ＝
exists-structure-Prop A (λ x → type-Prop P × B x)
eq-distributive-product-exists-structure =
eq-iff'
( P ∧ exists-structure-Prop A B)
( exists-structure-Prop A (λ x → type-Prop P × B x))
( iff-distributive-product-exists-structure)


### Conjunction distributes over existential quantification

module _
{l1 l2 l3 : Level} (P : Prop l1) {A : UU l2} (Q : A → Prop l3)
where

map-distributive-conjunction-exists :
type-Prop (P ∧ (∃ A Q) ⇒ ∃ A (λ x → P ∧ Q x))
map-distributive-conjunction-exists =
map-distributive-product-exists-structure P

map-inv-distributive-conjunction-exists :
type-Prop (∃ A (λ x → P ∧ Q x) ⇒ P ∧ (∃ A Q))
map-inv-distributive-conjunction-exists =
map-inv-distributive-product-exists-structure P

iff-distributive-conjunction-exists :
type-Prop (P ∧ ∃ A Q ⇔ ∃ A (λ x → P ∧ Q x))
iff-distributive-conjunction-exists =
iff-distributive-product-exists-structure P

eq-distributive-conjunction-exists :
P ∧ (∃ A Q) ＝ ∃ A (λ x → P ∧ Q x)
eq-distributive-conjunction-exists =
eq-distributive-product-exists-structure P


• Existential quantification is the indexed counterpart to disjunction

## Table of files about propositional logic

The following table gives an overview of basic constructions in propositional logic and related considerations.

ConceptFile
Propositions (foundation-core)foundation-core.propositions
Propositions (foundation)foundation.propositions
Subterminal typesfoundation.subterminal-types
Subsingleton inductionfoundation.subsingleton-induction
Empty types (foundation-core)foundation-core.empty-types
Empty types (foundation)foundation.empty-types
Unit typefoundation.unit-type
Logical equivalencesfoundation.logical-equivalences
Propositional extensionalityfoundation.propositional-extensionality
Mere logical equivalencesfoundation.mere-logical-equivalences
Conjunctionfoundation.conjunction
Disjunctionfoundation.disjunction
Exclusive disjunctionfoundation.exclusive-disjunction
Existential quantificationfoundation.existential-quantification
Uniqueness quantificationfoundation.uniqueness-quantification
Universal quantificationfoundation.universal-quantification
Negationfoundation.negation
Double negationfoundation.double-negation
Propositional truncationsfoundation.propositional-truncations
Universal property of propositional truncationsfoundation.universal-property-propositional-truncation
The induction principle of propositional truncationsfoundation.induction-principle-propositional-truncation
Functoriality of propositional truncationsfoundation.functoriality-propositional-truncations
Propositional resizingfoundation.propositional-resizing
Impredicative encodings of the logical operationsfoundation.impredicative-encodings