module README where

------------------------------------------------------------------------
-- A programmer's library for Cubical Agda
------------------------------------------------------------------------

-- Start here
import Prelude

------------------------------------------------------------------------
-- Module hierarchy
------------------------------------------------------------------------

-- Core definitions.
import Foundations.Everything

-- Automating boring things.
import Meta.Everything

-- (Univalently) structured types.
import Structures.Everything

-- (Topo)logical stuff.
import Logic.Everything

-- Vaguely combinatorial things.
import Combinatorics.Everything

-- Homotopy theory.
import Homotopy.Everything

-- Category theory.
import Cat.Everything

-- (Higher) algebra library.
import Algebra.Everything

-- Order theory.
import Order.Everything

-- Basic types and their properties.
import Data.Everything

-- Function kinds.
import Functions.Everything

-- I/O and related stuff.
import System.Everything
