(** * Dual functor categories *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Dual Functor.Dual NaturalTransformation.Dual.
Require Import Functor.Identity.
Require Import FunctorCategory.Core.
Require Import Functor.Paths.
Require Import HoTT.Tactics.

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

Local Open Scope functor_scope.

Section opposite.
  Context `{Funext}.

  (** ** Functors [(C → D) ↔ (Cᵒᵖ → Dᵒᵖ)ᵒᵖ] *)
  Definition opposite_functor (C D : PreCategory) : Functor (C -> D) (C^op -> D^op)^op
    := Build_Functor
         (C -> D) ((C^op -> D^op)^op)
         (fun F => F^op)%functor
         (fun _ _ T => T^op)%natural_transformation
         (fun _ _ _ _ _ => idpath)
         (fun _ => idpath).

  Local Ltac op_t C D :=
    split;
    path_functor;
    repeat (apply path_forall; intro);
    simpl;
    destruct_head NaturalTransformation;
    exact idpath.

  (** ** The above functors are isomorphisms *)
  Definition opposite_functor_law C D
  : opposite_functor C D o (opposite_functor C^op D^op)^op = 1
    /\ (opposite_functor C^op D^op)^op o opposite_functor C D = 1.
H: Funext
C, D: PreCategory
(opposite_functor C D
 o (opposite_functor C^op D^op)^op = 1) *
((opposite_functor C^op D^op)^op
 o opposite_functor C D = 1)
  Proof.
H: Funext
C, D: PreCategory
(opposite_functor C D
 o (opposite_functor C^op D^op)^op = 1) *
((opposite_functor C^op D^op)^op
 o opposite_functor C D = 1)
    op_t C D.
  Qed.
End opposite.