Added mention of the unresolved universe situation

Author: YaZko

README.md

@@ -49,3 +49,10 @@ cd ctrees
 ```shell
 dune build
 ```
+
+## Universe issue
+
+We currently unset locally universe checking in several places of the library. This is an annoying, but purely technical issue that affects in no way the soundness of our results.
+
+Given the complexity of the issue, and its root tracing back to other libraries (for instance, importing simultaneously some parts of the [Interaction Tree] library and of the [RelationAlgebra] library triggers a universe inconsistency), we project to tackle the issue as part of the future support in Rocq for alegbraic universes and the release of a universe polymorphic prelude.
+