• Skip to primary navigation
  • Skip to content
  • Skip to footer
Arend Theorem Prover
  • About
  • Documentation
  • Download
    • Getting Started
    • Language Reference
      • Lexical structure
      • Definitions
      • Expressions
      • Prelude
    • Tutorial
      • 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
    • Libraries
    • Standard metas
      • Unclassified metas
      • Paths metas
      • Functional metas
      • Algebraic metas
      • Logical metas
      • Debugging metas

    Part II: Homotopy Type Theory

    This part is a practical introduction to homotopy type theory in the context of Arend. Themes discussed here include data types with conditions (higher inductive types) and homotopy levels of universes.

    • Propositions and Sets
    • Stratified Universes and Univalence
    • Basic Set Theory
    • Spaces and Homotopy Theory
    • GitHub
    • Twitter
    • Feed
    © 2022 Arend. Powered by Jekyll & Minimal Mistakes.