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 .
(** * Dual functor categories *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
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 Implicit Arguments .
Generalizable All Variables .
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 .