Table of Contents

module library.contents where

Prelude

The following modules introduce the central concepts and methods behind Hyrax, and are an excellent place to start exploring the rest of the library.

• What is Synthetic Mathematics? Introduces the concepts of analytic and synthetic methods in mathematics, and argues for the need to develop tools for the latter:

  -- open import library.synthetic
  

• The Algebraic Essence of Type Theory Describes the theoretical basis of the synthetic approach taken by Hyrax in terms of dependently-typed algebraic theories. The module also discusses the pros and cons of using Agda for this purpose, and the reasons why it was chosen over the alternatives.

  -- open import library.algebraicEssence
  

Philosophy

I studied both Computer Science and Philosophy for my undergraduate degree, and many of the fundamental questions that drive my research remain philosophical in nature. As such, the following modules serve to record my philosophical thoughts as they pertain to the central topics of Hyrax.

• My Research Manifesto describes the aims, motivation, and methods of my research into the abstract structure of logic and computation.

  open import library.philosophy.research-manifesto