(n : nat) : Type0 := match n with | 0 => Empty | 1 => Unit | S n' => n' + Unit end. Coercion : nat >-> Sortclass. Global Instance trunc_cardinality_representative (n : nat) : IsHSet ( n). Proof. induction n; [ typeclasses eauto |]. induction n; [ typeclasses eauto |]. apply istrunc_S. intros [x|x] [y|y]; typeclasses eauto. Qed.
Require Import Category.Core DiscreteCategory IndiscreteCategory. Require Import Types.Unit Trunc Types.Sum Types.Empty. Require Import Basics.Nat.