Proposition iterate_on_pt_scott_continuous_map_fun_pt {X : dcpo} (n : ℕ) (f : scott_continuous_map X X) (x : X) : iterate_on_pt_scott_continuous_map n (f x ,, f) = f (iterate_on_pt_scott_continuous_map n (x ,, f)). Proof. revert x. induction n as [ | n IHn ]. - intro ; cbn. apply idpath. - intro x. simpl ; unfold prodtofuntoprod ; simpl. apply IHn. Qed.
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.