Equi-inhabitation of types predefined?

Is something like equi-inhabitance of types predefined in Coq?

Definition iffT (X Y: Type) : Type :=
  (X -> Y) * (Y -> X).

Notation "X <=> Y" := (iffT X Y) (at level 95, no associativity).

Anyone knows the proper name? Type equivalence?

iffT is defined in CRelationClasses
no notation for it afaict though

Gaƫtan Gilbert

In HoTT this is called propositional equivalence.

Perfect name. In Coq propositional equivalence of types should do it. Thanks.