Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Eléonore Mangel.

Created on 2022-02-08.
Last modified on 2024-04-11.

module foundation.conjunction where
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.universal-property-cartesian-product-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.decidable-propositions
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.propositions


The conjunction P ∧ Q of two propositions P and Q is the proposition that both P and Q hold and is thus defined by the cartesian product of their underlying types

  P ∧ Q := P × Q

The conjunction of two propositions satisfies the universal property of the meet in the locale of propositions. This means that any span of propositions over P and Q factor (uniquely) through the conjunction

        /  ∶  \
      /    ∶    \
    ∨      ∨      ∨
  P <--- P ∧ Q ---> Q.

In other words, we have a logical equivalence

  (R → P) ∧ (R → Q) ↔ (R → P ∧ Q)

for every proposition R. In fact, R can be any type.

The recursion principle of the conjunction of propositions states that to define a function P ∧ Q → R into a proposition R, or indeed any type, is equivalent to defining a function P → Q → R.


The conjunction

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

  conjunction-Prop : Prop (l1  l2)
  conjunction-Prop = product-Prop P Q

  type-conjunction-Prop : UU (l1  l2)
  type-conjunction-Prop = type-Prop conjunction-Prop

  is-prop-conjunction-Prop :
    is-prop type-conjunction-Prop
  is-prop-conjunction-Prop = is-prop-type-Prop conjunction-Prop

  infixr 15 _∧_
  _∧_ : Prop (l1  l2)
  _∧_ = conjunction-Prop

Note: The symbol used for the conjunction _∧_ is the logical and (agda-input: \wedge or \and).

The conjunction of decidable propositions

module _
  {l1 l2 : Level} (P : Decidable-Prop l1) (Q : Decidable-Prop l2)

  is-decidable-conjunction-Decidable-Prop :
      ( type-conjunction-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q))
  is-decidable-conjunction-Decidable-Prop =
      ( is-decidable-Decidable-Prop P)
      ( is-decidable-Decidable-Prop Q)

  conjunction-Decidable-Prop : Decidable-Prop (l1  l2)
  conjunction-Decidable-Prop =
    ( type-conjunction-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q) ,
      is-prop-conjunction-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q) ,

The introduction rule and projections for the conjunction of propositions

While we define the introduction rule and projections for the conjunction below, we advice users to use the standard pairing and projection functions for the cartesian product types: pair, pr1 and pr2.

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

  intro-conjunction-Prop : type-Prop P  type-Prop Q  type-conjunction-Prop P Q
  intro-conjunction-Prop = pair

  pr1-conjunction-Prop : type-conjunction-Prop P Q  type-Prop P
  pr1-conjunction-Prop = pr1

  pr2-conjunction-Prop : type-conjunction-Prop P Q  type-Prop Q
  pr2-conjunction-Prop = pr2

The elimination principle of the conjunction

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

  ev-conjunction-Prop :
    {l : Level} (R : Prop l)  type-Prop (((P  Q)  R)  P  Q  R)
  ev-conjunction-Prop R = ev-pair

  elimination-principle-conjunction-Prop : UUω
  elimination-principle-conjunction-Prop =
    {l : Level} (R : Prop l)  has-converse (ev-conjunction-Prop R)


The conjunction satisfies the recursion principle of the conjunction

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

  elim-conjunction-Prop : elimination-principle-conjunction-Prop P Q
  elim-conjunction-Prop R f (p , q) = f p q

The conjunction is the meet in the locale of propositions

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

  map-distributive-conjunction-Prop :
    type-conjunction-Prop (function-Prop C P) (function-Prop C Q) 
    C  type-conjunction-Prop P Q
  map-distributive-conjunction-Prop (f , g) y = (f y , g y)

  map-inv-distributive-conjunction-Prop :
    (C  type-conjunction-Prop P Q) 
    type-conjunction-Prop (function-Prop C P) (function-Prop C Q)
  map-inv-distributive-conjunction-Prop f = (pr1  f , pr2  f)

  is-equiv-map-distributive-conjunction-Prop :
    is-equiv map-distributive-conjunction-Prop
  is-equiv-map-distributive-conjunction-Prop =
      ( conjunction-Prop (function-Prop C P) (function-Prop C Q))
      ( function-Prop C (conjunction-Prop P Q))
      ( map-inv-distributive-conjunction-Prop)

  distributive-conjunction-Prop :
    type-conjunction-Prop (function-Prop C P) (function-Prop C Q) 
    (C  type-conjunction-Prop P Q)
  distributive-conjunction-Prop =
    ( map-distributive-conjunction-Prop ,

module _
  {l1 l2 l3 : Level} (P : Prop l1) (Q : Prop l2) (R : Prop l3)

  is-greatest-binary-lower-bound-conjunction-Prop :
    type-Prop (((R  P)  (R  Q))  (R  P  Q))
  is-greatest-binary-lower-bound-conjunction-Prop =
    ( map-distributive-conjunction-Prop P Q (type-Prop R) ,
      map-inv-distributive-conjunction-Prop P Q (type-Prop R))

See also

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