Proposition is_fixpoint_pataraia_fixpoint : f pataraia_fixpoint = pataraia_fixpoint. Proof. unfold pataraia_fixpoint. pose (p := maponpaths pr1 (pataraia_fixpoint_compose_lemma (restriction_to_post_fixpoint f) (bot_post_fixpoint f))). refine (p @ _). apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Examples.Products. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO.