(n : nat) := match n with | 0 => indiscrete_category 0 | 1 => indiscrete_category 1 | S (S n') => discrete_category (S (S n')) end.
Require Import Category.Core DiscreteCategory IndiscreteCategory. Require Import Types.Unit Trunc Types.Sum Types.Empty. Require Import Basics.Nat.