Definition binary_coproducts_struct_dcpo : hset_binary_coprod_struct struct_dcpo. Proof. simple refine (_ ,, _). - exact (λ X Y PX PY, coproduct_dcpo_struct (X ,, PX) (Y ,, PY)). - simple refine (_ ,, _ ,, _) ; cbn. + abstract (intros X Y PX PY ; cbn ; exact (is_scott_continuous_inl (X ,, PX) (Y ,, PY))). + abstract (intros X Y PX PY ; cbn ; exact (is_scott_continuous_inr (X ,, PX) (Y ,, PY))). + abstract (intros X Y Z PX PY PZ f g Pf Pg ; exact (@is_scott_continuous_sumofmaps (X ,, PX) (Y ,, PY) (Z ,, PZ) f Pf g Pg)). 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.