Topology!

Topology.agda

module Topology where

import Level
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat hiding (_⊔_)
open import Data.Fin
open import Data.Product
open import Relation.Nullary
open import Relation.Unary hiding (Pred)
open Level using (Lift; lower)


Pred : ∀ {l} → Set l → Set (Level.suc l)
Pred {l} A = A → Set l

Union : ∀ {A : Set} {I : Set} → (I → Pred A) → Pred A
Union F = λ a → ∃ (λ i → a ∈ F i)

Intersection : ∀ {A : Set} {I : Set} → (I → Pred A) → Pred A
Intersection F = λ a → ∀ i → a ∈ F i

Complement : ∀ {A : Set} → Pred A → Pred A
Complement A = λ a → a ∉ A

Disjoint : ∀ {A : Set} → Pred A → Pred A → Set
Disjoint A B = ∀ a → a ∈ A → a ∉ B

record Space : Set₂  where
  constructor space
  field
    C            : Set
    Open         : Pred (Pred C)
    none         : Open (λ _ → Lift ⊥)
    all          : Open (λ _ → Lift ⊤)
    union        : {A : Set} (f : A → ∃ Open) → Union (proj₁ ∘ f) ∈ Open
    intersection : ∀ {n} (f : Fin n → ∃ Open) → Intersection (proj₁ ∘ f) ∈ Open

  Neighborhood : C → Pred (Pred C)
  Neighborhood x = λ V → ∃ (λ U → Open U × U ⊆ V × x ∈ U)

  -- This definition was previously incorrect.
  Closed : Pred (Pred C)
  Closed P = ∀ x → x ∉ P → ∃ (λ U → Neighborhood x U → Disjoint P U)

  Clopen : Pred (Pred C)
  Clopen P = Open P × Closed P


  -- Random proofs
  none-Clopen : Clopen (λ _ → (Lift ⊥))
  none-Clopen = none , (λ x x∉P → (λ _ → Lift ⊤) , (λ N a a∈Empty a∈All → lower a∈Empty))

  all-Clopen : Clopen (λ _ → Lift ⊤)
  all-Clopen = all , (λ x x∉P → (λ _ → Lift ⊥) , (λ N a a∈All a∈Empty → lower a∈Empty))

  Complement-closes : ∀ {U : Pred C} → Open U → Closed (Complement U)
  Complement-closes {U} U-open = λ x x∉U → U , (λ N a a∈CU a∈U → a∈CU a∈U)

open Space

-- Definition of a continuous function.
preimage : ∀ {A B : Set} → (f : A → B) → Pred B → Pred A
preimage f B = λ a → B (f a)

Continuous : ∀ {{X Y : Space}} → (f : (C X) → (C Y)) → Set₁
Continuous {{X}} {{Y}} f = ∀ B → (Open Y) B → (Open X) (preimage f B)

-- The discrete topology which can be defined on any set.
Discrete : ∀ (A : Set) → Space
Discrete A = space A (λ _ → Lift ⊤) _ _ _ _

-- Everything is both closed and open on this topology.
Discrete-Clopen : ∀ {A : Set} → ∀ S → Clopen (Discrete A) S
Discrete-Clopen S = _ , (λ x x∉S → Complement S , (λ N a a∈S a∈CS → a∈CS a∈S))

-- Identity on any space is continuous.
-- Note that we get 'preimage id B ≡ B' for free.
id-Cont : ∀ {{X : Space}} → Continuous id
id-Cont B B-open = B-open