Library HoTT.Categories.Adjoint.Identity

Identity adjunction 1 ⊣ 1

Require Import Category.Core.
Require Import Functor.Identity NaturalTransformation.Identity.
Require Import Adjoint.UnitCounit Adjoint.Core.

Set Implicit Arguments.
Generalizable All Variables.

Section identity.

There is an identity adjunction. It does the obvious thing.

  Definition identity C : @Adjunction C C 1 1
    := @Build_AdjunctionUnitCounit
         C C 1 1
         1
         1
         (fun _ ⇒ identity_identity _ _)
         (fun _ ⇒ identity_identity _ _).
End identity.

Module Export AdjointIdentityNotations.
  Notation "1" := (identity _) : adjunction_scope.
End AdjointIdentityNotations.