Definition WOSET_precategory : precategory. Proof. use make_precategory. - use tpair. + exists ((WellOrderedSet,,isaset_WellOrderedSet) : hSet). apply (λ X Y, pr11 X → pr11 Y). + split; simpl. * intros X; apply idfun. * intros X Y Z f g; apply (g ∘ f). - abstract (now intros). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.exponentials.