Definition equalizers_struct_dcpo : hset_equalizer_struct struct_dcpo. Proof. simple refine (_ ,, _). - intros X Y f g DX DY Df Dg. exact (@equalizer_dcpo_struct (X ,, DX) (Y ,, DY) (f ,, Df) (g ,, Dg)). - refine (_ ,, _). + abstract (intros X Y f g DX DY Df Dg ; exact (@is_scott_continuous_equalizer_pr1 (X ,, DX) (Y ,, DY) (f ,, Df) (g ,, Dg))). + abstract (intros X Y f g DX DY Df Dg W DW h Dh q ; exact (@is_scott_continuous_equalizer_map (X ,, DX) (Y ,, DY) (f ,, Df) (g ,, Dg) (W ,, DW) (h ,, Dh) q)). 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.