Definition is_precategory_Undercategory_data : is_precategory Undercategory_data. Proof. repeat split. - intros. apply Under_mor_equality. apply id_left. - intros. apply Under_mor_equality. apply id_right. - intros. apply Under_mor_equality. apply assoc. - intros. apply Under_mor_equality. apply assoc'. 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.