Definition Initial_DCPPO_strict : Initial DCPPO_strict. Proof. use make_Initial. - exact unit_dcppo. - intros Y. use iscontraprop1. + abstract (use invproofirrelevance ; intros f₁ f₂ ; use (@eq_strict_scott_continuous_map unit_dcppo Y f₁ f₂) ; intro x ; induction x ; refine (@strict_scott_continuous_map_on_point unit_dcppo _ f₁ @ !_) ; exact (@strict_scott_continuous_map_on_point unit_dcppo _ f₂)). + refine ((λ _, ⊥_{Y}) ,, _). abstract (cbn ; apply is_strict_scott_continuous_constant). 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.