Definition type_products_struct_dcppo_strict (I : UU) : hset_struct_type_prod struct_dcppo_strict I. Proof. simple refine (_ ,, _). - exact (λ D PD, depfunction_dcppo_struct (λ i, D i ,, PD i)). - split ; cbn. + abstract (intros D PD i ; exact (@is_strict_scott_continuous_depfunction_pr I (λ i, D i ,, PD i) i)). + abstract (intros D PD W DW fs Hfs ; exact (@is_strict_scott_continuous_depfunction_map I (λ i, D i ,, PD 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.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Initial. 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. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct.