Universe Abstractions

A Lean 4 project to automate proofs that follow from structural properties, based on a simple generalized Universe concept.

This is still work in progress and subject to frequent refactoring.

For a mathematical description, see UniverseAbstractions.pdf.

Directory Structure

• Axioms: Abstract definition of a universe and of structure on universes.
  • Universe: Basic structure that most universes should have in some form: identities (also called "instance equivalences"), functors, products, (type) equivalences.
    • DependentTypes: Dependent versions of functors and products, i.e. Π and Σ types. These tend to involve multiple universes.
    • FunctorialIdentities: Properties that arise if operations on identities are assumed to be functorial (currently very experimental).
• Lemmas: Derived definitions and proofs that work generically on universes (with structure).
• Instances: Definitions of specific universes, including native Lean universes with their structure.
• Meta: Meta-level code to work with universes.
  • Tactics: Currently just one tactic, which builds a functor from a lambda term.
• CategoryTheory: Standard constructions from category theory, generalized to use instance equivalences instead of equality, so that they are compatible with higher categories.
• MathlibFragments: Small parts of mathlib ported to Lean 4; slightly generalized so we can use the ≃ notation for instance equivalences.