Definition unary_interpolation_directed_set : directed_set X. Proof. use make_directed_set. - exact (∑ (i : D), D_a i). - exact (λ ij, D_a (pr1 ij) (pr2 ij)). - exact is_directed_unary_interpolation_directed_set. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.