src/Main.v

   1 Generalizable All Variables.
   2 Require Import Notations.
   3
   4 Require Import Categories_ch1_3.
   5 Require Import Functors_ch1_4.
   6 Require Import Isomorphisms_ch1_5.
   7 Require Import ProductCategories_ch1_6_1.
   8 Require Import OppositeCategories_ch1_6_2.
   9 Require Import SliceCategories_ch1_6_4.
  10
  11 Require Import EpicMonic_ch2_1.
  12 Require Import InitialTerminal_ch2_2.
  13 Require Import SectionRetract_ch2_4.
  14
  15 Require Import Equalizers_ch3_3.
  16 Require Import CoEqualizers_ch3_4.
  17
  18 Require Import Algebras_ch4.
  19
  20 Require Import Enrichment_ch2_8.
  21 Require Import Subcategories_ch7_1.
  22 Require Import NaturalTransformations_ch7_4.
  23 Require Import NaturalIsomorphisms_ch7_5.
  24 Require Import FunctorCategories_ch7_7.
  25 Require Import Coherence_ch7_8.
  26
  27 Require Import PreMonoidalCategories.
  28 Require Import BinoidalCategories.
  29 Require Import MonoidalCategories_ch7_8.
  30 Require Import PreMonoidalCenter.
  31
  32 Require Import Exponentials_ch6.
  33 Require Import Yoneda_ch8.
  34 Require Import Adjoints_ch9.
  35
  36 (*Require Import CategoryOfCategories_ch7_1.*)
  37 (*Require Import PolynomialCategories.*)
  38 (*Require Import CoqCategory.*)
  39 (*Require Import CartesianEnrichmentsHaveMonoidalHomFunctors.*)
  40
  41 Require Import RepresentableStructure_ch7_2.
  42
  43 Require Import EquivalentCategories_ch7_8.
  44 Require Import FreydAFT_ch9_8.
  45 Require Import KanExtension_ch9_6.
  46 Require Import LCCCs_ch9_7.
  47 Require Import Monads_ch10.
  48 Require Import NaturalNumbersObject_ch9_8.
  49 Require Import Presheaves_ch9_7.
  50
  51 (* very slow! *)
  52 Require Import FreydCategories.
  53 (*Require Import Arrows.*)