Typoid_Typoid は Universe inconsistency になる．のは，そりゃそうだろって感じなんですが，Typoid_is_Typoid が作れるのはいい感じだなぁ，などと思っている．

Typoid_Typoid.v

Class is_Typoid (carrier: Type): Type :=
  { equal: relation carrier;
    prf_equiv :> Equivalence equal }.

Class Typoid: Type :=
  { typoid_carrier: Type;
    is_typoid:> is_Typoid typoid_carrier }.
Coercion typoid_carrier: Typoid >-> Sortclass.

Definition eq_Typoid (S T: Typoid) :=
  typoid_carrier (Typoid:=S) = typoid_carrier (Typoid:=T).

Program Instance Typoid_is_Typoid : is_Typoid Typoid :=
  { equal := eq_Typoid }.
Next Obligation.
  split.
  rewrite /Reflexive /eq_Typoid; congruence.
  rewrite /Symmetric /eq_Typoid; congruence.
  rewrite /Transitive /eq_Typoid; congruence.
Qed.

Program Instance Typoid_Typoid: Typoid :=
  { is_typoid := Typoid_is_Typoid }.