X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Flib%2Fhott%2FOverture.ma;h=e02683ffa8650caad5010be9e2904dea502f0c6d;hb=12d58352dbd62df65d44becc0f69fc5a7b370866;hp=3725123cce1e23424349e2f6dd848c6095668663;hpb=bfc9b5c983a046e1fcd111dbe8518c827643861e;p=helm.git

diff --git a/matita/matita/lib/hott/Overture.ma b/matita/matita/lib/hott/Overture.ma
index 3725123cc..e02683ffa 100644
--- a/matita/matita/lib/hott/Overture.ma
+++ b/matita/matita/lib/hott/Overture.ma
@@ -1,4 +1,5 @@
 include "hott/types.ma".
+include "basics/core_notation/compose_2.ma".
 
 (* * * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *)