# Isolated points

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

Created on 2022-01-27.

module foundation.isolated-points where

Imports
open import foundation.action-on-identifications-functions
open import foundation.constant-maps
open import foundation.decidable-embeddings
open import foundation.decidable-equality
open import foundation.decidable-maps
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.maybe
open import foundation.negation
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.decidable-propositions
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.injective-maps
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.subtypes
open import foundation-core.transport-along-identifications


## Idea

A point a : A is considered to be isolated if Id a x is decidable for any x.

## Definitions

### Isolated points

is-isolated :
{l1 : Level} {X : UU l1} (a : X) → UU l1
is-isolated {l1} {X} a = (x : X) → is-decidable (a ＝ x)

isolated-point :
{l1 : Level} (X : UU l1) → UU l1
isolated-point X = Σ X is-isolated

module _
{l : Level} {X : UU l} (x : isolated-point X)
where

point-isolated-point : X
point-isolated-point = pr1 x

is-isolated-isolated-point : is-isolated point-isolated-point
is-isolated-isolated-point = pr2 x


### Complements of isolated points

complement-isolated-point :
{l1 : Level} (X : UU l1) → isolated-point X → UU l1
complement-isolated-point X x =
Σ X (λ y → ¬ (point-isolated-point x ＝ y))


## Properties

### A point is decidable if and only if the constant map pointing at it is decidable

module _
{l1 : Level} {A : UU l1} (a : A)
where

is-decidable-map-const-is-isolated :
is-isolated a → is-decidable-map (const unit A a)
is-decidable-map-const-is-isolated d x =
is-decidable-equiv (fiber-const a x) (d x)

is-isolated-is-decidable-map-const :
is-decidable-map (const unit A a) → is-isolated a
is-isolated-is-decidable-map-const d x =
is-decidable-equiv' (fiber-const a x) (d x)

cases-Eq-isolated-point :
is-isolated a → (x : A) → is-decidable (a ＝ x) → UU lzero
cases-Eq-isolated-point H x (inl p) = unit
cases-Eq-isolated-point H x (inr f) = empty

abstract
is-prop-cases-Eq-isolated-point :
(d : is-isolated a) (x : A) (dx : is-decidable (a ＝ x)) →
is-prop (cases-Eq-isolated-point d x dx)
is-prop-cases-Eq-isolated-point d x (inl p) = is-prop-unit
is-prop-cases-Eq-isolated-point d x (inr f) = is-prop-empty

Eq-isolated-point : is-isolated a → A → UU lzero
Eq-isolated-point d x = cases-Eq-isolated-point d x (d x)

abstract
is-prop-Eq-isolated-point :
(d : is-isolated a) (x : A) → is-prop (Eq-isolated-point d x)
is-prop-Eq-isolated-point d x =
is-prop-cases-Eq-isolated-point d x (d x)

Eq-isolated-point-Prop : is-isolated a → A → Prop lzero
pr1 (Eq-isolated-point-Prop d x) = Eq-isolated-point d x
pr2 (Eq-isolated-point-Prop d x) = is-prop-Eq-isolated-point d x

decide-reflexivity :
(d : is-decidable (a ＝ a)) → Σ (a ＝ a) (λ p → inl p ＝ d)
pr1 (decide-reflexivity (inl p)) = p
pr2 (decide-reflexivity (inl p)) = refl
decide-reflexivity (inr f) = ex-falso (f refl)

abstract
refl-Eq-isolated-point : (d : is-isolated a) → Eq-isolated-point d a
refl-Eq-isolated-point d =
tr
( cases-Eq-isolated-point d a)
( pr2 (decide-reflexivity (d a)))
( star)

abstract
Eq-eq-isolated-point :
(d : is-isolated a) {x : A} → a ＝ x → Eq-isolated-point d x
Eq-eq-isolated-point d refl = refl-Eq-isolated-point d

abstract
center-total-Eq-isolated-point :
(d : is-isolated a) → Σ A (Eq-isolated-point d)
pr1 (center-total-Eq-isolated-point d) = a
pr2 (center-total-Eq-isolated-point d) = refl-Eq-isolated-point d

cases-contraction-total-Eq-isolated-point :
(d : is-isolated a) (x : A) (dx : is-decidable (a ＝ x))
(e : cases-Eq-isolated-point d x dx) → a ＝ x
cases-contraction-total-Eq-isolated-point d x (inl p) e = p

contraction-total-Eq-isolated-point :
(d : is-isolated a) (t : Σ A (Eq-isolated-point d)) →
center-total-Eq-isolated-point d ＝ t
contraction-total-Eq-isolated-point d (x , e) =
eq-type-subtype
( Eq-isolated-point-Prop d)
( cases-contraction-total-Eq-isolated-point d x (d x) e)

