Library HoTT.WildCat

(* Theory *)
Require Export WildCat.Adjoint.
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.

(* See also contrib/SetoidRewrite.v for tools that can be used for rewriting in wild categories. *)

(* 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.ZeroGroupoid.

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