Definition bot_iteration_map (n : ℕ) : X. Proof. induction n as [ | n IHn ]. - exact (⊥_{X}). - exact (f IHn). 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.