Definition equalizers_struct_dcppo_strict : hset_equalizer_struct struct_dcppo_strict. Proof. simple refine (_ ,, _). - intros X Y f g DX DY Df Dg. exact (@equalizer_dcppo_struct (X ,, DX) (Y ,, DY) (f ,, Df) (g ,, Dg)). - split. + abstract (intros X Y f g DX DY Df Dg ; cbn in * ; exact (@is_strict_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_strict_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.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.