diff --git a/HoTT.thy b/HoTT.thy
index 0e7a674..38097b1 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -24,6 +24,7 @@ Unit
 (* Derived definitions and properties *)
 EqualProps
 Proj
+Univalence
 
 begin