Generalizable All Variables. Require Import Notations. Require Import Categories_ch1_3. Require Import Functors_ch1_4. Require Import Isomorphisms_ch1_5. Require Import ProductCategories_ch1_6_1. Require Import OppositeCategories_ch1_6_2. Require Import SliceCategories_ch1_6_4. Require Import EpicMonic_ch2_1. Require Import InitialTerminal_ch2_2. Require Import SectionRetract_ch2_4. Require Import Equalizers_ch3_3. Require Import CoEqualizers_ch3_4. Require Import Algebras_ch4. Require Import Enrichment_ch2_8. Require Import Subcategories_ch7_1. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. Require Import FunctorCategories_ch7_7. Require Import Coherence_ch7_8. Require Import PreMonoidalCategories. Require Import BinoidalCategories. Require Import MonoidalCategories_ch7_8. Require Import PreMonoidalCenter. Require Import Exponentials_ch6. Require Import Yoneda_ch8. Require Import Adjoints_ch9. (*Require Import CategoryOfCategories_ch7_1.*) (*Require Import PolynomialCategories.*) (*Require Import CoqCategory.*) (*Require Import CartesianEnrichmentsHaveMonoidalHomFunctors.*) Require Import RepresentableStructure_ch7_2. Require Import EquivalentCategories_ch7_8. Require Import FreydAFT_ch9_8. Require Import KanExtension_ch9_6. Require Import LCCCs_ch9_7. Require Import Monads_ch10. Require Import NaturalNumbersObject_ch9_8. Require Import Presheaves_ch9_7. (* very slow! *) Require Import FreydCategories. (*Require Import Arrows.*)