Require Import WildCat.Core WildCat.NatTrans WildCat.FunctorCat. (** * Category of graphs *) (** ** Definition *) (** A graph is a [Type] together with a relation [$->]. *) Record Graph := { graph_carrier :> Type; isgraph_graph_carrier :: IsGraph graph_carrier }. (** ** Category of graphs *) (** Morphisms of graphs are 0-coherent 1-functors, i.e., maps between the underlying types of the graphs together with an [fmap] functorial map taking arrows to appropriate arrows. This is known as a graph homomorphism. *) Instance isgraph_graph : IsGraph Graph := { Hom A B := Fun01 A B }. (** A 2-cell between graph homomorphisms [F G : A $-> B] is a wild [Transformation], i.e., a family of 1-cells [forall x, F x $-> G x] subject to no coherence conditions. When [A] and [B] have more structure (e.g., they are 1-categories or bicategories) a stronger notion of 2-cell is appropriate, such as a (possibly lax or oplax) natural transformation.*) Instance is2graph_graph : Is2Graph Graph := fun A B => {| Hom F G := Transformation (fun01_F F) (fun01_F G) |}. (** We have identity graph homomorphisms together with compositions of graph homomorphisms. *) Instance is01cat_graph : Is01Cat Graph := { Id A := fun01_id; cat_comp A B C G F := fun01_compose G F }.