Lemma type_no_homsets : ¬ has_homsets type_precat. Proof. intros H. apply const_bool_eq_distinct. apply H. Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.NoInjectivePairing. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.CategoryTheory.Categories.Type.Core. Require Import UniMath.CategoryTheory.Core.Categories.