Library UniMath.CategoryTheory.DaggerCategories.Transformations


Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.

Require Import UniMath.CategoryTheory.DaggerCategories.Categories.
Require Import UniMath.CategoryTheory.DaggerCategories.Functors.

Local Open Scope cat.

Section DaggerAdjoint.

  Definition dagger_adjoint_data
             {C D : category}
             {dagC : dagger C} {dagD : dagger D}
             {F G : functor C D}
             (dagF : is_dagger_functor dagC dagD F)
             (dagG : is_dagger_functor dagC dagD G)
             (α : nat_trans F G)
    : nat_trans_data G F
    := λ c, dagD _ _ (α c).

  Definition dagger_adjoint_is_nat_trans
             {C D : category}
             {dagC : dagger C} {dagD : dagger D}
             {F G : functor C D}
             (dagF : is_dagger_functor dagC dagD F)
             (dagG : is_dagger_functor dagC dagD G)
             (α : nat_trans F G)
    : is_nat_trans _ _ (dagger_adjoint_data dagF dagG α).
  Show proof.
    intro ; intros.

    apply (dagger_injective dagD).

    refine (dagger_to_law_comp _ _ _ _ _ _ @ _ @ ! dagger_to_law_comp _ _ _ _ _ _).

    refine (maponpaths_2 compose (dagger_to_law_idemp _ _ _ _) _ @ _).
    refine (_ @ ! maponpaths_12 compose (idpath _) (dagger_to_law_idemp _ _ _ _)).

    refine (! maponpaths (compose (α x')) (dagG _ _ f) @ _).
    refine (_ @ maponpaths_12 compose (dagF _ _ f) (idpath _)).

    apply pathsinv0, (pr2 α).

  Definition dagger_adjoint
             {C D : category}
             {dagC : dagger C} {dagD : dagger D}
             {F G : functor C D}
             (dagF : is_dagger_functor dagC dagD F)
             (dagG : is_dagger_functor dagC dagD G)
             (α : nat_trans F G)
    : nat_trans G F
    := _ ,, dagger_adjoint_is_nat_trans dagF dagG α.

End DaggerAdjoint.

Section UnitaryFunctors.

  Definition unitary_functors
             {C D : category}
             {dagC : dagger C} {dagD : dagger D}
             {F G : functor C D}
             (dagF : is_dagger_functor dagC dagD F)
             (dagG : is_dagger_functor dagC dagD G)
    : UU
    := α : nat_trans F G,
        ( x : C, Isos.is_inverse_in_precat (α x) (dagD _ _ (α x))).

End UnitaryFunctors.