chapter HoTT

session HoTT = Pure +
  description {*
    Homotopy type theory based on intensional Martin-Löf type theory, with a cumulative universe
    hierarchy à la Russell.
    
    Follows the development of the theory in
    The Univalent Foundations Program,
    Homotopy Type Theory: Univalent Foundations of Mathematics,
    Institute for Advanced Study, (2013).
    Available online at https://homotopytypetheory.org/book.
    
    Author: Joshua Chen, University of Bonn (2018)
  *}
  sessions
    "HOL-Eisbach"
  theories
    HoTT (global)
    HoTT_Base
    HoTT_Methods
    "tests/Test"
    "ex/Methods"
    "ex/Synthesis"
    "ex/Book/Ch1"