is-contr-total-Eq-isolated-point :
(d : is-isolated a) → is-contr (Σ A (Eq-isolated-point d))
pr1 (is-contr-total-Eq-isolated-point d) = center-total-Eq-isolated-point d
pr2 (is-contr-total-Eq-isolated-point d) =
contraction-total-Eq-isolated-point d

abstract
is-equiv-Eq-eq-isolated-point :
(d : is-isolated a) (x : A) → is-equiv (Eq-eq-isolated-point d {x})
is-equiv-Eq-eq-isolated-point d =
fundamental-theorem-id
( is-contr-total-Eq-isolated-point d)
( λ x → Eq-eq-isolated-point d {x})

abstract
equiv-Eq-eq-isolated-point :
(d : is-isolated a) (x : A) → (a ＝ x) ≃ Eq-isolated-point d x
pr1 (equiv-Eq-eq-isolated-point d x) = Eq-eq-isolated-point d
pr2 (equiv-Eq-eq-isolated-point d x) = is-equiv-Eq-eq-isolated-point d x

abstract
is-prop-eq-isolated-point : (d : is-isolated a) (x : A) → is-prop (a ＝ x)
is-prop-eq-isolated-point d x =
is-prop-equiv
( equiv-Eq-eq-isolated-point d x)
( is-prop-Eq-isolated-point d x)

is-contr-loop-space-isolated-point :
(d : is-isolated a) → is-contr (a ＝ a)
is-contr-loop-space-isolated-point d =
is-proof-irrelevant-is-prop (is-prop-eq-isolated-point d a) refl

abstract
is-emb-const-is-isolated : is-isolated a → is-emb (const unit A a)
is-emb-const-is-isolated d star =
fundamental-theorem-id
( is-contr-equiv
( a ＝ a)
( left-unit-law-prod)
( is-proof-irrelevant-is-prop
( is-prop-eq-isolated-point d a)
( refl)))
( λ x → ap (λ y → a))


### Being an isolated point is a property

is-prop-is-isolated :
{l1 : Level} {A : UU l1} (a : A) → is-prop (is-isolated a)
is-prop-is-isolated a =
is-prop-is-inhabited
( λ H →
is-prop-Π (λ x → is-prop-is-decidable (is-prop-eq-isolated-point a H x)))

is-isolated-Prop :
{l1 : Level} {A : UU l1} (a : A) → Prop l1
pr1 (is-isolated-Prop a) = is-isolated a
pr2 (is-isolated-Prop a) = is-prop-is-isolated a

inclusion-isolated-point :
{l1 : Level} (A : UU l1) → isolated-point A → A
inclusion-isolated-point A = pr1

is-emb-inclusion-isolated-point :
{l1 : Level} (A : UU l1) → is-emb (inclusion-isolated-point A)
is-emb-inclusion-isolated-point A = is-emb-inclusion-subtype is-isolated-Prop

has-decidable-equality-isolated-point :
{l1 : Level} (A : UU l1) → has-decidable-equality (isolated-point A)
has-decidable-equality-isolated-point A (x , dx) (y , dy) =
is-decidable-equiv
( equiv-ap-inclusion-subtype is-isolated-Prop)
( dx y)

is-set-isolated-point :
{l1 : Level} (A : UU l1) → is-set (isolated-point A)
is-set-isolated-point A =
is-set-has-decidable-equality (has-decidable-equality-isolated-point A)

decidable-emb-isolated-point :
{l1 : Level} {A : UU l1} (a : isolated-point A) → unit ↪ᵈ A
pr1 (decidable-emb-isolated-point {l1} {A} a) =
const unit A (pr1 a)
pr1 (pr2 (decidable-emb-isolated-point {l1} {A} a)) =
is-emb-comp
( inclusion-isolated-point A)
( const unit (isolated-point A) a)
( is-emb-inclusion-isolated-point A)
( is-emb-is-injective
( is-set-isolated-point A)
( λ { {star} {star} p → refl}))
pr2 (pr2 (decidable-emb-isolated-point {l1} {A} a)) x =
is-decidable-prod is-decidable-unit (pr2 a x)


### Types with isolated points can be equipped with a Maybe-structure

map-maybe-structure-isolated-point :
{l1 : Level} (X : UU l1) (x : isolated-point X) →
Maybe (complement-isolated-point X x) → X
map-maybe-structure-isolated-point X (x , d) (inl (y , f)) = y
map-maybe-structure-isolated-point X (x , d) (inr star) = x

cases-map-inv-maybe-structure-isolated-point :
{l1 : Level} (X : UU l1) (x : isolated-point X) →
(y : X) → is-decidable (pr1 x ＝ y) → Maybe (complement-isolated-point X x)
cases-map-inv-maybe-structure-isolated-point X (x , dx) y (inl p) =
inr star
cases-map-inv-maybe-structure-isolated-point X (x , dx) y (inr f) =
inl (y , f)

