Definition set_coproducts_struct_dcpo (I : hSet) : hset_struct_set_coprod struct_dcpo I. Proof. simple refine (_ ,, _). - exact (λ Y PY, coproduct_set_dcpo_struct (λ i, Y i ,, PY i)). - simple refine (_ ,, _) ; cbn. + abstract (intros Y PY ; cbn ; exact (is_scott_continuous_incl (λ i, Y i ,, PY i))). + abstract (refine (λ Y PY W PW f Pf, _) ; exact (@is_scott_continuous_set_coproduct_map I (λ i, Y i ,, PY i) (W ,, PW) f Pf)). 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.