Definition wosetfun_precategory : precategory. Proof. use make_precategory. - exists (WellOrderedSet,,wofun). split; simpl. + intros X. apply (_,,iswofun_idfun). + intros X Y Z f g. apply (_,,iswofun_funcomp f g). - abstract (now repeat split; simpl; intros; apply wofun_eq). 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.