Impredicative encodings of the logical operations

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

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

module foundation.impredicative-encodings where
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.empty-types
open import foundation.existential-quantification
open import foundation.homotopies
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.universal-quantification
open import foundation.universe-levels

open import foundation-core.coproduct-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.sets


By universally quantifying over all propositions in a universe, we can define all the logical operations. The idea is to use the fact that any proposition P is equivalent to the proposition (Q : Prop l) → (P ⇒ Q) ⇒ Q, which can be thought of as the least proposition Q containing P.

The impredicative encoding of the propositional truncation

module _
  {l : Level} (A : UU l)

  impredicative-trunc-Prop : Prop (lsuc l)
  impredicative-trunc-Prop =
    ∀' (Prop l)  Q  function-Prop (A  type-Prop Q) Q)

  type-impredicative-trunc-Prop : UU (lsuc l)
  type-impredicative-trunc-Prop =
    type-Prop impredicative-trunc-Prop

  map-impredicative-trunc-Prop :
    type-trunc-Prop A  type-impredicative-trunc-Prop
  map-impredicative-trunc-Prop =
      ( impredicative-trunc-Prop)
      ( λ x Q f  f x)

  map-inv-impredicative-trunc-Prop :
    type-impredicative-trunc-Prop  type-trunc-Prop A
  map-inv-impredicative-trunc-Prop H =
    H (trunc-Prop A) unit-trunc-Prop

  equiv-impredicative-trunc-Prop :
    type-trunc-Prop A  type-impredicative-trunc-Prop
  equiv-impredicative-trunc-Prop =
      ( trunc-Prop A)
      ( impredicative-trunc-Prop)
      ( map-impredicative-trunc-Prop)
      ( map-inv-impredicative-trunc-Prop)

The impredicative encoding of conjunction

module _
  {l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2)

  impredicative-conjunction-Prop : Prop (lsuc (l1  l2))
  impredicative-conjunction-Prop =
    ∀' (Prop (l1  l2))  Q  (P1  P2  Q)  Q)

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

  map-product-impredicative-conjunction-Prop :
    type-conjunction-Prop P1 P2  type-impredicative-conjunction-Prop
  map-product-impredicative-conjunction-Prop (p1 , p2) Q f = f p1 p2

  map-inv-product-impredicative-conjunction-Prop :
    type-impredicative-conjunction-Prop  type-conjunction-Prop P1 P2
  map-inv-product-impredicative-conjunction-Prop H = H (P1  P2) pair

  equiv-product-impredicative-conjunction-Prop :
    type-conjunction-Prop P1 P2  type-impredicative-conjunction-Prop
  equiv-product-impredicative-conjunction-Prop =
      ( P1  P2)
      ( impredicative-conjunction-Prop)
      ( map-product-impredicative-conjunction-Prop)
      ( map-inv-product-impredicative-conjunction-Prop)

The impredicative encoding of disjunction

module _
  {l1 l2 : Level} (P1 : Prop l1) (P2 : Prop l2)

  impredicative-disjunction-Prop : Prop (lsuc (l1  l2))
  impredicative-disjunction-Prop =
    ∀' (Prop (l1  l2))  Q  (P1  Q)  (P2  Q)  Q)

  type-impredicative-disjunction-Prop : UU (lsuc (l1  l2))
  type-impredicative-disjunction-Prop =
    type-Prop impredicative-disjunction-Prop

  map-impredicative-disjunction-Prop :
    type-disjunction-Prop P1 P2  type-impredicative-disjunction-Prop
  map-impredicative-disjunction-Prop =
      ( impredicative-disjunction-Prop)
      ( rec-coproduct  x Q f1 f2  f1 x)  y Q f1 f2  f2 y))

  map-inv-impredicative-disjunction-Prop :
    type-impredicative-disjunction-Prop  type-disjunction-Prop P1 P2
  map-inv-impredicative-disjunction-Prop H =
    H (P1  P2) (inl-disjunction) (inr-disjunction)

  equiv-impredicative-disjunction-Prop :
    type-disjunction-Prop P1 P2  type-impredicative-disjunction-Prop
  equiv-impredicative-disjunction-Prop =
      ( P1  P2)
      ( impredicative-disjunction-Prop)
      ( map-impredicative-disjunction-Prop)
      ( map-inv-impredicative-disjunction-Prop)

The impredicative encoding of the empty type

impredicative-empty-Prop : Prop (lsuc lzero)
impredicative-empty-Prop = ∀' (Prop lzero)  P  P)

type-impredicative-empty-Prop : UU (lsuc lzero)
type-impredicative-empty-Prop = type-Prop impredicative-empty-Prop

is-empty-impredicative-empty-Prop :
  is-empty type-impredicative-empty-Prop
is-empty-impredicative-empty-Prop e = e empty-Prop

equiv-impredicative-empty-Prop :
  empty  type-impredicative-empty-Prop
equiv-impredicative-empty-Prop =
  equiv-is-empty id is-empty-impredicative-empty-Prop

The impredicative encoding of negation

module _
  {l : Level} (A : UU l)

  impredicative-neg-Prop : Prop (lsuc l)
  impredicative-neg-Prop =
    Π-Prop (Prop l)  Q  function-Prop A Q)

  type-impredicative-neg-Prop : UU (lsuc l)
  type-impredicative-neg-Prop = type-Prop impredicative-neg-Prop

  map-impredicative-neg-Prop : ¬ A  type-impredicative-neg-Prop
  map-impredicative-neg-Prop f Q a = ex-falso (f a)

  map-inv-impredicative-neg-Prop : type-impredicative-neg-Prop  ¬ A
  map-inv-impredicative-neg-Prop H a = H (neg-type-Prop A) a a

  equiv-impredicative-neg-Prop : ¬ A  type-impredicative-neg-Prop
  equiv-impredicative-neg-Prop =
      ( neg-type-Prop A)
      ( impredicative-neg-Prop)
      ( map-impredicative-neg-Prop)
      ( map-inv-impredicative-neg-Prop)

The impredicative encoding of existential quantification

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

  impredicative-exists-Prop : Prop (lsuc (l1  l2))
  impredicative-exists-Prop =
    ∀' (Prop (l1  l2))  Q  (∀' A  x  P x  Q))  Q)

  type-impredicative-exists-Prop : UU (lsuc (l1  l2))
  type-impredicative-exists-Prop =
    type-Prop impredicative-exists-Prop

  map-impredicative-exists-Prop :
    exists A P  type-impredicative-exists-Prop
  map-impredicative-exists-Prop =
      ( impredicative-exists-Prop)
      ( ind-Σ  x y Q h  h x y))

  map-inv-impredicative-exists-Prop :
    type-impredicative-exists-Prop  exists A P
  map-inv-impredicative-exists-Prop H =
    H ( A P)  x y  unit-trunc-Prop (x , y))

  equiv-impredicative-exists-Prop :
    exists A P  type-impredicative-exists-Prop
  equiv-impredicative-exists-Prop =
      (  A P)
      ( impredicative-exists-Prop)
      ( map-impredicative-exists-Prop)
      ( map-inv-impredicative-exists-Prop)

The impredicative encoding of the based identity type of a set

module _
  {l : Level} (A : Set l) (a x : type-Set A)

  impredicative-based-id-Prop : Prop (lsuc l)
  impredicative-based-id-Prop = ∀' (type-Set A  Prop l)  Q  Q a  Q x)

  type-impredicative-based-id-Prop : UU (lsuc l)
  type-impredicative-based-id-Prop = type-Prop impredicative-based-id-Prop

  map-impredicative-based-id-Prop :
    a  x  type-impredicative-based-id-Prop
  map-impredicative-based-id-Prop refl Q p = p

  map-inv-impredicative-based-id-Prop :
    type-impredicative-based-id-Prop  a  x
  map-inv-impredicative-based-id-Prop H = H (Id-Prop A a) refl

  equiv-impredicative-based-id-Prop :
    (a  x)  type-impredicative-based-id-Prop
  equiv-impredicative-based-id-Prop =
      ( Id-Prop A a x)
      ( impredicative-based-id-Prop)
      ( map-impredicative-based-id-Prop)
      ( map-inv-impredicative-based-id-Prop)

The impredicative encoding of Martin-Löf's identity type of a set

module _
  {l : Level} (A : Set l) (x y : type-Set A)

  impredicative-id-Prop : Prop (lsuc l)
  impredicative-id-Prop =
      ( type-Set A  type-Set A  Prop l)
      ( λ Q  (∀' (type-Set A)  a  Q a a))  Q x y)

  type-impredicative-id-Prop : UU (lsuc l)
  type-impredicative-id-Prop = type-Prop impredicative-id-Prop

  map-impredicative-id-Prop :
    x  y  type-impredicative-id-Prop
  map-impredicative-id-Prop refl Q r = r x

  map-inv-impredicative-id-Prop :
    type-impredicative-id-Prop  x  y
  map-inv-impredicative-id-Prop H = H (Id-Prop A) (refl-htpy)

  equiv-impredicative-id-Prop :
    (x  y)  type-impredicative-id-Prop
  equiv-impredicative-id-Prop =
      ( Id-Prop A x y)
      ( impredicative-id-Prop)
      ( map-impredicative-id-Prop)
      ( map-inv-impredicative-id-Prop)

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