(* Theory *)
Require Export WildCat.Adjoint.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Export WildCat.Core.
Require Export WildCat.Equiv.
Require Export WildCat.Opposite.
Require Export WildCat.Induced.
Require Export WildCat.EquivGpd.
Require Export WildCat.FunctorCat.
Require Export WildCat.NatTrans.
Require Export WildCat.Yoneda.
Require Export WildCat.Square.
Require Export WildCat.PointedCat.
Require Export WildCat.Bifunctor.
Require Export WildCat.Monoidal.
Require Export WildCat.MonoidalTwistConstruction.
Require Export WildCat.Products.
Require Export WildCat.Coproducts.
Require Export WildCat.Displayed.
Require Export WildCat.DisplayedEquiv.
Require Export WildCat.Pullbacks.
Require Export WildCat.AbEnriched.
[Loading ML file tauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file cc_plugin.cmxs (using legacy method) ... done]
[Loading ML file firstorder_plugin.cmxs (using legacy method) ... done]
Require Export WildCat.EpiStable.

Require Export WildCat.SetoidRewrite.

(* Examples *)
Require Export WildCat.Universe.
Require Export WildCat.Paths.
Require Export WildCat.UnitCat.
Require Export WildCat.EmptyCat.
Require Export WildCat.Prod.
Require Export WildCat.Sum.
Require Export WildCat.Forall.
Require Export WildCat.Sigma.
Require Export WildCat.Graph.
Require Export WildCat.Category.
Require Export WildCat.ZeroGroupoid.

(* Higher categories *)
Require Export WildCat.TwoOneCat.