Proposition cartesian_closed_struct_dcppo_laws : closed_under_fun_laws cartesian_closed_struct_dcppo_data. Proof. split. - intros X Y DX DY ; cbn in *. exact (is_scott_continuous_eval (X ,, pr1 DX) (Y ,, pr1 DY)). - intros X Y Z DX DY DZ f Df ; cbn in *. apply (@is_scott_continuous_lam (X ,, pr1 DX) (Y ,, pr1 DY) (Z ,, pr1 DZ) (f ,, Df)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits.