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 functors *)
Require Export Category.Notations Category.Utf8 Functor.Notations.
Require Import Functor.Core Functor.Composition.Core Functor.Dual.
Require Import Basics.Utf8.
Infix "โ" := compose : functor_scope.
Notation "F โ x" := (object_of F x) : object_scope.
Notation "F โ m" := (morphism_of F m) : morphism_scope.
Notation "F 'แตแต'" := (opposite F) : functor_scope.