Library GraphCategory


Require Import Utf8.
Require Export Category Graph.

Set Implicit Arguments.

Generalizable All Variables.

Category of Graphs

Section CategoryOfGraphs.
  Definition CategoryOfGraphs : @Category Graph.
    refine {|
        
        Morphism := GraphHomomorphism;
        Identity := identity_graph_homomorphism;
        Compose := compose_graph_homomorphisms
      |};
    abstract (
        intros;
        apply GraphHomomorphism_Eq;
        reflexivity
      ).
  Defined.

  Definition CategoryOfGraph's : @Category Graph'.
    refine {|
        
        Morphism := Graph'Homomorphism;
        Identity := identity_graph'_homomorphism;
        Compose := compose_graph'_homomorphisms
      |};
    abstract (
        intros;
        apply Graph'Homomorphism_Eq;
        reflexivity
      ).
  Defined.
End CategoryOfGraphs.