Library DiscreteTopology


Require Import Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import Finite_sets Classical IndefiniteDescription.
Require Export Topology.
Require Import Notations Common PreOrderCategory CategoryIsomorphisms Orders Morphism.

Set Implicit Arguments.

Generalizable All Variables.

Discrete Topology


Section discrete_topology.
  Variable X : Type.

  Definition DiscreteTopology : Topology X.
    refine {| Open := (fun U True) |};
    try abstract intuition.
  Defined.
End discrete_topology.