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
open Level using (_⊔_; Lift; lower)

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

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

record Space x ℓ : Set (Level.suc x ⊔ Level.suc ℓ)  where
  constructor space
  field
    X : Set x
    Open         : Pred (Pred X ℓ) ℓ
    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 : X → Pred (Pred X ℓ) _
  Neighborhood x = λ V → ∃ (λ U → Open U × U ⊆ V × x ∈ U)

  Closed : Pred (Pred X ℓ) _
  Closed P = ∃ (λ O → O ∈ Open × (∀ x → x ∈ O → x ∈ P → ⊥))

  Clopen : Pred (Pred X ℓ) _
  Clopen P = Open P × Closed P


  -- Random proofs

  none-Clopen : Clopen (λ _ → Lift ⊥)
  none-Clopen = none , (λ _ → Lift ⊤) , all , (λ _ _ → lower)

  all-Clopen : Clopen (λ _ → Lift ⊤)
  all-Clopen = all , (λ _ → Lift ⊥) , none , (λ _ b _ → lower b)

open Space

Discrete : ∀ {a} (A : Set a) → Space _ _
Discrete A = space A (λ _ → ⊤) _ _ _ _

proof : ∀ {a} {A : Set a} → ∀ S → Clopen (Discrete A) S
proof S = _ , ¬_ ∘ S , _ , λ _ → id

Did you write this yourself? I'm starting to use Agda while following a course on topology, so this is interesting. What does Pred stand for? How could I for example describe the indiscrete topology with your module?