Definition depfunction_dcppo_struct {I : UU} (D : I → dcppo) : dcppo_struct (∏ y, D y)%set. Proof. simple refine (depfunction_dcpo_struct (λ i, D i) ,, _ ,, _). - exact (λ i, ⊥_{ D i }). - abstract (intros f i ; cbn ; apply is_min_bottom_dcppo). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. 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.Propositions. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO.