v1.8.0

• New and improved metas:
  • Improved Exists meta and new metas Given and Forall.
  • Improved contradiction meta. Now, it can derive contradictions from transitive closure of <, <=, and =.
  • New simplify meta.
• Locales:
  • The definition of discrete locales and the embedding of rationals into reals.
  • The definition of overt locales and open maps.
  • The construction of dense-closed and strongly dense-weakly closed factorization systems on the category of locales.
  • A proof that nuclei form a frame.
  • Limits and colimits of locales.
  • A characterization of embeddings of locales: a map of locales is a regular monomorphism if and only if the left adjoint is surjective.
  • The definition of (weakly) regular locales and a proof that the locale of reals is regular.
  • The definition of Hausdorff locales and a proof that regular locales are Hausdorff.
  • The definition of uniform locales and the construction of their completion.
• The definition of abstract reduction systems, second-order term rewriting systems, and a proof that the disjoint union of confluent left-linear systems is confluent.
• The definition of algebraic theories, the category of its models, and a proof that it has all small limits and colimits.
• The preorder of subobjects and regular subobjects.
• The construction of the structure sheaf on the spectrum of a ring.