# Conjunction

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

Created on 2022-02-08.

module foundation.conjunction where

Imports
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


## Idea

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

           R
/  ∶  \
/    ∶    \
∨      ∨      ∨
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.

## Definitions

### The conjunction

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

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

is-decidable-conjunction-Decidable-Prop :
is-decidable
( type-conjunction-Prop (prop-Decidable-Prop P) (prop-Decidable-Prop Q))
is-decidable-conjunction-Decidable-Prop =
is-decidable-product
( 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) ,
is-decidable-conjunction-Decidable-Prop)


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

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

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)


## Properties

### The conjunction satisfies the recursion principle of the conjunction

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

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

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 =
is-equiv-has-converse
( 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 ,
is-equiv-map-distributive-conjunction-Prop)

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

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


## 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