(A : Type) `{Is2Graph A} : Is3Graph A := fun _ _ => is2graph_paths _. Local Existing Instances isgraph_paths is2graph_paths | 10. Global Instance is01cat_paths (A : Type) : Is01Cat A := {| Id := @idpath _ ; cat_comp := fun _ _ _ x y => concat y x |}. Global Instance is0gpd_paths (A : Type) : Is0Gpd A := {| gpd_rev := @inverse _ |}. Global Instance is0functor_cat_postcomp_paths (A : Type) `{Is01Cat A} (a b c : A) (g : b $-> c) : Is0Functor (cat_postcomp a g). Proof. snrapply Build_Is0Functor. exact (@ap _ _ (cat_postcomp a g)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids. Require Import WildCat.Core WildCat.TwoOneCat WildCat.NatTrans.