arend-lib

• The definion of modules, algebras, strict domains, polynomials, and various structures on them
• A synthetic definition of a derivative and its basic properties
• The definition of real numbers and the construction of the structure of an ordered field on them (except for multiplication).
• A tactic for solving systems of linear equations
• The definition of schemes, affine schemes, and a prove that affine schemes are schemes.
• A partial prove of the univalence for the precategory of ringed locales.

• 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.

• The locale of real numbers
• Compactness of the interval and local compactness of reals
• Spectrum of a ring
• Sheaves
• rewriteEq meta

• A few bug fixes
• Non-unital presentations of frames
• Definition of adjoint functors

• Locales and topological spaces
• Functor category
• Euclidean domains and (extended) Euclidean algorithm
• The quotient ring Z/nZ and the field structure on it for prime n
• Solvers for commutative monoids and rings are implemented in the equation meta
• Extensionality meta
• Structure identity principle meta
• simp_coe meta
• cases meta and improved mcases meta
• unfold and unfold_let metas

• Debug metas (println, random, time)
• Congruence closure
• Insertion and tree sort functions
• Meta mcases

• Implemented at meta.
• Improved contradiction meta.
• Removed unnecessary implicit arguments.

Updates:

• Refine and 'replace with constructor' goal solvers
• Level prover for non-recursive data types
• 'contradiction' meta
• Transitive and equivalence closure
• 'using' and 'hiding' meta definitions
• 'equation' meta
• Construction of K(G,1)

Implemented a few tactics: rewrite, repeat, apply, solver for monoids.

A proof of the generalized Blakers-Massey theorem.

Minor updates

First stable version