Maps with double negation dense equality

Content created by Fredrik Bakke.

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

module foundation.double-negation-dense-equality-maps where
Imports 
open import foundation.double-negation-dense-equality
open import foundation.irrefutable-equality
open import foundation.universe-levels

open import foundation-core.fibers-of-maps

Idea

A map f : A → B is said to have double negation dense equality if its fibers have double negation dense equality. I.e., if for every y : B and every pair p q : fiber f y it is irrefutable that p equals q. In other words, ¬¬ (p ＝ q) holds.

Definitions

has-double-negation-dense-equality-map :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2)
has-double-negation-dense-equality-map {B = B} f =
  (y : B) → has-double-negation-dense-equality (fiber f y)

Recent changes