Library UniMath.Bicategories.DisplayedBicats.DispPseudofunctor

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.DisplayedCats.Auxiliary.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.Initial.
Require Import UniMath.Bicategories.Core.Examples.Final.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles.
Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions.
Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.
Require Import UniMath.Bicategories.DisplayedBicats.Fibration.
Require Import UniMath.Bicategories.DisplayedBicats.FiberCategory.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity.
Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.
Import PseudoFunctor.Notations.

Local Open Scope cat.

Section DispPseudofunctor.

Context {B₁ : bicat} (D₁ : disp_bicat B₁)
        {B₂ : bicat} (D₂ : disp_bicat B₂)
        (F : psfunctor B₁ B₂).

Definition disp_psfunctor_data : UU
  :=
    ∑ (obFF : ∏ x:B₁, D₁ x → D₂ (F x))
      (morFF : ∏ (x y : B₁) (f : B₁⟦x,y⟧) (xx : D₁ x) (yy : D₁ y),
               (xx -->[f] yy) →
               (obFF x xx -->[#F f] obFF y yy))
      (cellFF : ∏ (x y : B₁) (f g : B₁⟦x,y⟧) (α : f ==> g) (xx : D₁ x) (yy : D₁ y)
                  (ff : xx -->[f] yy) (gg : xx -->[g] yy),
                (ff ==>[α] gg) → (morFF x y f xx yy ff ==>[##F α] morFF x y g xx yy gg))
      (disp_psfunctor_id : ∏ (x : B₁) (xx : D₁ x),
                           disp_invertible_2cell
                             (psfunctor_id F x)
                             (id_disp (obFF x xx))
                             (morFF x x (id₁ x) xx xx (id_disp xx))),
    (∏ (x y z : B₁) (f : x --> y) (g : y --> z)
       (xx : D₁ x) (yy : D₁ y) (zz : D₁ z)
       (ff : xx -->[f] yy) (gg : yy -->[g] zz),
     disp_invertible_2cell
       (psfunctor_comp F f g)
       (comp_disp (morFF x y f xx yy ff) (morFF y z g yy zz gg))
       (morFF x z (f · g) xx zz (comp_disp ff gg))).

Definition make_disp_psfunctor_data
           (obFF : ∏ x:B₁, D₁ x → D₂ (F x))
           (morFF : ∏ (x y : B₁) (f : B₁⟦x,y⟧) (xx : D₁ x) (yy : D₁ y),
                    (xx -->[f] yy) →
                    (obFF x xx -->[#F f] obFF y yy))
           (cellFF : ∏ (x y : B₁) (f g : B₁⟦x,y⟧) (α : f ==> g) (xx : D₁ x) (yy : D₁ y)
                       (ff : xx -->[f] yy) (gg : xx -->[g] yy),
                     (ff ==>[α] gg) → (morFF x y f xx yy ff ==>[##F α] morFF x y g xx yy gg))
           (disp_psfunctor_id : ∏ (x : B₁) (xx : D₁ x),
                                disp_invertible_2cell
                                  (psfunctor_id F x)
                                  (id_disp (obFF x xx))
                                  (morFF x x (id₁ x) xx xx (id_disp xx)))
           (disp_psfunctor_comp : ∏ (x y z : B₁) (f : x --> y) (g : y --> z)
                                    (xx : D₁ x) (yy : D₁ y) (zz : D₁ z)
                                    (ff : xx -->[f] yy) (gg : yy -->[g] zz),
                                  disp_invertible_2cell
                                    (psfunctor_comp F f g)
                                    (comp_disp (morFF x y f xx yy ff) (morFF y z g yy zz gg))
                                    (morFF x z (f · g) xx zz (comp_disp ff gg)))
  : disp_psfunctor_data
  := (obFF,, morFF,, cellFF,, disp_psfunctor_id,, disp_psfunctor_comp).

Definition disp_psfunctor_ob (FFdata : disp_psfunctor_data)
           {x : B₁}
           (xx : D₁ x)
  : D₂ (F x)
  := pr1 FFdata x xx.

Coercion disp_psfunctor_ob : disp_psfunctor_data >-> Funclass.

Section Projections.

Variable (FFdata : disp_psfunctor_data).

Definition disp_psfunctor_mor
           {x y : B₁} {f : B₁⟦x,y⟧} {xx : D₁ x} {yy : D₁ y}
           (ff : xx -->[f] yy)
  : FFdata x xx -->[#F f] FFdata y yy
  := pr12 FFdata x y f xx yy ff.

Definition disp_psfunctor_cell {x y : B₁} {f g : B₁⟦x,y⟧} {α : f ==> g}
           {xx : D₁ x} {yy : D₁ y}
           {ff : xx -->[f] yy} {gg : xx -->[g] yy}
           (αα : ff ==>[α] gg)
  : disp_psfunctor_mor ff ==>[##F α] disp_psfunctor_mor gg
  := pr122 FFdata x y f g α xx yy ff gg αα.

Definition disp_psfunctor_id {x : B₁} (xx : D₁ x)
  : disp_invertible_2cell (psfunctor_id F x)
                          (id_disp (FFdata x xx))
                          (disp_psfunctor_mor (id_disp xx))
  := pr122 (pr2 FFdata) x xx.

Definition disp_psfunctor_comp
           {x y z : B₁} {f : x --> y} {g : y --> z}
           {xx : D₁ x} {yy : D₁ y} {zz : D₁ z}
           (ff : xx -->[f] yy) (gg : yy -->[g] zz)
  : disp_invertible_2cell (psfunctor_comp F f g)
                          (comp_disp (disp_psfunctor_mor ff) (disp_psfunctor_mor gg))
                          (disp_psfunctor_mor (comp_disp ff gg))
  := pr222 (pr2 FFdata) x y z f g xx yy zz ff gg.

End Projections.

Definition total_psfunctor_data (FFdata : disp_psfunctor_data)
  : psfunctor_data (total_bicat D₁) (total_bicat D₂).
Proof.
  use make_psfunctor_data.
  - exact (λ x, (F (pr1 x),, FFdata _ (pr2 x))).
  - exact (λ x y f, (#F (pr1 f) ,, disp_psfunctor_mor FFdata (pr2 f))).
  - exact (λ x y f g α, (##F (pr1 α),, disp_psfunctor_cell FFdata (pr2 α))).
  - exact (λ x, iso_in_E_weq _ _ (psfunctor_id F (pr1 x),, disp_psfunctor_id FFdata (pr2 x))).
  - refine (λ x y z f g, iso_in_E_weq _ _ _).
    exact (psfunctor_comp F (pr1 f) (pr1 g),, disp_psfunctor_comp FFdata (pr2 f) (pr2 g)).
Defined.

Section DispPseudofunctorLaws.

Variable FFdata : disp_psfunctor_data.

Definition disp_psfunctor_id2_law
  : UU
  := ∏ (a b : B₁) (f : a --> b)
       (aa : D₁ a)
       (bb : D₁ b)
       (ff : aa -->[f] bb),
     disp_psfunctor_cell FFdata (disp_id2 ff) =
     transportb
       (λ p : # F f ==> # F f, disp_psfunctor_mor FFdata ff ==>[p] disp_psfunctor_mor FFdata ff)
       (psfunctor_id2 F f) (disp_id2 (disp_psfunctor_mor FFdata ff)).

Definition disp_psfunctor_vcomp2_law : UU
  := ∏ (a b : B₁) (f g h : B₁ ⟦a, b⟧) (η : f ==> g) (φ : g ==> h) (aa : D₁ a)
       (bb : D₁ b) (ff : aa -->[f] bb) (gg : aa -->[g] bb) (hh : aa -->[h] bb)
       (ηη : ff ==>[η] gg) (φφ : gg ==>[φ] hh),
     disp_psfunctor_cell FFdata (ηη •• φφ) =
     transportb
       (λ p : # F f ==> # F h, disp_psfunctor_mor FFdata ff ==>[ p] disp_psfunctor_mor FFdata hh)
       (psfunctor_vcomp F η φ) (disp_psfunctor_cell FFdata ηη •• disp_psfunctor_cell FFdata φφ).

Definition disp_psfunctor_lunitor_law : UU
  := ∏ (a b : B₁) (f : B₁ ⟦ a, b ⟧) (aa : D₁ a) (bb : D₁ b) (ff : aa -->[ f] bb),
     disp_lunitor (disp_psfunctor_mor FFdata ff) =
     transportb
       (λ p, _ ==>[p] _)
       (psfunctor_lunitor F f)
       (((disp_psfunctor_id FFdata aa ▹▹ disp_psfunctor_mor FFdata ff)
           •• disp_psfunctor_comp FFdata (id_disp aa) ff)
          •• disp_psfunctor_cell FFdata (disp_lunitor ff)).

Definition disp_psfunctor_runitor_law : UU
  := ∏ (a b : B₁) (f : B₁ ⟦ a, b ⟧) (aa : D₁ a) (bb : D₁ b) (ff : aa -->[ f] bb),
     disp_runitor (disp_psfunctor_mor FFdata ff) =
     transportb
       (λ p, _ ==>[p] _)
       (psfunctor_runitor F f)
       (((disp_psfunctor_mor FFdata ff ◃◃ disp_psfunctor_id FFdata _)
           •• disp_psfunctor_comp FFdata _ _)
          •• disp_psfunctor_cell FFdata (disp_runitor ff)).

Definition disp_psfunctor_lassociator_law : UU
  :=
    ∏ (a b c d : B₁) (f : B₁ ⟦ a, b ⟧) (g : B₁ ⟦ b, c ⟧) (h : B₁ ⟦ c, d ⟧)
      (aa : D₁ a) (bb : D₁ b) (cc : D₁ c) (dd : D₁ d) (ff : aa -->[ f] bb) (gg : bb -->[ g] cc)
      (hh : cc -->[ h] dd),
    ((disp_psfunctor_mor FFdata ff ◃◃ disp_psfunctor_comp FFdata gg hh)
       •• disp_psfunctor_comp FFdata ff (gg;; hh))
      •• disp_psfunctor_cell FFdata (disp_lassociator ff gg hh) =
    transportb
      (λ p, _ ==>[p] _)
      (psfunctor_lassociator F f g h)
      ((disp_lassociator (disp_psfunctor_mor FFdata ff) (disp_psfunctor_mor FFdata gg)
                         (disp_psfunctor_mor FFdata hh)
         •• (disp_psfunctor_comp FFdata ff gg ▹▹ disp_psfunctor_mor FFdata hh))
        •• disp_psfunctor_comp FFdata (ff;; gg) hh).

Definition disp_psfunctor_lwhisker_law : UU
  := ∏ (a b c : B₁) (f : B₁ ⟦ a, b ⟧) (g₁ g₂ : B₁ ⟦ b, c ⟧) (η : g₁ ==> g₂)
       (aa : D₁ a) (bb : D₁ b) (cc : D₁ c) (ff : aa -->[ f] bb) (gg₁ : bb -->[ g₁] cc)
       (gg₂ : bb -->[ g₂] cc) (ηη : gg₁ ==>[ η] gg₂),
     disp_psfunctor_comp FFdata ff gg₁ •• disp_psfunctor_cell FFdata (ff ◃◃ ηη) =
     transportb
       (λ p, _ ==>[p] _)
       (psfunctor_lwhisker F f η)
       ((disp_psfunctor_mor FFdata ff ◃◃ disp_psfunctor_cell FFdata ηη)
          •• disp_psfunctor_comp FFdata ff gg₂).

Definition disp_psfunctor_rwhisker_law : UU
  := ∏ (a b c : B₁) (f₁ f₂ : B₁ ⟦ a, b ⟧) (g : B₁ ⟦ b, c ⟧) (η : f₁ ==> f₂)
       (aa : D₁ a) (bb : D₁ b) (cc : D₁ c)
       (ff₁ : aa -->[f₁] bb)
       (ff₂ : aa -->[f₂] bb)
       (gg : bb -->[g] cc)
       (ηη : ff₁ ==>[ η] ff₂),
     disp_psfunctor_comp FFdata _ _ •• disp_psfunctor_cell FFdata (ηη ▹▹ gg) =
     transportb
       (λ p, _ ==>[p] _)
       (psfunctor_rwhisker F g η)
       ((disp_psfunctor_cell FFdata ηη ▹▹ _)
          •• disp_psfunctor_comp FFdata _ _).

Definition is_disp_psfunctor : UU
    := disp_psfunctor_id2_law
         × disp_psfunctor_vcomp2_law
         × disp_psfunctor_lunitor_law
         × disp_psfunctor_runitor_law
         × disp_psfunctor_lassociator_law
         × disp_psfunctor_lwhisker_law
         × disp_psfunctor_rwhisker_law.

Definition disp_psfunctor_id2 (H : is_disp_psfunctor) := pr1 H.

Definition disp_psfunctor_vcomp2 (H : is_disp_psfunctor) := pr12 H.

Definition disp_psfunctor_vcomp2_alt (H : is_disp_psfunctor)
           (a b : B₁) (f g h : B₁ ⟦a, b⟧) (η : f ==> g) (φ : g ==> h) (aa : D₁ a)
           (bb : D₁ b) (ff : aa -->[f] bb) (gg : aa -->[g] bb) (hh : aa -->[h] bb)
           (ηη : ff ==>[η] gg) (φφ : gg ==>[φ] hh)
  : transportf
      (λ p : # F f ==> # F h, disp_psfunctor_mor FFdata ff ==>[ p] disp_psfunctor_mor FFdata hh)
      (psfunctor_vcomp F η φ)
      (disp_psfunctor_cell FFdata (ηη •• φφ)) =
    disp_psfunctor_cell FFdata ηη •• disp_psfunctor_cell FFdata φφ.
Proof.
  refine (transportf_transpose_left (P := λ p, _ ==>[p] _) _).
  apply (disp_psfunctor_vcomp2 H).
Qed.

End DispPseudofunctorLaws.

Definition disp_psfunctor : UU
  := ∑ FF : disp_psfunctor_data, is_disp_psfunctor FF.

Coercion disp_psfunctor_to_disp_psfunctor_data (FF : disp_psfunctor)
  : disp_psfunctor_data
  := pr1 FF.

Lemma total_psfunctor_laws (FF : disp_psfunctor)
  : psfunctor_laws (total_psfunctor_data FF).
Proof.
  repeat apply make_dirprod; intro; intros; (use total2_paths_b; [ apply F | apply FF ]).
Qed.

Definition total_psfunctor (FF : disp_psfunctor)
  : psfunctor (total_bicat D₁) (total_bicat D₂).
Proof.
  use make_psfunctor.
  - exact (total_psfunctor_data FF).
  - exact (total_psfunctor_laws FF).
  - split; intros; use iso_in_E_weq.
Defined.

Definition is_disp_psfunctor_from_total (FF : disp_psfunctor_data)
  : is_psfunctor (total_psfunctor_data FF) → is_disp_psfunctor FF.
Proof.
  intros HFF.
  pose (EF := make_psfunctor _ (pr1 HFF) (pr2 HFF)).
  repeat split.
  - intros a b f aa bb ff.
    pose (P := !fiber_paths (@psfunctor_id2 _ _ EF (a,,aa) (b,,bb) (f,,ff))).
    symmetry.
    etrans. { apply maponpaths. exact P. }
    unfold transportb.
    rewrite transport_f_f.
    rewrite transportf_set.
    × apply idpath.
    × apply B₂.
  - intros a b f g h η φ aa bb ff gg hh ηη φφ.
    pose (P := !fiber_paths (@psfunctor_vcomp _ _ EF
                                              (a,,aa) (b,,bb) (f,,ff) (g,,gg) (h,,hh)
                                              (η,,ηη) (φ,,φφ))).
    cbn in P; rewrite P.
    unfold transportb.
    rewrite transport_f_f.
    rewrite transportf_set.
    × apply idpath.
    × apply B₂.
  - intros a b f aa bb ff.
    pose (P := !fiber_paths (@psfunctor_lunitor _ _
                                                EF (a,,aa) (b,,bb) (f,,ff))).
    symmetry.
    etrans. { apply maponpaths. exact P. }
    unfold transportb.
    rewrite transport_f_f.
    rewrite transportf_set.
    × apply idpath.
    × apply B₂.
  - intros a b f aa bb ff.
    pose (P := !fiber_paths (@psfunctor_runitor _ _
                                                EF (a,,aa) (b,,bb) (f,,ff))).
    symmetry.
    etrans. { apply maponpaths. exact P. }
    unfold transportb.
    rewrite transport_f_f.
    rewrite transportf_set.
    × apply idpath.
    × apply B₂.
  - intros a b c d f g h aa bb cc dd ff gg hh.
    pose (P := !fiber_paths (@psfunctor_lassociator _ _
                                                    EF (a,,aa) (b,,bb) (c,,cc) (d,,dd)
                                                    (f,,ff) (g,,gg) (h,,hh))).
    symmetry.
    etrans. { apply maponpaths. exact P. }
    unfold transportb.
    rewrite transport_f_f.
    rewrite transportf_set.
    × apply idpath.
    × apply B₂.
  - intros a b c f g1 g2 η aa bb cc ff gg1 gg2 ηη.
    pose (P := !fiber_paths (@psfunctor_lwhisker _ _
                                                 EF (a,,aa) (b,,bb) (c,,cc)
                                                 (f,,ff) (g1,,gg1) (g2,,gg2) (η,,ηη))).
    symmetry.
    etrans. { apply maponpaths. exact P. }
    unfold transportb.
    rewrite transport_f_f.
    rewrite transportf_set.
    × apply idpath.
    × apply B₂.
  - intros a b c f1 f2 g η aa bb cc ff1 ff2 gg ηη.
    pose (P := !fiber_paths (@psfunctor_rwhisker _ _ EF (a,,aa) (b,,bb) (c,,cc)
                                                 (f1,,ff1) (f2,,ff2) (g,,gg) (η,,ηη))).
    symmetry.
    etrans. { apply maponpaths. exact P. }
    unfold transportb.
    rewrite transport_f_f.
    rewrite transportf_set.
    × apply idpath.
    × apply B₂.
Qed.

End DispPseudofunctor.

Section DispPseudofunctor_identity.

Context {B : bicat} (D : disp_bicat B).

Definition disp_pseudo_id_data : disp_psfunctor_data D D (id_psfunctor B).
Proof.
  use make_disp_psfunctor_data; cbn.
  - exact (λ _ y, y).
  - exact (λ _ _ _ _ _ ff, ff).
  - exact (λ _ _ _ _ _ _ _ _ _ αα, αα).
  - intros. apply disp_id2_invertible_2cell.
  - intros. apply disp_id2_invertible_2cell.
Defined.

Lemma disp_pseudo_id_laws : is_disp_psfunctor D D _ disp_pseudo_id_data.
Proof.
  apply is_disp_psfunctor_from_total.
  apply id_psfunctor.
Qed.

Definition disp_pseudo_id : disp_psfunctor D D (id_psfunctor B)
  := disp_pseudo_id_data,, disp_pseudo_id_laws.

End DispPseudofunctor_identity.

Definition disp_psfunctor_cell_transportb
           {B₁ B₂ : bicat}
           {F : psfunctor B₁ B₂}
           {D₁ : disp_bicat B₁}
           {D₂ : disp_bicat B₂}
           (FF : disp_psfunctor D₁ D₂ F)
           {x y : B₁}
           {f : x --> y}
           {φ ψ : f ==> f}
           {xx : D₁ x}
           {yy : D₁ y}
           {ff : xx -->[f] yy}
           (p : φ = ψ)
           (ψψ : ff ==>[ ψ ] ff)
  : disp_psfunctor_cell
      _ _ _ (pr1 FF)
      (transportb (λ z, ff ==>[ z ] ff) p ψψ)
    =
    transportb
      (λ z, _ ==>[ z ] _)
      (maponpaths (λ z, ##F z) p)
      (disp_psfunctor_cell
         _ _ _ (pr1 FF)
         ψψ).
Proof.
  induction p.
  cbn.
  apply idpath.
Defined.

Section DispPseudofunctorInvertible_2cell.

Context {B₁ B₂ : bicat}
        {F : psfunctor B₁ B₂}
        {D₁ : disp_bicat B₁}
        {D₂ : disp_bicat B₂}
        (FF : disp_psfunctor D₁ D₂ F)
        {x y : B₁}
        {f g : x --> y}
        {α : invertible_2cell f g}
        {xx : D₁ x}
        {yy : D₁ y}
        {ff : xx -->[f] yy}
        {gg : xx -->[g] yy}
        (αα : disp_invertible_2cell α ff gg).

Definition disp_psfunctor_invertible_2cell
  : disp_invertible_2cell
      (_,, psfunctor_is_iso F α)
      (disp_psfunctor_mor _ _ _ FF ff)
      (disp_psfunctor_mor _ _ _ FF gg).
Proof.
  repeat use tpair; cbn.
  - exact (disp_psfunctor_cell _ _ _ FF αα).
  - exact (disp_psfunctor_cell _ _ _ FF (disp_inv_cell αα)).
  - abstract
      (rewrite <- (disp_psfunctor_vcomp2_alt _ _ _ _ (pr2 FF));
       rewrite disp_vcomp_rinv;
       rewrite disp_psfunctor_cell_transportb;
       unfold transportb;
       rewrite transport_f_f;
       rewrite (disp_psfunctor_id2 _ _ _ _ (pr2 FF));
       unfold transportb;
       rewrite transport_f_f;
       apply (@transportf_paths _ (λ p, _ ==>[ p ] _));
       apply B₂).
  - abstract
      (rewrite <- (disp_psfunctor_vcomp2_alt _ _ _ _ (pr2 FF));
       rewrite disp_vcomp_linv;
       rewrite disp_psfunctor_cell_transportb;
       unfold transportb;
       rewrite transport_f_f;
       rewrite (disp_psfunctor_id2 _ _ _ _ (pr2 FF));
       unfold transportb;
       rewrite transport_f_f;
       apply (@transportf_paths _ (λ p, _ ==>[ p ] _));
       apply B₂).
Defined.

End DispPseudofunctorInvertible_2cell.

Section DispPseudofunctor_comp.

Context {B₁ B₂ B₃ : bicat}
        (F₁ : psfunctor B₁ B₂)
        (F₂ : psfunctor B₂ B₃)
        (D₁ : disp_bicat B₁)
        (D₂ : disp_bicat B₂)
        (D₃ : disp_bicat B₃)
        (FF₁ : disp_psfunctor D₁ D₂ F₁)
        (FF₂ : disp_psfunctor D₂ D₃ F₂).

Definition disp_pseudo_comp_data : disp_psfunctor_data D₁ D₃ (comp_psfunctor F₂ F₁).
Proof.
  use make_disp_psfunctor_data; cbn.
  - exact (λ x xx, FF₂ _ (FF₁ _ xx)).
  - exact (λ x y f xx yy ff, disp_psfunctor_mor _ _ _ FF₂ (disp_psfunctor_mor _ _ _ FF₁ ff)).
  - exact (λ x y f g α xx yy ff gg αα, disp_psfunctor_cell _ _ _ FF₂ (disp_psfunctor_cell _ _ _ FF₁ αα)).
  - intros x xx.
    exact (vcomp_disp_invertible
             (disp_psfunctor_id _ _ _ FF₂ (FF₁ _ xx))
             (disp_psfunctor_invertible_2cell FF₂ (disp_psfunctor_id _ _ _ FF₁ xx))).
  - intros x y z f g xx yy zz ff gg.
    exact (vcomp_disp_invertible
             (disp_psfunctor_comp _ _ _ FF₂
                                  (disp_psfunctor_mor _ _ _ FF₁ ff)
                                  (disp_psfunctor_mor _ _ _ FF₁ gg))
             (disp_psfunctor_invertible_2cell FF₂ (disp_psfunctor_comp _ _ _ FF₁ ff gg))).
Defined.

Lemma disp_pseudo_comp_laws : is_disp_psfunctor _ _ _ disp_pseudo_comp_data.
Proof.
  apply is_disp_psfunctor_from_total.
  apply (comp_psfunctor (total_psfunctor _ _ _ FF₂) (total_psfunctor _ _ _ FF₁)).
Qed.

Definition disp_pseudo_comp : disp_psfunctor _ _ (comp_psfunctor F₂ F₁)
  := disp_pseudo_comp_data,, disp_pseudo_comp_laws.

End DispPseudofunctor_comp.

Local Open Scope mor_disp_scope.

Definition transportb_disp_psfunctor
           {C : bicat}
           (HC : is_univalent_2_1 C)
           (D₁ : disp_bicat C)
           (D₂ : disp_bicat C)
           (F : disp_psfunctor D₁ D₂ (id_psfunctor C))
           {x y : C}
           {f g : x --> y}
           {xx : D₁ x} {yy : D₁ y}
           (ff : xx -->[ f ] yy)
           (p : g = f)
  : transportb
      (mor_disp ((pr11 F) x xx) ((pr11 F) y yy)) p
      ((pr121 F) _ _ _ xx yy ff)
    =
    (pr121 F)
      x y g xx yy
      (transportb (mor_disp xx yy) p ff).
Proof.
  induction p.
  apply idpath.
Defined.

Section FiberOfFunctor.
  Context {C : bicat}
          (HC : is_univalent_2_1 C)
          {D₁ : disp_bicat C}
          (HD₁ : disp_2cells_isaprop D₁)
          (HD₁_2_1 : disp_univalent_2_1 D₁)
          (h₁ : local_iso_cleaving D₁)
          {D₂ : disp_bicat C}
          (HD₂ : disp_2cells_isaprop D₂)
          (HD₂_2_1 : disp_univalent_2_1 D₂)
          (h₂ : local_iso_cleaving D₂)
          (F : disp_psfunctor D₁ D₂ (id_psfunctor C)).

  Definition fiber_functor_data
             (c : C)
    : functor_data
        (discrete_fiber_category D₁ HD₁ HD₁_2_1 h₁ c)
        (discrete_fiber_category D₂ HD₂ HD₂_2_1 h₂ c).
  Proof.
    use make_functor_data.
    - exact (pr11 F c).
    - exact (pr121 F c c (id₁ c)).
  Defined.

  Definition fiber_is_functor
             (c : C)
    : is_functor (fiber_functor_data c).
  Proof.
    split.
    - intros x.
      exact (!(disp_isotoid_2_1 _ HD₂_2_1 (idpath _) _ _ (pr12 (pr221 F) c x))).
    - intros x y z f g ; cbn.
      pose ((disp_isotoid_2_1
               _
               HD₂_2_1 (idpath _)
               _ _
               (pr22 (pr221 F) c c c (id₁ c) (id₁ c) x y z f g))) as p.
      cbn in p.
      rewrite p ; clear p.
      pose (disp_local_iso_cleaving_invertible_2cell
              h₂
              ((pr121 F) c c (id₁ c · id₁ c) x z (f;; g))
              (idempunitor c)) as p1.
      pose (disp_local_iso_cleaving_invertible_2cell h₁ (f;; g) (idempunitor c)) as p2.
      rewrite <- (idtoiso_2_1_isotoid_2_1 HC (idempunitor c)) in p1, p2.
      etrans.
      {
        apply maponpaths.
        pose (transportb_transpose_right (disp_isotoid_2_1 D₁ HD₁_2_1 _ _ _ p2)) as p.
        rewrite idtoiso_2_1_isotoid_2_1 in p.
        exact p.
      }
      clear p2.
      refine (!_).
      etrans.
      {
        pose (transportb_transpose_right (disp_isotoid_2_1 D₂ HD₂_2_1 _ _ _ p1)) as p.
        rewrite idtoiso_2_1_isotoid_2_1 in p.
        exact p.
      }
      clear p1.
      apply transportb_disp_psfunctor.
      exact HC.
  Qed.

  Definition fiber_functor
             (c : C)
    : discrete_fiber_category D₁ HD₁ HD₁_2_1 h₁ c
      ⟶
      discrete_fiber_category D₂ HD₂ HD₂_2_1 h₂ c.
  Proof.
    use make_functor.
    - exact (fiber_functor_data c).
    - exact (fiber_is_functor c).
  Defined.
End FiberOfFunctor.