Require Import Basics.Overture Basics.Tactics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core.

(** Empty category *)

Global Instance isgraph_empty : IsGraph Empty.
IsGraph Empty
Proof.
IsGraph Empty
  by apply Build_IsGraph.
Defined.

Global Instance is01cat_empty : Is01Cat Empty.
Is01Cat Empty
Proof.
Is01Cat Empty
  srapply Build_Is01Cat; intros [].
Defined.

Global Instance is0gpd_empty : Is0Gpd Empty.
Is0Gpd Empty
Proof.
Is0Gpd Empty
  constructor; intros [].
Defined.

Global Instance is2graph_empty : Is2Graph Empty.
Is2Graph Empty
Proof.
Is2Graph Empty
  intros f g.
f, g: Empty
IsGraph (f $-> g)
  by apply Build_IsGraph.
Defined.

Global Instance is1cat_empty : Is1Cat Empty.
Is1Cat Empty
Proof.
Is1Cat Empty
  snrapply Build_Is1Cat; intros [].
Defined.