Definition monotone_function_app_r {X Y Z : dcpo} (f : monotone_function (X × Y) Z) (y : Y) : monotone_function X Z. Proof. simple refine (_ ,, _). - exact (λ x, f (x ,, y)). - abstract (intros y₁ y₂ p ; cbn ; apply f ; exact (p ,, refl_PartialOrder Y y)). Defined.
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.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.