Library NatCategory


Require Import Utf8.
Require Export Category.
Require Import Common DiscreteCategory.

Set Implicit Arguments.

Generalizable All Variables.

Finite Discrete Category



Definition NatCategory (n : nat) := Eval unfold DiscreteCategory, DiscreteCategory_Identity in DiscreteCategory { k | k < n }.

Coercion NatCategory : nat >-> Category.