Bundled categories.

theories/Diagrams/ConstantDiagram.v

@@ -2,7 +2,7 @@ Require Import Basics Types.Paths.
 Require Import Cone.
 Require Import Cocone.
 Require Import Diagram.
-Require Import Graph.
+Require Import Diagrams.Graph.
 
 (** * Constant diagram *)
 

theories/WildCat.v

@@ -29,6 +29,8 @@ Require Export WildCat.Prod.
 Require Export WildCat.Sum.
 Require Export WildCat.Forall.
 Require Export WildCat.Sigma.
+Require Export WildCat.Graph.
+Require Export WildCat.Category.
 Require Export WildCat.ZeroGroupoid.
 
 (* Higher categories *)

theories/WildCat/Category.v

@@ -0,0 +1,18 @@
+Require Import Basics.Overture.
+Require Import WildCat.Core WildCat.NatTrans WildCat.FunctorCat.
+
+Record Category := {
+    category_carrier :> Type;
+    isgraph_category_carrier :: IsGraph category_carrier;
+    is01cat_category_carrier :: Is01Cat category_carrier;
+    is2graph_category_carrier :: Is2Graph category_carrier;
+    is1cat_category_carrier :: Is1Cat category_carrier (* This can be seen as the "mixin" in the sense of packed classes. *)
+  }.
+
+Instance isgraph_Cat : IsGraph Category := { Hom A B := Fun11 A B }.
+
+Instance Is2GraphCategory : Is2Graph Category := fun (A B : Category) => {|
+    Hom (F G : Fun11 A B) := NatTrans F G
+|}.
+
+Instance is3graph_Cat : Is3Graph Category := fun (A B : Category) => _.

theories/WildCat/FunctorCat.v

@@ -18,6 +18,7 @@ Coercion fun01_F : Fun01 >-> Funclass.
 Global Existing Instance fun01_is0functor.
 
 Arguments Build_Fun01 A B {isgraph_A isgraph_B} F {fun01_is0functor} : rename.
+Arguments fun01_F {A B isgraph_A isgraph_B} : rename.
 
 Definition issig_Fun01 (A B : Type) `{IsGraph A} `{IsGraph B}
   : _  <~> Fun01 A B := ltac:(issig).

theories/WildCat/Graph.v

@@ -0,0 +1,21 @@
+Require Import Basics.Overture.
+Require Import WildCat.Core WildCat.NatTrans WildCat.FunctorCat.
+
+Record Graph := {
+    graph_carrier :> Type;
+    isgraph_graph_carrier :: IsGraph graph_carrier
+}.
+
+Instance is0Graph_Graph : IsGraph Graph := {
+  Hom A B := Fun01 A B
+}.
+
+Instance Is2GraphGraph : Is2Graph Graph :=
+  fun A B => {| Hom F G := Transformation (fun01_F F) (fun01_F G)|}.
+
+(** There is a (0,1)-category of graphs under composition. *)
+Instance is01cat_Graph : Is01Cat Graph := {
+    Id A := {| fun01_F := idmap; fun01_is0functor := _ |};
+    cat_comp A B C G F :=
+     {| fun01_F := compose G F ; fun01_is0functor := _ |}
+}.

theories/WildCat/Paths.v

@@ -24,11 +24,11 @@ Local Existing Instances isgraph_paths is2graph_paths is3graph_paths | 10.
 
 (** Any type has composition and identity morphisms given by path concatenation and reflexivity. *)
 Global Instance is01cat_paths (A : Type) : Is01Cat A
-  := {| Id := @idpath _ ; cat_comp := fun _ _ _ x y => concat y x |}.
+  := { Id := @idpath _ ; cat_comp := fun _ _ _ x y => concat y x }.
 
 (** Any type has a 0-groupoid structure with inverse morphisms given by path inversion. *)
 Global Instance is0gpd_paths (A : Type) : Is0Gpd A
-  := {| gpd_rev := @inverse _ |}.
+  := { gpd_rev := @inverse _ }.
 
 (** Postcomposition is a 0-functor when the 2-cells are paths. *)
 Global Instance is0functor_cat_postcomp_paths (A : Type) `{Is01Cat A}