Lemma po_homsets_isaprop (PO : po X) (a b : (po_precategory_data PO)) : isaprop (po_precategory_data PO ⟦a,b⟧). Proof. apply propproperty. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence.