Valeria: Dial_2(Set) is a category

dial_2.v

Record Dial_2 :=
  {
  U : Type;
  X : Type;
  alpha : U -> X -> Prop
  }.

Record Mor (A B : Dial_2) :=
  {
  f : U A -> U B;
  F : X B -> X A;
  prop : forall u y, alpha A u (F y) -> alpha B (f u) y
  }.

Definition id {A} : Mor A A.
Proof.
  split with (f := fun x => x) (F := fun x => x).
  firstorder.
Defined.

Print id.

Definition comp {A B C} : Mor A B -> Mor B C -> Mor A C.
Proof.
  intros ? ?.
  destruct X0; destruct X1.
  split with (f := fun x => f1 (f0 x)) (F := fun x => F0 (F1 x)).
  firstorder.
Defined.

Print comp.

Theorem id_left {A B} : forall gamma : Mor A B, comp gamma id = gamma.
Proof.
  intros [f F h]; unfold comp, id; simpl.
  f_equal.
Qed.

Theorem id_right {A B} : forall gamma : Mor A B, comp id gamma = gamma.
Proof.
  intros [f F h]; unfold comp, id; simpl.
  f_equal.
Qed.

Theorem comp_assoc {A B C D} :
  forall (gamma : Mor A B) (delta : Mor B C) (iota : Mor C D),
    comp gamma (comp delta iota) = comp (comp gamma delta) iota.
Proof.
  intros [f0 F0 h0] [f1 F1 h1] [f2 F2 h2].
  unfold comp; simpl.
  f_equal.
Qed.

Valeria says Dial_L(Set) is a category, where L is a monoidal closed poset (L, \leq, \otimes, \linimp, 1) where
a,b,c in L ==> a\otimes b \leq c iff a \leq (b\linimp c) linimp = linear implication

Or (instead of generalizing L) you can prove Dial_2(Set) is a symmetric monoidal closed category.