How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.

topology.v

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

(* We think of subsets as propositional functions.
   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
   [U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.

(* A subset is in general defined as [fun x : A => ...]. We introduce
   a more familiar subset notation. NB: We are overriding Coq's standard
   notation for dependent sums. Luckily, we are not going to use dependent
   sums, so this is not a problem. *)
Notation "{ x : A | P }" := (fun x : A => P).

Definition singleton {A : Type} (x : A) := { y : A | x = y }.

(* Definition and notation for subset relation. *)
Definition subset {A : Type} (u v : P A) :=
  forall x : A, u x -> v x.

Notation "u <= v" := (subset u v).

(* Disjointness. *)
Definition disjoint {A : Type} (u v : P A) :=
  forall x, ~ (u x /\ v x).

(* We are going to write a lot of statements of the form
   [forall x : A, U x -> P] and we'd like to write
   them in a less verbose manner. We introduce a notation
   that lets us write [all x : U, P] -- Coq will figure
   out what [A] is. *)
Notation "'all' x : U , P" := (forall x, U x -> P) (at level 20, x at level 99).

(* Similarly for existence. *)
Notation "'some' x : U , P" := (exists x, U x /\ P) (at level 20, x at level 99).

(* Arbitrary unions and binary intersections *)

Definition union {A : Type} (S : P (P A)) :=
  { x : A | some U : S , U x }.

Definition inter {A : Type} (u v : P A) :=
  { x : A | u x /\ v x }.

(* Infix notation for intersections. *)
Notation "u * v" := (inter u v).

(* The empty and the full set. *)

Definition empty {A : Type} := { x : A | False }.

Definition full {A : Type} := { x : A | True }.

(* A topology in a type [A] is a structure which consists
   of a family of subsets (called the opens), satisfying
   the usual axioms. In Coq this amounts to the following
   definition. The mysterious [:>] means "automatically
   coerce from the topology structure to its opens". This
   is useful as it lets us write [U : T] instead of
   [U : opens T].
*)

Structure topology (A : Type) := {
  open :> P A -> Prop ;
  empty_open : open empty ;
  full_open : open full ;
  inter_open : all u : open, all v : open, open (u * v) ;
  union_open : forall S, S <= open -> open (union S)
}.

(* The discrete topology on a type. *)
Definition discrete (A : Type) : topology A.
Proof.
  exists full ; firstorder.
Defined.

(* The definition of a T_1 space. *)
Definition T1 {A : Type} (T : topology A) :=
  forall x y : A,
    x <> y ->
      some u : T, (u x /\ ~ (u y)).

(* The definition of Hausdorff space. *)
Definition hausdorff {A : Type} (T : topology A) :=
  forall x y : A,
  x <> y ->
    some u : T, some v : T,
      (u x /\ v y /\ disjoint u v).

(* A discrete space is Hausdorff. *)
Lemma discrete_hausdorff {A : Type} : hausdorff (discrete A).
Proof.
  intros x y N.
  exists { z : A | x = z } ; split ; [exact I | idtac].
  exists { z : A | y = z } ; split ; [exact I | idtac].
  repeat split ; auto.
  intros z [? ?].
  absurd (x = y) ; auto.
  transitivity z ; auto.
Qed.

(* Every Hausdorff space is T1. *)
Lemma hausdorff_is_T1 {A : Type} (T : topology A) :
  hausdorff T -> T1 T.
Proof.
  intros H x y N.
  destruct (H x y N) as [u [? [v [? [? [? G]]]]]].
  exists u ; repeat split ; auto.
  intro.
  absurd (u y /\ v y) ; auto.
Qed.

(* Indiscrete topology. A classical mathematician will be tempted to use
   disjunction: a set is open if it is either empty or the whole set. But
   that relies on excluded middle and generally causes trouble. Here is
   a better definition: a set is open iff as soon as it contains an element,
   it is the whole set. *)
Definition indiscrete (A : Type) : topology A.
Proof.
  exists { u : P A | forall x : A, u x -> (forall y : A, u y) } ; firstorder.
Defined.

(* Let us prove that the indiscrete topology is the least one.
   We seem to need extensionality for propositions. *)
Lemma indiscrete_least (A : Type) (T : topology A) :
  (forall (X : Type) (s t : P X), s <= t -> t <= s -> s = t) ->
  indiscrete A <= T.
Proof.
  intros ext u H.
  (* Idea: if u is in the indiscrete topology then it is the union of all
     T-opens v which it meets. *)
  assert (G : (u = union { v : P A | T v /\ some x : v, u x })).
  - apply ext.
    + intros x ?. exists full ; firstorder using full_open.
    + intros x [v [[? [y [? ?]]] ?]] ; now apply (H y).
  - rewrite G ; apply union_open ; firstorder.
Qed.

(* Particular point topology, see
   http://en.wikipedia.org/wiki/Particular_point_topology, but of course
   without unecessary excluded middle.
*)
Definition particular {A : Type} (x : A) : topology A.
Proof.
  exists { u : P A | (exists y, u y) -> u x } ; firstorder.
Qed.

(* The topology generated by a family B of subsets that are
   closed under finite intersections. *)
Definition base {A : Type} (B : P (P A)) : 
  B full -> (all u : B, all v : B, B (u * v)) -> topology A.
Proof.
  intros H G.
  exists { u : P A | forall x, u x <-> some v : B, (v x /\ v <= u) }.
  - firstorder.
  - firstorder.
  - intros u Hu v Hv x.
    split.
    + intros [Gu Gv].
      destruct (proj1 (Hu x) Gu) as [u' [? [? ?]]].
      destruct (proj1 (Hv x) Gv) as [v' [? [? ?]]].
      exists (u' * v') ; firstorder.
    + intros [w [? [? ?]]].
      split ; now apply H2.
  - intros S K x.
    split.
    + intros [u [H1 H2]].
      destruct (K u H1 x) as [L1 _].
      destruct (L1 H2) as [v ?].
      exists v ; firstorder.
    + firstorder.
Defined.

Require Import List.

(* The intersection of a finite list of subsets. *)
Definition inters {A : Type} (us : list (P A)) : P A :=
  {x : A | Forall (fun u =>  u x) us }.

(* The closure of a family of sets by finite intersections. *)
Definition inter_close {A : Type} (S : P (P A)) :=
  { v : P A | some us : Forall S , (forall x, v x <-> inters us x) }.

Lemma Forall_app {A : Type} (l1 l2 : list A) (P : A -> Prop) :
  Forall P l1 -> Forall P l2 -> Forall P (l1 ++ l2).
Proof.
  induction l1 ; simpl ; auto.
  intros H G.
  constructor.
  - apply (Forall_inv H).
  - apply IHl1 ; auto.
    inversion H ; assumption.
Qed.

Lemma Forall_app1 {A : Type} (l1 l2 : list A) (P : A -> Prop) :
  Forall P (l1 ++ l2) -> Forall P l1.
Proof.
  induction l1 ; simpl ; auto.
  intro H.
  inversion H ; auto.
Qed.

Lemma Forall_app2 {A : Type} (l1 l2 : list A) (P : A -> Prop) :
  Forall P (l1 ++ l2) -> Forall P l2.
Proof.
  induction l1 ; simpl ; auto.
  intro H.
  inversion H ; auto.
Qed.

(* The topology generated by a subbase S. *)
Definition subbase {A : Type} (S : P (P A)) : topology A.
Proof.
  apply (base (inter_close S)).
  - exists nil ; firstorder using Forall_nil.
  - intros u [us [Hu Gu]] v [vs [Hv Gv]].
    exists (us ++ vs).
    split ; [ (now apply Forall_app) | idtac ].
    split.
    + intros [? ?].
      apply Forall_app ; firstorder.
    + intro K ; split.
      * apply Gu.
        apply (Forall_app1 _ _ _ K).
      * apply Gv.
        apply (Forall_app2 _ _ _ K).
Defined.

(* A subbasic set is open. *)
Lemma subbase_open {A : Type} (S : P (P A)) (u : P A) :
  S u -> (subbase S) u.
Proof.
  intros H x.
  split.
  - intro G.
    exists u ; split ; [ idtac | firstorder ].
    exists (u :: nil).
    split ; [now constructor | idtac].
    intro y ; split.
    + intro ; now constructor.
    + intro K.
      inversion K ; auto.
  - firstorder.
Qed.

(* The cofinite topology on A. *)
Definition cofinite (A : Type) : topology A :=
  subbase { u : P A | exists x, forall y, (u y <-> y <> x) }.

(* The cofinite topology is T1. *)
Lemma cofinite_T1 (A : Type) : T1 (cofinite A).
Proof.
  intros x y N.
  exists { z : A | z <> y }.
  split ; auto.
  apply subbase_open.
  exists y ; firstorder.
Qed.

Interesting. I'd love to see a version done how you feel one should do it natively in Coq, to learn from by comparison. Or is there some established project that already has that where I should go look at it?

Well, if I did it my way, I wouldn't posit that topology is closed under arbitrary unions, nor would I state that opens are subsets of a space. I would axiomatize the Sierpinski space S and then define the topology of a type A to be A -> S, a la synthetic topology.

Ah, so you mean the topology is the type A -> S, and every type comes with an intrinsic topology, as in http://math.andrej.com/2010/01/06/metric-spaces-in-synthetic-topology-2/

Is it possible to represent Subspaces (Subspace topologies) in this formalization? I guess not because you require that (open (@Full A)), so this won't allow us to consider a topology on a subset of A, is that right?

How about Quotient topologies?

i like it