Dependent products of propositions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2026-05-02.
Last modified on 2026-05-02.

module foundation.dependent-products-propositions where

open import foundation.dependent-pair-types
open import foundation.dependent-products-contractible-types
open import foundation.universe-levels

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

Idea

Given a family of propositions B : A → 𝒰, then the dependent product Π A B is again a proposition.

Definitions

Products of families of propositions are propositions

abstract
  is-prop-Π :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    ((x : A) → is-prop (B x)) → is-prop ((x : A) → B x)
  is-prop-Π H =
    is-prop-is-proof-irrelevant
      ( λ f → is-contr-Π (λ x → is-proof-irrelevant-is-prop (H x) (f x)))

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

  type-Π-Prop : UU (l1 ⊔ l2)
  type-Π-Prop = (x : A) → type-Prop (P x)

  is-prop-Π-Prop : is-prop type-Π-Prop
  is-prop-Π-Prop = is-prop-Π (λ x → is-prop-type-Prop (P x))

  Π-Prop : Prop (l1 ⊔ l2)
  pr1 Π-Prop = type-Π-Prop
  pr2 Π-Prop = is-prop-Π-Prop

We now repeat the above for implicit Π-types.

abstract
  is-prop-implicit-Π :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    ((x : A) → is-prop (B x)) → is-prop ({x : A} → B x)
  is-prop-implicit-Π H =
    is-prop-equiv
      ( ( λ f x → f {x}) ,
        ( is-equiv-is-invertible (λ g {x} → g x) (refl-htpy) (refl-htpy)))
      ( is-prop-Π H)

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

  type-implicit-Π-Prop : UU (l1 ⊔ l2)
  type-implicit-Π-Prop = {x : A} → type-Prop (P x)

  is-prop-implicit-Π-Prop : is-prop type-implicit-Π-Prop
  is-prop-implicit-Π-Prop =
    is-prop-implicit-Π (λ x → is-prop-type-Prop (P x))

  implicit-Π-Prop : Prop (l1 ⊔ l2)
  pr1 implicit-Π-Prop = type-implicit-Π-Prop
  pr2 implicit-Π-Prop = is-prop-implicit-Π-Prop

The type of functions into a proposition is a proposition

abstract
  is-prop-function-type :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    is-prop B → is-prop (A → B)
  is-prop-function-type H = is-prop-Π (λ _ → H)

type-function-Prop :
  {l1 l2 : Level} → UU l1 → Prop l2 → UU (l1 ⊔ l2)
type-function-Prop A P = A → type-Prop P

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

function-Prop :
  {l1 l2 : Level} → UU l1 → Prop l2 → Prop (l1 ⊔ l2)
pr1 (function-Prop A P) = type-function-Prop A P
pr2 (function-Prop A P) = is-prop-function-Prop P

type-hom-Prop :
  {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) → UU (l1 ⊔ l2)
type-hom-Prop P = type-function-Prop (type-Prop P)

is-prop-hom-Prop :
  {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) →
  is-prop (type-hom-Prop P Q)
is-prop-hom-Prop P = is-prop-function-Prop

hom-Prop :
  {l1 l2 : Level} → Prop l1 → Prop l2 → Prop (l1 ⊔ l2)
pr1 (hom-Prop P Q) = type-hom-Prop P Q
pr2 (hom-Prop P Q) = is-prop-hom-Prop P Q

infixr  _⇒_
_⇒_ = hom-Prop

See also

Operations on propositions

There is a wide range of operations on propositions due to the rich structure of intuitionistic logic. Below we give a structured overview of a notable selection of such operations and their notation in the library.

The list is split into two sections, the first consists of operations that generalize to arbitrary types and even sufficiently nice subuniverses, such as $n$-types.

Note that for many operations in the second section, there is an equivalent operation on propositions in the first.

We can also organize these operations by indexed and binary variants, giving us the following table:

Table of files about propositional logic

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

Recent changes

• 2026-05-02. Fredrik Bakke and Egbert Rijke. Remove dependency between BUILTIN and postulates (#1373).