Library IndiscreteTopology


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.

Indiscrete Topology


Section indiscrete_topology.
  Variable X : Type.

  Local Open Scope topology_scope.

  Local Ltac t' :=
    repeat match goal with
             | [ H : ?X = ?Y, _ : ?x ?X |- ?x ?Y ] ⇒ rewrite <- H; assumption
             | [ H : ?B = Ensembles.Empty_set _ |- _ _ ?B = Ensembles.Empty_set _ ] ⇒ right
             | [ H : ?A = Ensembles.Empty_set _ |- _ ?A _ = Ensembles.Empty_set _ ] ⇒ right
             | [ HA : ?A = Full_set _, HB : ?B = Full_set _ |- ?A ?B = Full_set _ _ ] ⇒ left
             | _intro
             | _split
             | _progress subst
             | _progress (destruct_head_hnf or)
             | _progress (destruct_head_hnf Intersection)
             | _progress (destruct_head_hnf ArbitraryUnion)
             | _apply Extensionality_Ensembles
             | _progress firstorder
             | _progress specialize_all_ways
           end.
  Local Ltac t := solve [ left; t' | right; t' | t' ].

  Definition IndiscreteTopology : Topology X.
    refine {| Open := (fun U U = Full_set _ U = Ensembles.Empty_set _) |};
    abstract (
        repeat intro;
        match goal with
          | [ XjP : _ |- _ ] ⇒
            (destruct (classic ( x, x XjP x = Full_set X)); t)
          | _t
        end
      ).
  Defined.
End indiscrete_topology.