proposition: Proposition cartesian_closed_struct_poset_laws : closed_under_fun_laws cartesian_closed_struct_poset_data.
proof: Proof. repeat split. - intros X Y PX PY xf yg p. induction xf as [ x [ f Hf ]]. induction yg as [ y [ g Hg ]]. cbn in *. induction p as [ p q ]. exact (trans_PartialOrder PY (q x) (Hg _ _ p)). - intros X Y Z PX PY PZ f Pf z₁ z₂ p x. cbn in *. exact (Pf (x ,, z₁) (x ,, z₂) (refl_PartialOrder PX x ,, p)). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits