(** * Category Theory *)
(** To get all of the category theory library in scope with the proper qualified names, you should [Require Import Categories.] or [Require Import HoTT.Categories.] *)

(** First we give modules to all of the kinds of category theory constructions (corresponding to directories), so that we can refer to them as [Category.foo] or [Functor.foo] after [Require Import Categories.] *)
(** ** Categories *)
Require HoTT.Categories.Category.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
(** ** Functors *)
Require HoTT.Categories.Functor.
(** ** Natural Transformations *)
Require HoTT.Categories.NaturalTransformation.
(** ** Functor Categories *)
Require HoTT.Categories.FunctorCategory.
(** ** Groupoids *)
Require HoTT.Categories.GroupoidCategory.
(** ** Precategory of Groupoids *)
Require HoTT.Categories.CategoryOfGroupoids.
(** ** Discrete Categories *)
Require HoTT.Categories.DiscreteCategory.
(** ** Indiscrete Categories *)
Require HoTT.Categories.IndiscreteCategory.
(** ** Finite Discrete Categories (natural numbers as categories) *)
Require HoTT.Categories.NatCategory.
(** ** Chain Categories [[n]] *)
Require HoTT.Categories.ChainCategory.
(** ** Initial and Terminal Categories *)
Require HoTT.Categories.InitialTerminalCategory.
(** ** The Category of Sets *)
Require HoTT.Categories.SetCategory.
(** ** The Category of Simplicial Sets *)
Require HoTT.Categories.SimplicialSets.
(** ** The Category of Semi-Simplicial Sets *)
Require HoTT.Categories.SemiSimplicialSets.
(** ** The Hom Functor *)
Require HoTT.Categories.HomFunctor.
(** ** Profunctors *)
Require HoTT.Categories.Profunctor.
(** ** The Category of Categories *)
Require HoTT.Categories.Cat.
(** ** Laws about Functor Categories *)
Require HoTT.Categories.ExponentialLaws.
(** ** Laws about Product Categories *)
Require HoTT.Categories.ProductLaws.
(** ** Comma Categories *)
Require HoTT.Categories.Comma.
(** ** Universal Properties and Universal Morphisms *)
Require HoTT.Categories.UniversalProperties.
(** ** Kan Extensions *)
Require HoTT.Categories.KanExtensions.
(** ** Adjunctions *)
Require HoTT.Categories.Adjoint.
(** ** Limits *)
Require HoTT.Categories.Limits.
(** ** Pseudofunctors *)
Require HoTT.Categories.Pseudofunctor.
(** ** Pseudonatural Transformations *)
Require HoTT.Categories.PseudonaturalTransformation.
(** ** Lax Comma Categories *)
Require HoTT.Categories.LaxComma.
(** ** Duality as a Functor *)
Require HoTT.Categories.DualFunctor.
(** ** The Grothendieck Construction *)
Require HoTT.Categories.Grothendieck.
(** ** The Category of Sections of a Functor *)
Require HoTT.Categories.CategoryOfSections.
(** ** The Dependent Product *)
Require HoTT.Categories.DependentProduct.
(** ** The Yoneda Lemma *)
Require HoTT.Categories.Yoneda.
(** ** The Structure Identity Principle *)
Require HoTT.Categories.Structure.
(** ** Fundamental Pregroupoids *)
Require HoTT.Categories.FundamentalPreGroupoidCategory.
(** ** Homotopy PreCategory *)
Require HoTT.Categories.HomotopyPreCategory.

(* We bind the record structures for [PreCategory], [IsCategory], [IsStrictCategory], [Functor], and eventually [NaturalTransformation] at top level. *)
Local Set Warnings Append "-notation-overridden".
Include HoTT.Categories.Category.Core.
Include HoTT.Categories.Category.Strict.
Include HoTT.Categories.Category.Univalent.
Include HoTT.Categories.Functor.Core.
Include HoTT.Categories.NaturalTransformation.Core.
Include HoTT.Categories.FunctorCategory.Core.
Include HoTT.Categories.GroupoidCategory.Core.
Include HoTT.Categories.CategoryOfGroupoids.
Include HoTT.Categories.DiscreteCategory.Core.
Include HoTT.Categories.IndiscreteCategory.Core.
Include HoTT.Categories.NatCategory.Core.
Include HoTT.Categories.ChainCategory.Core.
Include HoTT.Categories.InitialTerminalCategory.Core.
Include HoTT.Categories.SetCategory.Core.
Include HoTT.Categories.SimplicialSets.Core.
Include HoTT.Categories.SemiSimplicialSets.Core.
Include HoTT.Categories.HomFunctor.
Include HoTT.Categories.Profunctor.Core.
Include HoTT.Categories.Cat.Core.
Include HoTT.Categories.Comma.Core.
Include HoTT.Categories.UniversalProperties.
Include HoTT.Categories.KanExtensions.Core.
Include HoTT.Categories.Adjoint.Core.
Include HoTT.Categories.Limits.Core.
Include HoTT.Categories.Pseudofunctor.Core.
Include HoTT.Categories.PseudonaturalTransformation.Core.
Include HoTT.Categories.LaxComma.Core.
Include HoTT.Categories.DualFunctor.
Include HoTT.Categories.CategoryOfSections.Core.
Include HoTT.Categories.DependentProduct.
Include HoTT.Categories.Yoneda.
Include HoTT.Categories.Structure.Core.
Include HoTT.Categories.FundamentalPreGroupoidCategory.
Include HoTT.Categories.HomotopyPreCategory.

Require Export HoTT.Categories.Notations.

(** Some checks that should pass, if all of the importing went correctly. *)
(*Check PreCategory.
Check IsStrictCategory _.
Check Category.compose.
Check Category.sum.
Check Category.Sum.sum_compose.
Check Functor.sum.
Check Functor.Prod.Core.unique.
Check (_ o _)%morphism.
Check (_ o _)%functor.*)