module Main where
{-
--------- Меняя мир морфизм за морфизмом ------------
Как с нуля построить инструмент моделирования, анализа и программирования

Мы начнем создавать формализм теории категорий и применять его к самому себе
и окружающему миру. Начать можно было бы с естественного языка, но на нем
очень легко ошибаться. Поэтому начнем мы с сочетания естественного языка 
и существующего формализма - теории типов Пера Мартина-Лёффа в его реализации в 
системе Agda.

Мы постараемся использовать абсолютный минимум от Agda, как можно раньше переходя
на собственный, создаваемый формализм. Мы практически не будем использовать стандартную
библиотеку. Целью не является изучение Agda. Все используемые конструкции будут объясняться
на естественном языке ровно в том объеме, который нам необходим.

Многие вещи в тексте являются ссылками. Ниже мы включаем модуль FirstConcepts.
Чтобы перейти к содержимому этого модуля, можно щелкнуть на его имени.
-} 

module Agda where
    -- Основные понятия Agda и пустой тип ∅
    import FirstConcepts

    -- Curry-Howard correspondence. Типы как утверждения. 
    import CurryHoward
    -- Понятие идентичности объектов
    import PropositionalEquivalence
    -- Отношения
    import Relations
    -- Записи, отношение эквивалентности
    import  Equivalence
    -- Пропозициональная эквивалентность (тождественность)
    import EqReasoning

module Categories where
   -- Ура ! понятие категории!
  import Category
-- К этому моменту у нас есть понятие о мире категорий и первый представитель этого мира
-- Мы уже можем начать его продуктивно изучать. 
  module ConstructionsInCategoryTheory where
  module ExamplesOfCategories where