Fredrik Bakke 26–28 March 2025 We formalize a series of properties of dense maps. - We construct the unique double negation image factorization - We show compact types are closed under dense covers - We give variants of Lawvere's and Cantor's fixed point theorems for dense maps \begin{code} {-# OPTIONS --safe --without-K #-} module TypeTopology.DenseMapsProperties where open import MLTT.Spartan open import MLTT.Plus-Properties open import NotionsOfDecidability.Complemented open import NotionsOfDecidability.Decidable open import TypeTopology.CompactTypes open import TypeTopology.Density open import UF.Base open import UF.DiscreteAndSeparated open import UF.Embeddings open import UF.Equiv open import UF.LeftCancellable open import UF.PropTrunc open import UF.Retracts open import UF.Subsingletons open import UF.Subsingletons-FunExt open import UF.SubtypeClassifier open import Various.LawvereFPT \end{code} Double negation image factorization. Every function can be factored essentially uniquely into a dense map followed by a double negation stable embedding through its "double negation image". We only appeal to a relaxation of the function extensionality axiom: that negations are propositions. \begin{code} is-¬¬-stable-map : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇ is-¬¬-stable-map {𝓤} {𝓥} {X} {Y} f = each-fiber-of f ¬¬-stable _∈¬¬-image_ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → Y → (X → Y) → 𝓤 ⊔ 𝓥 ̇ y ∈¬¬-image f = ¬¬ (fiber f y) being-in-the-¬¬-image-is-prop : negations-are-props-statement (𝓤 ⊔ 𝓥) → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (y : Y) (f : X → Y) → is-prop (y ∈¬¬-image f) being-in-the-¬¬-image-is-prop negations-are-props y f = negations-are-props ¬¬-image : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇ ¬¬-image f = Σ y ꞉ codomain f , y ∈¬¬-image f ¬¬-restriction : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → ¬¬-image f → Y ¬¬-restriction f (y , _) = y ¬¬-corestriction : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → X → ¬¬-image f ¬¬-corestriction f x = (f x , ¬¬-intro (x , refl)) ¬¬-image-factorization : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → f ∼ ¬¬-restriction f ∘ ¬¬-corestriction f ¬¬-image-factorization f x = refl ¬¬-corestrictions-are-dense : negations-are-props-statement (𝓤 ⊔ 𝓥) → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-dense (¬¬-corestriction f) ¬¬-corestrictions-are-dense negations-are-props f ((y , nnp) , nq) = nnp (λ (x , p) → nq (x , to-Σ-= (p , negations-are-props _ nnp))) ¬¬-restrictions-are-embeddings : negations-are-props-statement (𝓤 ⊔ 𝓥) → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-embedding (¬¬-restriction f) ¬¬-restrictions-are-embeddings negations-are-props f = pr₁-is-embedding (λ y → negations-are-props) ¬¬-restrictions-are-left-cancellable : negations-are-props-statement (𝓤 ⊔ 𝓥) → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → left-cancellable (¬¬-restriction f) ¬¬-restrictions-are-left-cancellable negations-are-props f = embeddings-are-lc (¬¬-restriction f) (¬¬-restrictions-are-embeddings negations-are-props f) ¬¬-restrictions-are-¬¬-stable : negations-are-props-statement (𝓤 ⊔ 𝓥) → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-¬¬-stable-map (¬¬-restriction f) ¬¬-restrictions-are-¬¬-stable negations-are-props f y nnip = ((y , a) , refl) where a : y ∈¬¬-image f a np = nnip b where b : ¬ (fiber (¬¬-restriction f) y) b (v , p) = ¬¬-corestrictions-are-dense negations-are-props f c where c : Σ v ꞉ ¬¬-image f , ¬ (fiber (¬¬-corestriction f) v) c = (v , d) where d : ¬ (fiber (¬¬-corestriction f) v) d (x , q) = np (x , (ap (¬¬-restriction f) q ∙ p)) \end{code} Double negation stability is a form of split support and lets us conclude from left cancellability that a map is an embedding. \begin{code} ¬¬-stable-left-cancellable-maps-are-embeddings : negations-are-props-statement (𝓤 ⊔ 𝓥) → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (f : X → Y) → left-cancellable f → is-¬¬-stable-map f → is-embedding f ¬¬-stable-left-cancellable-maps-are-embeddings negations-are-props f lc s = f-is-embedding where ¬¬-corestriction-f-is-split-surjective : (u : ¬¬-image f) → fiber (¬¬-corestriction f) u ¬¬-corestriction-f-is-split-surjective (y , nnp) = let (x , p) = s y nnp in ( x , ¬¬-restrictions-are-left-cancellable negations-are-props f p) ¬¬-corestriction-f-is-equiv : is-equiv (¬¬-corestriction f) ¬¬-corestriction-f-is-equiv = lc-split-surjections-are-equivs (¬¬-corestriction f) (factor-is-lc (¬¬-corestriction f) (¬¬-restriction f) lc) (¬¬-corestriction-f-is-split-surjective) ¬¬-corestriction-f-is-embedding : is-embedding (¬¬-corestriction f) ¬¬-corestriction-f-is-embedding = equivs-are-embeddings (¬¬-corestriction f) (¬¬-corestriction-f-is-equiv) f-is-embedding : is-embedding f f-is-embedding = ∘-is-embedding (¬¬-corestriction-f-is-embedding) (¬¬-restrictions-are-embeddings negations-are-props f) complemented-maps-are-¬¬-stable : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (f : X → Y) → is-complemented-map f → is-¬¬-stable-map f complemented-maps-are-¬¬-stable f d x = ¬¬-stable-if-decidable (fiber f x) (d x) complemented-left-cancellable-maps-are-embeddings : negations-are-props-statement (𝓤 ⊔ 𝓥) → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (f : X → Y) → left-cancellable f → is-complemented-map f → is-embedding f complemented-left-cancellable-maps-are-embeddings negations-are-props f lc d = ¬¬-stable-left-cancellable-maps-are-embeddings negations-are-props f lc (complemented-maps-are-¬¬-stable f d) \end{code} Compact types are closed under dense covers. We give a generalization of the fact that compact types are closed under covers that also avoids function extensionality and propositional truncations. \begin{code} dense-map-Compact : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-dense f → is-Compact X {𝓦} → is-Compact Y {𝓦} dense-map-Compact f i c A δ = +functor positive-case negative-case d where positive-case : Σ (A ∘ f) → Σ A positive-case (x , p) = (f x , p) negative-case : ¬ Σ (A ∘ f) → ¬ Σ A negative-case nf (y , p) = i (y , λ (x , r) → nf (x , transport A (r ⁻¹) p)) d : is-decidable (Σ (A ∘ f)) d = c (A ∘ f) (δ ∘ f) dense-map-Π-Compact : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-dense f → is-Π-Compact X {𝓦} → is-Π-Compact Y {𝓦} dense-map-Π-Compact {𝓤} {𝓥} {𝓦} {X} {Y} f i c A δ = claim where positive-case : Π (A ∘ f) → Π A positive-case g y = Cases (δ y) id negative-positive-case where negative-positive-case : ¬ A y → A y negative-positive-case np = 𝟘-elim (i (y , λ (x , r) → np (transport A r (g x)))) negative-case : ¬ Π (A ∘ f) → ¬ Π A negative-case nph p = nph (p ∘ f) claim : is-decidable (Π A) claim = +functor positive-case negative-case (c (A ∘ f) (δ ∘ f)) \end{code} As a corollary compact types are closed under covers. This proof improves on a previously established result in the library by avoiding function extensionality. \begin{code} module _ (pt : propositional-truncations-exist) where open propositional-truncations-exist pt open import UF.ImageAndSurjection pt surjections-are-dense : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-surjection f → is-dense f surjections-are-dense f s (y , q) = ∥∥-rec 𝟘-is-prop q (s y) surjection-Compact' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-surjection f → is-Compact X {𝓦} → is-Compact Y {𝓦} surjection-Compact' f i = dense-map-Compact f (surjections-are-dense f i) image-Compact' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-Compact X {𝓦} → is-Compact (image f) {𝓦} image-Compact' f = surjection-Compact' (corestriction f) (corestrictions-are-surjections f) surjection-Π-Compact : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-surjection f → is-Π-Compact X {𝓦} → is-Π-Compact Y {𝓦} surjection-Π-Compact f i = dense-map-Π-Compact f (surjections-are-dense f i) image-Π-Compact : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → is-Π-Compact X {𝓦} → is-Π-Compact (image f) {𝓦} image-Π-Compact f c = surjection-Π-Compact (corestriction f) (corestrictions-are-surjections f) c \end{code} Fixed point theorems for dense maps. We give an alternative formulation of Lawvere's fixed point theorem using double negations. This formulation also leads to a variant of Cantor's theorem. The strengthening again only assumes a relaxation of function extensionality: that negations are propositions. The formalization is a repeat of the proofs for the traditional theorems with double negations appropriately substituted in. \begin{code} ¬¬-fixed-point-property : 𝓤 ̇ → 𝓤 ̇ ¬¬-fixed-point-property X = (f : X → X) → ¬¬ (Σ x ꞉ X , x = f x) LFPT¬¬ : {A : 𝓤 ̇ } {X : 𝓥 ̇ } (φ : A → (A → X)) → is-dense φ → ¬¬-fixed-point-property X LFPT¬¬ {𝓤} {𝓥} {A} {X} φ s f = ¬¬-functor γ e where g : A → X g a = f (φ a a) e : ¬¬ (Σ a ꞉ A , φ a = g) e np = s (g , np) γ : (Σ a ꞉ A , φ a = g) → Σ x ꞉ X , x = f x γ (a , q) = x , p where x : X x = φ a a p : x = f x p = x =⟨ refl ⟩ φ a a =⟨ ap (λ - → - a) q ⟩ g a =⟨ refl ⟩ f x ∎ \end{code} We apply this version of Lawvere's fixed point theorem to also get a variant of Cantor's theorem for dense maps. \begin{code} not-no-fp' : (ne : negations-are-props-statement 𝓤) → ¬ (Σ P ꞉ Ω 𝓤 , P = not' ne P) not-no-fp' _ (P , p) = retract-version.¬-no-fp (P holds , ap _holds p) cantor-¬¬-theorem-for-universes : (A : 𝓥 ̇ ) → (φ : A → (A → 𝓤 ̇ )) → is-dense φ → (X : 𝓤 ̇ ) → ¬¬-fixed-point-property X cantor-¬¬-theorem-for-universes {𝓥} {𝓤} A φ s X f = ¬¬-functor g (LFPT¬¬ φ s (λ B → B → X)) where g : (Σ B ꞉ 𝓤 ̇ , B = (B → X)) → Σ x ꞉ X , x = f x g (B , p) = retract-version.LFPT-= {𝓤} {𝓤} p f Cantor-¬¬-theorem-for-universes : (A : 𝓥 ̇ ) → (φ : A → (A → 𝓤 ̇ )) → ¬ is-dense φ Cantor-¬¬-theorem-for-universes A r h = cantor-¬¬-theorem-for-universes A r h 𝟘 id (λ ()) cantor-¬¬-theorem : negations-are-props-statement 𝓤 → (A : 𝓥 ̇ ) → (φ : A → (A → Ω 𝓤)) → ¬ is-dense φ cantor-¬¬-theorem ne A φ s = LFPT¬¬ φ s (not' ne) (not-no-fp' ne) \end{code}