Definition type_precat : precategory. Proof. use make_precategory. - use tpair; use tpair. + exact UU. + exact (λ X Y, X -> Y). + exact (λ X, idfun X). + exact (λ X Y Z f g, funcomp f g). - repeat split; intros; apply idpath. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.