map-inv-maybe-structure-isolated-point :
{l1 : Level} (X : UU l1) (x : isolated-point X) →
X → Maybe (complement-isolated-point X x)
map-inv-maybe-structure-isolated-point X (x , d) y =
cases-map-inv-maybe-structure-isolated-point X (x , d) y (d y)

cases-is-section-map-inv-maybe-structure-isolated-point :
{l1 : Level} (X : UU l1) (x : isolated-point X) →
(y : X) (d : is-decidable (pr1 x ＝ y)) →
( map-maybe-structure-isolated-point X x
( cases-map-inv-maybe-structure-isolated-point X x y d)) ＝
( y)
cases-is-section-map-inv-maybe-structure-isolated-point X
(x , dx) .x (inl refl) =
refl
cases-is-section-map-inv-maybe-structure-isolated-point X (x , dx) y (inr f) =
refl

is-section-map-inv-maybe-structure-isolated-point :
{l1 : Level} (X : UU l1) (x : isolated-point X) →
( map-maybe-structure-isolated-point X x ∘
map-inv-maybe-structure-isolated-point X x) ~ id
is-section-map-inv-maybe-structure-isolated-point X (x , d) y =
cases-is-section-map-inv-maybe-structure-isolated-point X (x , d) y (d y)

is-retraction-map-inv-maybe-structure-isolated-point :
{l1 : Level} (X : UU l1) (x : isolated-point X) →
( map-inv-maybe-structure-isolated-point X x ∘
map-maybe-structure-isolated-point X x) ~ id
is-retraction-map-inv-maybe-structure-isolated-point X (x , dx) (inl (y , f)) =
ap
( cases-map-inv-maybe-structure-isolated-point X (x , dx) y)
( eq-is-prop (is-prop-is-decidable (is-prop-eq-isolated-point x dx y)))
is-retraction-map-inv-maybe-structure-isolated-point X (x , dx) (inr star) =
ap
( cases-map-inv-maybe-structure-isolated-point X (x , dx) x)
{ x = dx (map-maybe-structure-isolated-point X (x , dx) (inr star))}
{ y = inl refl}
( eq-is-prop (is-prop-is-decidable (is-prop-eq-isolated-point x dx x)))

is-equiv-map-maybe-structure-isolated-point :
{l1 : Level} (X : UU l1) (x : isolated-point X) →
is-equiv (map-maybe-structure-isolated-point X x)
is-equiv-map-maybe-structure-isolated-point X x =
is-equiv-is-invertible
( map-inv-maybe-structure-isolated-point X x)
( is-section-map-inv-maybe-structure-isolated-point X x)
( is-retraction-map-inv-maybe-structure-isolated-point X x)

equiv-maybe-structure-isolated-point :
{l1 : Level} (X : UU l1) (x : isolated-point X) →
Maybe (complement-isolated-point X x) ≃ X
pr1 (equiv-maybe-structure-isolated-point X x) =
map-maybe-structure-isolated-point X x
pr2 (equiv-maybe-structure-isolated-point X x) =
is-equiv-map-maybe-structure-isolated-point X x

maybe-structure-isolated-point :
{l1 : Level} {X : UU l1} → isolated-point X → maybe-structure X
pr1 (maybe-structure-isolated-point {l1} {X} x) =
complement-isolated-point X x
pr2 (maybe-structure-isolated-point {l1} {X} x) =
equiv-maybe-structure-isolated-point X x

equiv-complement-isolated-point :
{l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) (x : isolated-point X)
(y : isolated-point Y) (p : map-equiv e (pr1 x) ＝ pr1 y) →
complement-isolated-point X x ≃ complement-isolated-point Y y
equiv-complement-isolated-point e x y p =
equiv-Σ
( λ z → ¬ (pr1 y ＝ z))
( e)
( λ z →
equiv-neg
( equiv-concat (inv p) (map-equiv e z) ∘e (equiv-ap e (pr1 x) z)))

inclusion-complement-isolated-point :
{l1 : Level} {X : UU l1} (x : isolated-point X) →
complement-isolated-point X x → X
inclusion-complement-isolated-point x = pr1

natural-inclusion-equiv-complement-isolated-point :
{l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ≃ Y) (x : isolated-point X)
(y : isolated-point Y) (p : map-equiv e (pr1 x) ＝ pr1 y) →
( inclusion-complement-isolated-point y ∘
map-equiv (equiv-complement-isolated-point e x y p)) ~
( map-equiv e ∘ inclusion-complement-isolated-point x)
natural-inclusion-equiv-complement-isolated-point e x y p (x' , f) = refl