Universal quantification

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.
Last modified on 2024-04-11.

module foundation.universal-quantification where
open import foundation.dependent-pair-types
open import foundation.evaluation-functions
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.propositions


Given a type A and a subtype P : A → Prop, the universal quantification

  ∀ (x : A), (P x)

is the proposition that there exists a proof of P x for every x in A.

The universal property of universal quantification states that it is the greatest lower 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

  (∀ (a : A), (R → P a)) ↔ (R → ∀ (a : A), (P a))

Notation. Because of syntactic limitations of the Agda language, we cannot use for the universal quantification in formalizations, and instead use ∀'.


Universal quantification

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

  for-all-Prop : Prop (l1  l2)
  for-all-Prop = Π-Prop A P

  type-for-all-Prop : UU (l1  l2)
  type-for-all-Prop = type-Prop for-all-Prop

  is-prop-for-all-Prop : is-prop type-for-all-Prop
  is-prop-for-all-Prop = is-prop-type-Prop for-all-Prop

  for-all : UU (l1  l2)
  for-all = type-for-all-Prop

  ∀' : Prop (l1  l2)
  ∀' = for-all-Prop

The universal property of universal quantification

The universal property of the universal quantification ∀ (a : A), (P a) states that for every proposition R, the canonical map

  (∀ (a : A), (R → P a)) → (R → ∀ (a : A), (P a))

is a logical equivalence. Indeed, this holds for any type R.

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

  universal-property-for-all : {l3 : Level} (S : Prop l3)  UUω
  universal-property-for-all S =
    {l : Level} (R : Prop l) 
    type-Prop ((∀' A  a  R  P a))  (R  S))

  ev-for-all :
    {l : Level} {B : UU l} 
    for-all A  a  function-Prop B (P a))  B  for-all A P
  ev-for-all f r a = f a r


Universal quantification satisfies its universal property

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

  map-up-for-all :
    {l : Level} {B : UU l} 
    (B  for-all A P)  for-all A  a  function-Prop B (P a))
  map-up-for-all f a r = f r a

  is-equiv-ev-for-all :
    {l : Level} {B : UU l}  is-equiv (ev-for-all A P {B = B})
  is-equiv-ev-for-all {B = B} =
      ( ∀' A  a  function-Prop B (P a)))
      ( function-Prop B (∀' A P))
      ( map-up-for-all)

  up-for-all : universal-property-for-all A P (∀' A P)
  up-for-all R = (ev-for-all A P , map-up-for-all)

See also

  • Universal quantification is the indexed counterpart to conjunction.

Table of files about propositional logic

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

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
Exclusive disjunctionfoundation.exclusive-disjunction
Existential quantificationfoundation.existential-quantification
Uniqueness quantificationfoundation.uniqueness-quantification
Universal quantificationfoundation.universal-quantification
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

Recent changes