Definition Undercategory_data : precategory_data. Proof. exists Undercategory_ob_mor. split. - exact Under_id. - exact Under_comp. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors.