Proposition cartesian_closed_struct_poset_laws : closed_under_fun_laws cartesian_closed_struct_poset_data. 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.
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.