Library UniMath.Bicategories.PseudoFunctors.Examples.OpFunctor

The opposite of a category as a pseudofunctor *********************************************************************************
Require Import UniMath.Foundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.Core.Examples.OpCellBicat.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.

Local Open Scope cat.

Local Notation "∁" := bicat_of_univ_cats.

Definition op_psfunctor_data : psfunctor_data (op2_bicat ∁) ∁.
Show proof.
  use make_psfunctor_data.
  - exact (λ C, op_unicat C).
  - exact (λ _ _ f, functor_opp f).
  - exact (λ _ _ _ _ x, op_nt x).
  - exact (λ C, functor_identity_op _).
  - exact (λ _ _ _ F G, functor_comp_op F G).

Definition op_psfunctor_laws : psfunctor_laws op_psfunctor_data.
Show proof.
  repeat split.
  - intros C D F. cbn in *.
    apply nat_trans_eq; [apply (homset_property (op_cat D) )|].
    intro. apply idpath.
  - intros C D F G H α β ; cbn in *.
    apply nat_trans_eq ; [apply (homset_property (op_cat D) )|].
    intro x ; cbn in *.
    apply idpath.
  - intros C D F. cbn in *.
    apply nat_trans_eq; [apply (homset_property (op_cat D) )|].
    intro. cbn. apply pathsinv0.
    rewrite !id_left.
    apply functor_id.
  - intros C D F. cbn in *.
    apply nat_trans_eq; [apply (homset_property (op_cat D) )|].
    intro. cbn. apply pathsinv0.
    rewrite id_left. rewrite id_right. apply idpath.
  - intros C1 C2 C3 C4 F G H. cbn in *.
    apply nat_trans_eq; [apply (homset_property (op_cat C4) )|].
    intro. cbn. apply pathsinv0.
    rewrite id_left. rewrite !id_right.
    rewrite functor_id.
    apply idpath.
  - intros C1 C2 C3 F G H alpha. cbn in *.
    apply nat_trans_eq; [apply (homset_property (op_cat C3) )|].
    intro. cbn. apply pathsinv0.
    rewrite id_left. rewrite id_right.
    apply idpath.
  - intros C1 C2 C3 F1 F2 F3 α ; cbn in *.
    apply nat_trans_eq; [apply (homset_property (op_cat C3) )|].
    intros x ; cbn.
    rewrite id_left, id_right.
    apply idpath.

Definition op_psfunctor_invertible_cells
  : invertible_cells op_psfunctor_data.
Show proof.
  split.
  - intro C.
    use is_nat_z_iso_to_is_invertible_2cell.
    apply is_nat_z_iso_functor_identity_op.
  - intros C₁ C₂ C₃ F G.
    use is_nat_z_iso_to_is_invertible_2cell.
    apply is_nat_z_iso_functor_comp_op.

Definition op_psfunctor : psfunctor (op2_bicat ∁) ∁.
Show proof.
  use make_psfunctor.
  - exact op_psfunctor_data.
  - exact op_psfunctor_laws.
  - exact op_psfunctor_invertible_cells.