Library TopologyCategory


Require Import Utf8.
Require Export Topology TopologicalContinuity Category.
Require Import Notations Common.

Set Implicit Arguments.

Generalizable All Variables.

Category of Topologies

There's a category Top of topological spaces, where continuous maps are the morphisms

Section CategoryOfTopologies.
  Record > TotalTopology :=
    {
      TypeOfTotalTopology :> Type;
      TopologyOfTotalTopology :> Topology TypeOfTotalTopology
    }.

  Definition CategoryOfTopologies : @Category TotalTopology.
    refine {| Morphism := (fun s d : TotalTopology { f : s d | continuous s d f });
              Identity := (fun x exist _ _ (identity_is_continuous x));
              Compose := (fun _ _ _ m1 m2 exist _ _ (compose_continuous (proj2_sig m1) (proj2_sig m2))) |};
    abstract (repeat intro; simpl_eq; try reflexivity).
  Defined.
End CategoryOfTopologies.