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.
(** * Identity functor *)
Require Import Category.Core Functor.Core.
Set Implicit Arguments.
Generalizable All Variables.
Section identity.
(** There is an identity functor. It does the obvious thing. *)
Definition identity C : Functor C C
:= Build_Functor C C
(fun x => x)
(fun _ _ x => x)
(fun _ _ _ _ _ => idpath)
(fun _ => idpath).
End identity.
Module Export FunctorIdentityNotations.
Notation "1" := (identity _) : functor_scope.
End FunctorIdentityNotations.