add DEPRECATED message

Author: williamdemeo

UALib/UALib.lagda

@@ -43,6 +43,15 @@ of citation.
 **Author**. [William DeMeo][]  
 **Affiliation**. [Department of Algebra][], [Charles University in Prague][]
 
+
+<p>
+
+**DEPRECATED** This is the documentation for the old version of the Agda Universal Algebra Library.  For the lastest version, please go to:
+
+[https://ualib.github.io/agda-algebras](https://ualib.github.io/agda-algebras)
+
+</p>
+
 **Abstract**. The [Agda Universal Algebra Library][] ([UALib][]) is a library of types and programs (theorems and proofs) that formalizes the foundations of universal algebra in dependent type theory using the [Agda][] proof assistant language.
 
 In the latest version of the library we have defined many new types for representing the important constructs and theorems that comprise part of the foundations of general (universal) algebra and equational logic. These types are implemented in so called "literate" Agda files, with the `.lagda` extension, and they are grouped into modules so that they may be easily imported into other Agda programs.