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.
(** * Unicode notations for categories *)
Local Set Warnings "-notation-overridden".
Require Export HoTT.Categories.Notations.
Require Export Category.Utf8 Functor.Utf8 NaturalTransformation.Utf8.
Require Export Comma.Utf8.
Require Export Adjoint.Utf8.
Require Export FunctorCategory.Utf8.
Require Export Profunctor.Utf8.
Require Export Structure.Utf8.
Require ChainCategory.
Export ChainCategory.Utf8.
Require SimplicialSets.
Export SimplicialSets.Utf8.