diff --git a/theories/HoTT/Relation.v b/theories/HoTT/Relation.v
index 2356251e..dc710df5 100644
--- a/theories/HoTT/Relation.v
+++ b/theories/HoTT/Relation.v
@@ -12,6 +12,7 @@ From Equations Require Import Init.
 
 Set Warnings "-notation-overridden".
 Require Import Equations.HoTT.Logic.
+Require Export Equations.HoTT.Iff.
 
 Local Open Scope equations_scope.