Definition bottom_element_fixpoint_dcpo : bottom_element (fixpoint_dcpo f). Proof. simple refine ((least_fixpoint ,, _) ,, _). - apply is_fixpoint_least_fixpoint. - exact (λ x, is_least_fixpoint_least_fixpoint _ (pr2 x)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Examples.Fixpoints. Require Import UniMath.OrderTheory.DCPOs.Examples.Exponentials. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.