src/Main.v

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