Equi-inhabitation of types predefined?

Using Coq
1

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?

2

iffT is defined in CRelationClasses
no notation for it afaict though

Gaëtan Gilbert

3

In HoTT this is called propositional equivalence.

4

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