Definition type_products_struct_dcppo (I : UU) : hset_struct_type_prod struct_dcppo I. Proof. simple refine (_ ,, _). - exact (λ D DD, @depfunction_dcppo_struct I (λ i, D i ,, DD i)). - split ; cbn. + abstract (intros D DD i ; exact (is_scott_continuous_depfunction_pr (λ i, D i ,, pr1 (DD i)) i)). + abstract (intros D DD W DW fs Hfs ; exact (@is_scott_continuous_depfunction_map _ (λ i, D i ,, pr1 (DD i)) (W ,, pr1 DW) (λ i, fs i ,, Hfs i))). Defined.
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.