Definition monotone_function_app_l {X Y Z : dcpo} (f : monotone_function (X × Y) Z) (x : X) : monotone_function Y Z. Proof. simple refine (_ ,, _). - exact (λ y, f (x ,, y)). - abstract (intros y₁ y₂ p ; cbn ; apply f ; exact (refl_PartialOrder X x ,, p)). 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.