(*
Require Import structures.Category.
Require Import structures.Lattice.
Require Import lattices.Upset.
Require Import lattices.LatticeProduct.
Require Import lattices.FCD.
*)

Definition esig := Type → Type.

Delimit Scope esig_scope with esig.
Bind Scope esig_scope with esig.

Inductive esum {E F : esig} : esig :=
  | einl {X} : E X → esum X
  | einr {X} : F X → esum X.

Arguments esum : clear implicits.

Infix "+" := esum : esig_scope.

Inductive empty_sig : esig := .

Notation "0" := empty_sig.

(*
Class LazyMorphism {A B : cdlattice} (f : A -> B) :=
  {
    lcdlm_inf :> Inf.Morphism f;
    lcdlm_sup {I} (x : I -> A) :
      inhabited I -> f (lsup x) = lsup (f @ x);
  }.

Record interp {E : esig} {A : cdlattice} :=
  {
    op {ar} (m : E ar) :> (A ^ ar)mor;*)