Double negation stable propositions

Content created by Fredrik Bakke.

Created on 2024-10-15.
Last modified on 2024-10-15.

module foundation.double-negation-stable-propositions where
Imports 
open import foundation.double-negation
open import foundation.empty-types
open import foundation.negation
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.propositions

Idea

A proposition P is double negation stable if the implication

  ¬¬P ⇒ P

is true. In other words, if double negation elimination is valid for P.

Definitions

The predicate on a proposition of being double negation stable

module _
  {l : Level} (P : Prop l)
  where

  is-double-negation-stable-Prop : Prop l
  is-double-negation-stable-Prop = ¬¬' P ⇒ P

  is-double-negation-stable : UU l
  is-double-negation-stable = type-Prop is-double-negation-stable-Prop

  is-prop-is-double-negation-stable : is-prop is-double-negation-stable
  is-prop-is-double-negation-stable =
    is-prop-type-Prop is-double-negation-stable-Prop

Properties

The empty proposition is double negation stable

is-double-negation-stable-empty : is-double-negation-stable empty-Prop
is-double-negation-stable-empty e = e id

The unit proposition is double negation stable

is-double-negation-stable-unit : is-double-negation-stable unit-Prop
is-double-negation-stable-unit _ = star

The negation of a type is double negation stable

is-double-negation-stable-neg :
  {l : Level} (A : UU l) → is-double-negation-stable (neg-type-Prop A)
is-double-negation-stable-neg = double-negation-elim-neg

See also

Recent changes