Propositionally double negation eliminating maps

Content created by Fredrik Bakke.

Created on 2025-08-14.
Last modified on 2025-08-14.

module logic.propositionally-double-negation-eliminating-maps where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import foundation-core.fibers-of-maps
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies

open import logic.double-negation-eliminating-maps
open import logic.propositional-double-negation-elimination
open import logic.propositionally-decidable-maps

Idea

A map is said to be propositionally double negation eliminating if its fibers satisfy propositional double negation elimination. I.e., for every y : B, if fiber f y is irrefutable, then we have that the fiber is in fact inhabited. In other words, double negation eliminating maps come equipped with a map

  (y : B) → ¬¬ (fiber f y) → ║ fiber f y ║₋₁.

Definitions

Propositional double negation elimination on a map

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  is-prop-double-negation-eliminating-map : (A → B) → UU (l1 ⊔ l2)
  is-prop-double-negation-eliminating-map f =
    (y : B) → has-prop-double-negation-elim (fiber f y)

  is-property-is-prop-double-negation-eliminating-map :
    {f : A → B} → is-prop (is-prop-double-negation-eliminating-map f)
  is-property-is-prop-double-negation-eliminating-map {f} =
    is-prop-Π (λ y → is-prop-has-prop-double-negation-elim (fiber f y))

  is-prop-double-negation-eliminating-map-Prop : (A → B) → Prop (l1 ⊔ l2)
  is-prop-double-negation-eliminating-map-Prop f =
    is-prop-double-negation-eliminating-map f ,
    is-property-is-prop-double-negation-eliminating-map

The type of propositionally double negation eliminating maps

prop-double-negation-eliminating-map :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
prop-double-negation-eliminating-map A B =
  Σ (A → B) (is-prop-double-negation-eliminating-map)

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  (f : prop-double-negation-eliminating-map A B)
  where

  map-prop-double-negation-eliminating-map : A → B
  map-prop-double-negation-eliminating-map = pr1 f

  is-prop-double-negation-eliminating-prop-double-negation-eliminating-map :
    is-prop-double-negation-eliminating-map
      map-prop-double-negation-eliminating-map
  is-prop-double-negation-eliminating-prop-double-negation-eliminating-map =
    pr2 f

Properties

Propositionally double negation eliminating maps are closed under homotopy

abstract
  is-prop-double-negation-eliminating-map-htpy :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B} →
    f ~ g →
    is-prop-double-negation-eliminating-map g →
    is-prop-double-negation-eliminating-map f
  is-prop-double-negation-eliminating-map-htpy H K b =
    has-prop-double-negation-elim-equiv
      ( equiv-tot (λ a → equiv-concat (inv (H a)) b))
      ( K b)

Double negation eliminating maps are propositionally double negation eliminating

is-prop-double-negation-eliminating-map-is-double-negation-eliminating-map :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} →
  is-double-negation-eliminating-map f →
  is-prop-double-negation-eliminating-map f
is-prop-double-negation-eliminating-map-is-double-negation-eliminating-map H y =
  has-prop-double-negation-elim-has-double-negation-elim (H y)

Propositionally decidable maps are propositionally double negation eliminating

is-prop-double-negation-eliminating-map-is-inhabited-or-empty-map :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} →
  is-inhabited-or-empty-map f → is-prop-double-negation-eliminating-map f
is-prop-double-negation-eliminating-map-is-inhabited-or-empty-map H y =
  prop-double-negation-elim-is-inhabited-or-empty (H y)

Recent changes