Library HoTT.categories.Functor.Dual

Opposite functors

Require Category.Dual.
Import Category.Dual.CategoryDualNotations.
Require Import Category.Core Functor.Core.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Open Scope category_scope.

Definition of Fᵒᵖ

Definition opposite C D (F : Functor C D) : Functor C^op D^op
  := Build_Functor (C^op) (D^op)
                   (object_of F)
                   (fun s dmorphism_of F (s := d) (d := s))
                   (fun d' d s m1 m2composition_of F s d d' m2 m1)
                   (identity_of F).

Local Notation "F ^op" := (opposite F) (at level 3, format "F ^op") : functor_scope.

Local Open Scope functor_scope.

ᵒᵖ is judgmentally involutive

Definition opposite_involutive C D (F : Functor C D) : (F^op)^op = F
  := idpath.

Module Export FunctorDualNotations.
  Notation "F ^op" := (opposite F) (at level 3, format "F ^op") : functor_scope.
End FunctorDualNotations.