# Universal quantification

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.

module foundation.universal-quantification where

Imports
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


## Idea

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 ∀'.

## Definitions

### Universal quantification

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

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)
where

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


## Properties

### Universal quantification satisfies its universal property

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

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} =
is-equiv-has-converse
( ∀' 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)


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

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