codyroux

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

Record Mor (A B : Dial_2) :=
  {
  f : U A -> U B;