Definition poset_fun_space {X Y : hSet} (PX : PartialOrder X) (PY : PartialOrder Y) : PartialOrder (@struct_fun_hSet struct_poset X Y PX PY). Proof. use make_PartialOrder. - exact (λ f g, ∀ (x : X), PY (pr1 f x) (pr1 g x)). - refine ((_ ,, _) ,, _). + abstract (intros f g h p q x ; exact (trans_PartialOrder PY (p x) (q x))). + abstract (intros f x ; exact (refl_PartialOrder PY (pr1 f x))). + abstract (intros f g p q ; use eq_monotone_function ; intro x ; exact (antisymm_PartialOrder PY (p x) (q x))). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits.