LIBRARY

HOMOTOPY LIBRARY

Homotopy Library for Anders proof assistant consists of two parts Foundations and Mathematics just as HoTT Book.

Foundations

MLTT, Modal and Univalent Foundations represent a basic language primitives of Anders and its base library.

MLTT

  1. Π, Σ, =
  2. 0, 1, 2, W
  3. +, 1+
  4. N, LIST
  5. FIN, VEC
  1. DERHAM
  2. PROCESS
  3. INFINITESIMAL

UNIVALENT

  1. EQUIV
  2. ISO
  3. FUNEXT
  4. PATH
  5. GLUE

Mathematics

The second part is dedicated to mathematical models and theories internalized in this language.

ALGEBRA

  1. ALGEBRA
  2. HOMOLOGY

GEOMETRY

  1. ETALE
  2. BUNDLE
  3. MANIFOLD

HOMOTOPY

  1. COEQUALIZER
  2. PUSHOUT
  3. PULLBACK
  4. HOPF
  5. CW

CATEGORIES

  1. CATEGORY
  2. FUNCTOR
  3. GROUPOID

TOPOI

  1. TOPOS
  2. PRESHEAF

The base library for cubicaltt is given on separate page: Formal Mathematics: The Cubical Base Library