{n} : IsCategory [n]. Proof. exact _. Defined.
Require Import Category.Subcategory.Full. Require Import Category.Sigma.Univalent. Require Import Category.Morphisms Category.Univalent Category.Strict. Require Import HoTT.Basics HoTT.Types HoTT.Spaces.Nat.Core.