Built with
Alectryon. 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 *)
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.
Require Export WildCat.Pullbacks.
Require Export WildCat.AbEnriched.
Require Export WildCat.EpiStable.
Require Export WildCat.HomologicalAlgebra.
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.