Require Import Basics.Overture Basics.Tactics.Require Import Basics.Overture Basics.Tactics.
Require Import WildCat.Core.

(** Unit category *)

Instance isgraph_unit : IsGraph Unit.
IsGraph Unit
Proof.
IsGraph Unit
  apply Build_IsGraph.
Unit -> Unit -> Type
  intros; exact Unit.
Defined.

Instance is01cat_unit : Is01Cat Unit.
Is01Cat Unit
Proof.
Is01Cat Unit
  srapply Build_Is01Cat.
forall a : Unit, a $-> a
forall a b c : Unit, (b $-> c) -> (a $-> b) -> a $-> c
  all: intros; exact tt.
Defined.

Instance is0gpd_unit : Is0Gpd Unit.
Is0Gpd Unit
Proof.
Is0Gpd Unit
  constructor; intros; exact tt.
Defined.

Instance is2graph_unit : Is2Graph Unit
  := fun f g => isgraph_unit.

Instance is1cat_unit : Is1Cat Unit.
Is1Cat Unit
Proof.
Is1Cat Unit
  econstructor.
forall (a b c : Unit) (g : b $-> c), Is0Functor (cat_postcomp a g)
forall (a b c : Unit) (f : a $-> b), Is0Functor (cat_precomp c f)
forall (a b c d : Unit) (f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f $== h $o (g $o f)
forall (a b c d : Unit) (f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) $== h $o g $o f
forall (a b : Unit) (f : a $-> b), Id b $o f $== f
forall (a b : Unit) (f : a $-> b), f $o Id a $== f
  1,2:econstructor.
a, b, c: Unit
g: b $-> c
forall a0 b0 : a $-> b,
(a0 $-> b0) -> cat_postcomp a g a0 $-> cat_postcomp a g b0
a, b, c: Unit
f: a $-> b
forall a0 b0 : b $-> c,
(a0 $-> b0) -> cat_precomp c f a0 $-> cat_precomp c f b0
forall (a b c d : Unit) (f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f $== h $o (g $o f)
forall (a b c d : Unit) (f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) $== h $o g $o f
forall (a b : Unit) (f : a $-> b), Id b $o f $== f
forall (a b : Unit) (f : a $-> b), f $o Id a $== f
  all:intros; exact tt.
Defined.