Definition type_products_struct_dcpo (I : UU) : hset_struct_type_prod struct_dcpo I. Proof. simple refine (_ ,, _). - exact (λ D DD, @depfunction_dcpo_struct I (λ i, D i ,, DD i)). - split ; cbn. + abstract (intros D DD i ; exact (is_scott_continuous_depfunction_pr (λ i, D i ,, DD i) i)). + abstract (intros D DD W DW fs Hfs ; exact (@is_scott_continuous_depfunction_map _ (λ i, D i ,, DD i) (W ,, 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.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits.