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 profunctor *)
Require Import Category.Core Profunctor.Core HomFunctor.
Set Implicit Arguments.
Generalizable All Variables.
Local Open Scope profunctor_scope.
Section identity.
(** Quoting nLab:
In particular the identity profunctor [Id : C โธ C] is represented by the identity functor and hence is given by the hom-functor [C(โ,โ) : Cแตแต ร C โ Set]. *)
Definition identity `{Funext} (C : PreCategory) : C -|-> C
:= hom_functor C.
End identity.
Module Export ProfunctorIdentityNotations.
Notation "1" := (identity _) : profunctor_scope.
End ProfunctorIdentityNotations.