• Skip to primary navigation
  • Skip to content
  • Skip to footer
Arend Theorem Prover
  • About
  • Documentation
  • Download
  • Arend Library
    • Getting Started
      • Arend features
      • Downloading Arend
      • Creating first project
      • Arend libraries
      • Short tutorial
    • Tutorial
      • Part I: Dependent Types
      • Part II: Homotopy Type Theory
    • Standard metas
      • Unclassified metas
      • Paths metas
      • Functional metas
      • Algebraic metas
      • Logical metas
      • Debugging metas
    • Language Reference
      • Lexical structure
      • Definitions
      • Expressions
      • Prelude
    • Plugin reference
      • Editor features
      • Navigation
      • Refactoring

    Language Reference

    This section contains the specification of the Arend language.

    • Part I: Dependent Types
      • Basics
      • Propositions and Proofs
      • Indexed Data Types
      • Equality
      • Proofs of Equality
      • Classes and Records
      • Case Expression
      • Universes, Induction, Specifications
    • Part II: Homotopy Type Theory
      • Propositions and Sets
      • Stratified Universes and Univalence
      • Basic Set Theory
      • Spaces and Homotopy Theory
    • GitHub
    • Twitter
    • Feed
    © 2025 Arend Theorem Prover. Powered by Jekyll & Minimal Mistakes.