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 Require Import MonoidalCategories_ch7_8.
  28
  29 Require Import Exponentials_ch6.
  30 (*Require Import CategoryOfCategories_ch7_1.*)
  31 Require Import Yoneda_ch8.
  32 Require Import Adjoints_ch9.
  33
  34 (*Require Import PolynomialCategories.*)
  35 (*Require Import CoqCategory.*)
  36 (*Require Import NaturalDeduction.*)
  37 (*Require Import NaturalDeductionCategories.*)
  38 (*Require Import CartesianEnrichmentsHaveMonoidalRepresentableFunctors.*)
  39 (*Require Import Reification.*)
  40 (*Require Import GeneralizedArrow.*)
  41 (*Require Import ReificationFromGArrow.*)
  42 (*Require Import GArrowFromReification.*)
  43 (*Require Import Roundtrip.*)
  44 (*Require Import RoundtripSlides.*)
  45
  46 (* very slow! *)
  47 (*Require Import FreydCategories.*)
  48 (*Require Import Arrows.*)