Existential quantification

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

Created on 2022-02-08.
Last modified on 2023-12-12.

module foundation.existential-quantification where
Imports
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.logical-equivalences
open import foundation.propositional-extensionality
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.equivalences
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, because the Curry-Howard interpretation of the existential quantification as Σ A P does not guarantee that existential quantifications are interpreted as propositions.

Definition

Existential quantification for families of propositions

exists-Prop :
  {l1 l2 : Level} (A : UU l1) (P : A  Prop l2)  Prop (l1  l2)
exists-Prop {l1} {l2} A P = trunc-Prop (Σ A  x  type-Prop (P x)))

exists :
  {l1 l2 : Level} (A : UU l1) (P : A  Prop l2)  UU (l1  l2)
exists A P = type-Prop (exists-Prop A P)

abstract
  is-prop-exists :
    {l1 l2 : Level} (A : UU l1) (P : A  Prop l2)  is-prop (exists A P)
  is-prop-exists A P = is-prop-type-Prop (exists-Prop A P)

Existential quantification of arbitrary type families

∃-Prop :
  {l1 l2 : Level} (A : UU l1) (B : A  UU l2)  Prop (l1  l2)
∃-Prop A B = trunc-Prop (Σ A B)

 :
  {l1 l2 : Level} (A : UU l1) (B : A  UU l2)  UU (l1  l2)
 A B = type-Prop (∃-Prop A B)

is-prop-∃ :
  {l1 l2 : Level} (A : UU l1) (B : A  UU l2)  is-prop ( A B)
is-prop-∃ A B = is-prop-type-Prop (∃-Prop A B)

Properties

The introduction rule for existential quantification

intro-exists :
  {l1 l2 : Level} {A : UU l1} (P : A  Prop l2) 
  (x : A)  type-Prop (P x)  exists A P
intro-exists P x p = unit-trunc-Prop (pair x p)

intro-∃ :
  {l1 l2 : Level} {A : UU l1} {B : A  UU l2} (a : A) (b : B a) 
   A B
intro-∃ a b = unit-trunc-Prop (pair a b)

The elimination rule and the universal property of existential quantification

ev-intro-exists-Prop :
  {l1 l2 l3 : Level} {A : UU l1} (P : A  Prop l2) (Q : Prop l3) 
  type-hom-Prop (exists-Prop A P) Q  (x : A)  type-hom-Prop (P x) Q
ev-intro-exists-Prop P Q H x p = H (intro-exists P x p)

elim-exists-Prop :
  {l1 l2 l3 : Level} {A : UU l1} (P : A  Prop l2) (Q : Prop l3) 
  ((x : A)  type-hom-Prop (P x) Q)  type-hom-Prop (exists-Prop A P) Q
elim-exists-Prop P Q f =
  map-universal-property-trunc-Prop Q (ind-Σ f)

abstract
  is-equiv-ev-intro-exists-Prop :
    {l1 l2 l3 : Level} (A : UU l1) (P : A  Prop l2) (Q : Prop l3) 
    is-equiv (ev-intro-exists-Prop P Q)
  is-equiv-ev-intro-exists-Prop A P Q =
    is-equiv-is-prop
      ( is-prop-type-hom-Prop (exists-Prop A P) Q)
      ( is-prop-Π ((λ x  is-prop-type-hom-Prop (P x) Q)))
      ( elim-exists-Prop P Q)

is-least-upper-bound-exists-Prop :
  {l1 l2 l3 : Level} {A : UU l1} (P : A  Prop l2) (Q : Prop l3) 
  ((a : A)  type-hom-Prop (P a) Q)  type-hom-Prop (exists-Prop A P) Q
pr1 (is-least-upper-bound-exists-Prop P Q) = elim-exists-Prop P Q
pr2 (is-least-upper-bound-exists-Prop P Q) h a p = h (intro-∃ a p)

Conjunction distributes over existential quatification

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

  iff-distributive-conjunction-exists-Prop :
    ( conjunction-Prop P (exists-Prop A Q)) 
    ( exists-Prop A  a  conjunction-Prop P (Q a)))
  pr1 iff-distributive-conjunction-exists-Prop (p , e) =
    elim-exists-Prop Q
      ( exists-Prop A  a  conjunction-Prop P (Q a)))
      ( λ x q  intro-∃ x (p , q))
      ( e)
  pr2 iff-distributive-conjunction-exists-Prop =
    elim-exists-Prop
      ( λ x  conjunction-Prop P (Q x))
      ( conjunction-Prop P (exists-Prop A Q))
      ( λ x (p , q)  (p , intro-∃ x q))

  distributive-conjunction-exists-Prop :
    conjunction-Prop P (exists-Prop A Q) 
    exists-Prop A  a  conjunction-Prop P (Q a))
  distributive-conjunction-exists-Prop =
    eq-iff'
      ( conjunction-Prop P (exists-Prop A Q))
      ( exists-Prop A  a  conjunction-Prop P (Q a)))
      ( iff-distributive-conjunction-exists-Prop)

Recent changes