Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(* Theory *)

[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.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.