{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module book where

-- Formalization with --safe enabled
open import book.00-preamble public
open import book.02-pi public
open import book.03-natural-numbers public
open import book.04-inductive-types public
open import book.05-identity-types public
open import book.06-universes public
open import book.07-modular-arithmetic public
open import book.08-decidability-in-number-theory public
open import book.08-integers public
open import book.09-equivalences public
open import book.10-contractible-types public
open import book.11-fundamental-theorem public
open import book.12-truncation-levels public

-- Formalization with --safe disabled
open import book.13-function-extensionality public
open import book.13-function-extensionality-solutions public
open import book.14-propositional-truncation public
open import book.15-image public
open import book.16-finite-types public
open import book.17-univalence public
open import book.18-set-quotients public
open import book.19-groups public
open import book.20-real-numbers public
open import book.21-circle public
open import book.22-universal-cover-circle public
open import book.23-pullbacks public
open import book.24-pushouts public
open import book.25-cubical-diagrams public
open import book.26-descent public
open import book.26-id-pushout public
open import book.27-sequences public
open import book.b-systems public
open import book.W-types public
