Library UniMath.CategoryTheory.DisplayedCats.Isos


Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.

Local Open Scope cat.
Local Open Scope mor_disp_scope.

Isomorphisms (and lemmas)


Section Isos.

  Definition is_disp_inverse {C : precategory} {D : disp_cat_data C} {x y : C}
    {f : x --> y} {g: y --> x} (isinv: is_inverse_in_precat f g)
    {xx : D x} {yy : D y} (ff : xx -->[f] yy) (gg : yy -->[g] xx) : UU
    := gg ;; ff = transportb _ (pr2 isinv) (id_disp yy) ×
                    ff ;; gg = transportb _ (pr1 isinv) (id_disp xx).

  Definition is_z_iso_disp {C : precategory} {D : disp_cat_data C}
             {x y : C} (f : z_iso x y) {xx : D x} {yy} (ff : xx -->[f] yy) : UU
    := ∑ (gg : yy -->[inv_from_z_iso f] xx),
      is_disp_inverse (z_iso_is_inverse_in_precat f) ff gg.

  Definition z_iso_disp {C : precategory} {D : disp_cat_data C}
             {x y : C} (f : z_iso x y) (xx : D x) (yy : D y)
    := ∑ ff : xx -->[f] yy, is_z_iso_disp f ff.

  Definition make_z_iso_disp {C : precategory} {D : disp_cat_data C}
             {x y : C} {f : z_iso x y} {xx : D x} {yy : D y}
             (ff : xx -->[f] yy) (is : is_z_iso_disp f ff)
    : z_iso_disp _ _ _
    := (ff,, is).

  Definition mor_disp_from_z_iso {C : precategory} {D : disp_cat_data C}
             {x y : C} {f : z_iso x y}{xx : D x} {yy : D y}
             (i : z_iso_disp f xx yy) : _ -->[ _ ] _ := pr1 i.
  Coercion mor_disp_from_z_iso : z_iso_disp >-> mor_disp.

  Definition is_z_iso_disp_from_z_iso {C : precategory} {D : disp_cat_data C}
             {x y : C} {f : z_iso x y}{xx : D x} {yy : D y}
             (i : z_iso_disp f xx yy) : is_z_iso_disp f i := pr2 i.
  Coercion is_z_iso_disp_from_z_iso : z_iso_disp >-> is_z_iso_disp.

  Definition inv_mor_disp_from_z_iso {C : precategory} {D : disp_cat_data C}
             {x y : C} {f : z_iso x y}{xx : D x} {yy : D y}
             {ff : xx -->[f] yy} (i : is_z_iso_disp f ff)
    : _ -->[ _ ] _ := pr1 i.

  Definition z_iso_disp_after_inv_mor {C : precategory} {D : disp_cat_data C}
             {x y : C} {f : z_iso x y}{xx : D x} {yy : D y}
             {ff : xx -->[f] yy} (i : is_z_iso_disp f ff)
    : inv_mor_disp_from_z_iso i ;; ff
      = transportb _ (z_iso_after_z_iso_inv _) (id_disp _).
  Show proof.
    apply (pr2 i).

  Definition inv_mor_after_z_iso_disp {C : precategory} {D : disp_cat_data C}
             {x y : C} {f : z_iso x y}{xx : D x} {yy : D y}
             {ff : xx -->[f] yy} (i : is_z_iso_disp f ff)
    : ff ;; inv_mor_disp_from_z_iso i
      = transportb _ (z_iso_inv_after_z_iso _) (id_disp _).
  Show proof.
    apply (pr2 (pr2 i)).

  Lemma isaprop_is_disp_inverse {C : category} {D : disp_cat C} {x y : C}
    (f : x --> y) (g: y --> x) (isinv: is_inverse_in_precat f g)
    {xx : D x} {yy : D y} (ff : xx -->[f] yy) (gg : yy -->[g] xx)
    : isaprop (is_disp_inverse isinv ff gg).
  Show proof.
    apply isapropdirprod; apply homsets_disp.

  Lemma isaprop_is_z_iso_disp {C : category} {D : disp_cat C}
        {x y : C} (f : z_iso x y) {xx : D x} {yy} (ff : xx -->[f] yy)
    : isaprop (is_z_iso_disp f ff).
  Show proof.
    apply invproofirrelevance; intros i i'.
    apply subtypePath.
    - intros gg. apply isaprop_is_disp_inverse.
    - destruct i as [gg [gf fg]], i' as [gg' [gf' fg']]; simpl.
      etrans. eapply pathsinv0, transportfbinv.
      etrans. apply maponpaths, @pathsinv0, id_right_disp.
      etrans. apply maponpaths, maponpaths.
      etrans. eapply pathsinv0, transportfbinv.
      apply maponpaths, @pathsinv0, fg'.
      etrans. apply maponpaths, mor_disp_transportf_prewhisker.
      etrans. apply transport_f_f.
      etrans. apply maponpaths, assoc_disp.
      etrans. apply transport_f_f.
      etrans. apply maponpaths, maponpaths_2, gf.
      etrans. apply maponpaths, mor_disp_transportf_postwhisker.
      etrans. apply transport_f_f.
      etrans. apply maponpaths, id_left_disp.
      etrans. apply transport_f_f.
      use (@maponpaths_2 _ _ _ (transportf _) _ (idpath _)).
      apply homset_property.

  Lemma isaset_z_iso_disp {C : category} {D : disp_cat C}
        {x y} (f : z_iso x y) (xx : D x) (yy : D y)
    : isaset (z_iso_disp f xx yy).
  Show proof.
    apply isaset_total2.
    - apply homsets_disp.
    - intros. apply isasetaprop, isaprop_is_z_iso_disp.

  Lemma eq_z_iso_disp {C : category} {D : disp_cat C}
        {x y : C} (f : z_iso x y)
        {xx : D x} {yy} (ff ff' : z_iso_disp f xx yy)
    : pr1 ff = pr1 ff' -> ff = ff'.
  Show proof.
    apply subtypePath; intro; apply isaprop_is_z_iso_disp.

  Lemma is_z_iso_disp_transportf {C : category} {D : disp_cat C}
        {x y : C} {f f' : z_iso x y} (e : f = f')
        {xx : D x} {yy} {ff : xx -->[f] yy}
        (is : is_z_iso_disp _ ff)
    : is_z_iso_disp f' (transportf _ (maponpaths _ e) ff).
  Show proof.
    induction e.
    apply is.

  Lemma transportf_z_iso_disp {C : category} {D : disp_cat C}
        {x y : C} {xx : D x} {yy}
        {f f' : z_iso x y} (e : f = f')
        (ff : z_iso_disp f xx yy)
    : pr1 (transportf (λ g, z_iso_disp g _ _) e ff)
      = transportf _ (maponpaths pr1 e) (pr1 ff).
  Show proof.
    destruct e; apply idpath.

  Definition is_z_iso_inv_from_z_iso_disp {C : category} {D : disp_cat_data C}
             {x y : C} {f : z_iso x y}{xx : D x} {yy : D y}
             (i : z_iso_disp f xx yy)
    :
    is_z_iso_disp (z_iso_inv_from_z_iso f) (inv_mor_disp_from_z_iso i).
  Show proof.
    use tpair.
    - change ( xx -->[ z_iso_inv_from_z_iso (z_iso_inv_from_z_iso f)] yy).
      set (XR := transportb (mor_disp xx yy )
                            (maponpaths pr1 (z_iso_inv_z_iso_inv _ _ f))).
      apply XR. apply i.
    - cbn.
      split.
      + abstract (
            etrans ;[ apply mor_disp_transportf_postwhisker |];
            etrans ; [ apply maponpaths; apply (inv_mor_after_z_iso_disp i) | ];
            etrans ;[ apply transport_f_f |];
            apply transportf_comp_lemma; apply transportf_comp_lemma_hset;
            try apply homset_property; apply idpath ).
      + abstract (
            etrans ;[ apply mor_disp_transportf_prewhisker |];
            etrans ;[ apply maponpaths; apply (z_iso_disp_after_inv_mor i) |];
            etrans ;[ apply transport_f_f |];
            apply transportf_comp_lemma; apply transportf_comp_lemma_hset;
            try apply homset_property; apply idpath ).

  Definition is_z_iso_inv_from_is_z_iso_disp {C : category} {D : disp_cat_data C}
             {x y : C} {f : z_iso x y}{xx : D x} {yy : D y}
             (ff : xx -->[f] yy)
             (i : is_z_iso_disp f ff)
    :
    is_z_iso_disp (z_iso_inv_from_z_iso f) (inv_mor_disp_from_z_iso i).
  Show proof.
    apply (is_z_iso_inv_from_z_iso_disp (ff ,, i)).

  Definition z_iso_inv_from_z_iso_disp {C : category} {D : disp_cat_data C}
             {x y : C} {f : z_iso x y}{xx : D x} {yy : D y}
             (i : z_iso_disp f xx yy)
    :
    z_iso_disp (z_iso_inv_from_z_iso f) yy xx.
  Show proof.
    exists (inv_mor_disp_from_z_iso i).
    apply is_z_iso_inv_from_z_iso_disp.

  Definition z_iso_disp_comp {C : category} {D : disp_cat C}
             {x y z : C} {f : z_iso x y} {g : z_iso y z} {xx : D x} {yy : D y} {zz : D z}
             (ff : z_iso_disp f xx yy) (gg : z_iso_disp g yy zz)
    :
    z_iso_disp (z_iso_comp f g) xx zz.
  Show proof.
    use tpair.
    - apply (ff ;; gg).
    - use tpair.
      + apply (transportb (mor_disp zz xx) (maponpaths pr1 (z_iso_inv_of_z_iso_comp _ _ _ f g))).
        cbn.
        apply (inv_mor_disp_from_z_iso gg ;; inv_mor_disp_from_z_iso ff).
      + split.
        * etrans. apply mor_disp_transportf_postwhisker.
          etrans. apply maponpaths. apply assoc_disp_var.
          etrans. apply maponpaths, maponpaths, maponpaths.
          apply assoc_disp.
          etrans. apply maponpaths, maponpaths, maponpaths, maponpaths.
          eapply (maponpaths (λ x, x ;; gg)).
          apply z_iso_disp_after_inv_mor.
          etrans. apply transport_f_f.
          etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
          etrans. apply transport_f_f.
          etrans. apply maponpaths, maponpaths.
          apply mor_disp_transportf_postwhisker.
          etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
          etrans. apply transport_f_f.
          etrans. apply maponpaths, maponpaths. apply id_left_disp.
          etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
          etrans. apply transport_f_f.
          etrans. apply maponpaths. apply z_iso_disp_after_inv_mor.
          etrans. apply transport_f_f.
          apply transportf_comp_lemma; apply transportf_comp_lemma_hset;
            try apply homset_property; apply idpath.
        * cbn. simpl.
          etrans. apply assoc_disp_var.
          etrans. apply maponpaths, maponpaths.
          apply mor_disp_transportf_prewhisker.
          etrans. apply maponpaths, maponpaths, maponpaths.
          apply assoc_disp.
          etrans. apply maponpaths, maponpaths, maponpaths, maponpaths.
          eapply (maponpaths (λ x, x ;; inv_mor_disp_from_z_iso ff )).
          apply inv_mor_after_z_iso_disp.
          etrans. apply maponpaths, maponpaths, maponpaths, maponpaths.
          apply mor_disp_transportf_postwhisker.
          etrans. apply maponpaths, maponpaths, maponpaths, maponpaths, maponpaths.
          apply id_left_disp.
          etrans. apply maponpaths, maponpaths. apply transport_f_f.
          etrans. apply maponpaths, maponpaths. apply transport_f_f.
          etrans. apply maponpaths, maponpaths. apply transport_f_f.
          etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
          etrans. apply transport_f_f.
          etrans. apply maponpaths.
          apply inv_mor_after_z_iso_disp.
          etrans. apply transport_f_f.
          apply transportf_comp_lemma; apply transportf_comp_lemma_hset;
            try apply homset_property; apply idpath.

  Definition id_is_z_iso_disp {C} {D : disp_cat C} {x : C} (xx : D x)
    : is_z_iso_disp (identity_z_iso x) (id_disp xx).
  Show proof.
    exists (id_disp _); split.
    - etrans. apply id_left_disp.
      apply maponpaths_2, homset_property.
    - etrans. apply id_left_disp.
      apply maponpaths_2, homset_property.

  Definition identity_z_iso_disp {C} {D : disp_cat C} {x : C} (xx : D x)
    : z_iso_disp (identity_z_iso x) xx xx
    := (_ ,, id_is_z_iso_disp _).

  Lemma idtoiso_disp {C} {D : disp_cat C}
        {x x' : C} (e : x = x')
        {xx : D x} {xx' : D x'} (ee : transportf _ e xx = xx')
    : z_iso_disp (idtoiso e) xx xx'.
  Show proof.
    destruct e, ee; apply identity_z_iso_disp.

  Lemma idtoiso_fiber_disp {C} {D : disp_cat C} {x : C}
        {xx xx' : D x} (ee : xx = xx')
    : z_iso_disp (identity_z_iso x) xx xx'.
  Show proof.
    exact (idtoiso_disp (idpath _) ee).

  Lemma z_iso_disp_precomp {C : category} {D : disp_cat C}
        {x y : C} (f : z_iso x y)
        {xx : D x} {yy} (ff : z_iso_disp f xx yy)
    : forall (y' : C) (f' : y --> y') (yy' : D y'),
      isweq (fun ff' : yy -->[ f' ] yy' => pr1 ff ;; ff').
  Show proof.
    intros y' f' yy'.
    use isweq_iso.
    + intro X.
      set (XR := (pr1 (pr2 ff)) ;; X).
      set (XR' := transportf _ (assoc _ _ _ ) XR).
      set (XRRT := transportf _
                              (maponpaths (λ xyz, xyz · f') (z_iso_after_z_iso_inv f))
                              XR').
      set (XRRT' := transportf _ (id_left _ )
                               XRRT).
      apply XRRT'.
    + intros. simpl.
      etrans. apply transport_f_f.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply assoc_disp.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply maponpaths_2. apply (pr2 (pr2 ff)).
      etrans. apply maponpaths. apply mor_disp_transportf_postwhisker.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply id_left_disp.
      etrans. apply transport_f_f.
      apply transportf_comp_lemma_hset.
      apply C. apply idpath.
    + intros; simpl.
      etrans. apply maponpaths. apply transport_f_f.
      etrans. apply mor_disp_transportf_prewhisker.
      etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply assoc_disp.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply maponpaths_2.
      assert (XR := pr2 (pr2 (pr2 ff))). simpl in XR. apply XR.
      etrans. apply maponpaths. apply mor_disp_transportf_postwhisker.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply id_left_disp.
      etrans. apply transport_f_f.
      apply transportf_comp_lemma_hset.
      apply C. apply idpath.

  Lemma z_iso_disp_postcomp {C : category} {D : disp_cat C}
        {x y : C} (i : z_iso x y)
        {xx : D x} {yy} (ii : z_iso_disp i xx yy)
    : forall (x' : C) (f' : x' --> x) (xx' : D x'),
      isweq (fun ff : xx' -->[ f' ] xx => ff ;; ii)%mor_disp.
  Show proof.
    intros y' f' yy'.
    use isweq_iso.
    + intro X.
      set (XR := X ;; (pr1 (pr2 ii))).
      set (XR' := transportf (λ x, _ -->[ x ] _) (!assoc _ _ _ ) XR).
      set (XRRT := transportf (λ x, _ -->[ x ] _ )
                              (maponpaths (λ xyz, _ · xyz) (z_iso_inv_after_z_iso _ ))
                              XR').
      set (XRRT' := transportf _ (id_right _ )
                               XRRT).
      apply XRRT'.
    + intros. simpl.
      etrans. apply transport_f_f.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply assoc_disp_var.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply maponpaths. apply (pr2 (pr2 (pr2 ii))).
      etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply id_right_disp.
      etrans. apply transport_f_f.
      apply transportf_comp_lemma_hset.
      apply C. apply idpath.
    + intros; simpl.
      etrans. apply maponpaths_2. apply transport_f_f.
      etrans. apply mor_disp_transportf_postwhisker.
      etrans. apply maponpaths. apply mor_disp_transportf_postwhisker.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply assoc_disp_var.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply maponpaths.
      assert (XR := pr1 (pr2 (pr2 ii))). simpl in XR. apply XR.
      etrans. apply maponpaths. apply mor_disp_transportf_prewhisker.
      etrans. apply transport_f_f.
      etrans. apply maponpaths. apply id_right_disp.
      etrans. apply transport_f_f.
      apply transportf_comp_lemma_hset.
      apply C. apply idpath.

  Lemma is_z_iso_disp_independent_of_is_z_iso
        {C : category} {D : disp_cat_data C}
        {x y : C} (f : z_iso x y) {xx : D x} {yy} (ff : xx -->[f] yy)
        {H'f : is_z_isomorphism f} (Hff : is_z_iso_disp ((f : _ --> _),,H'f) ff)
    : is_z_iso_disp f ff.
  Show proof.
    destruct f as [F Hf].
    assert (E : Hf = H'f). apply isaprop_is_z_isomorphism.
    destruct E. exact Hff.

End Isos.

More utility lemmas

A few more general lemmas for displayed-cat algebra, that require isomorphisms to state.
Section Utilities.

Note: closely analogous to idtoiso_precompose. We name it differently to fit the convention of naming equalities according to their LHS, for reference during calculation.
  Lemma transportf_precompose_disp {C} {D : disp_cat C}
        {c d : C} (f : c --> d )
        {cc cc' : D c} (e : cc = cc') {dd} (ff : cc -->[f] dd)
    : transportf (λ xx : D c, xx -->[f] dd) e ff
      = transportf _ (id_left _)
                   (z_iso_inv_from_z_iso_disp (idtoiso_disp (idpath _) (e)) ;; ff).
  Show proof.
    destruct e; cbn.
    rewrite (@id_left_disp _ _ _ _ _ cc).
    apply pathsinv0, transportfbinv.


  Definition precomp_with_z_iso_disp_is_inj
             {C : category} {D : disp_cat C}
             {a b c : C} {i : z_iso a b} {f : b --> c}
             {aa : D a} {bb} {cc} (ii : z_iso_disp i aa bb) {ff ff' : bb -->[f] cc}
    : (ii ;; ff = ii ;; ff') -> ff = ff'.
  Show proof.
    intros e.
    use pathscomp0.
    - use (transportf _ _ ((z_iso_inv_from_z_iso_disp ii ;; ii) ;; ff)).
      etrans; [ apply maponpaths_2, z_iso_after_z_iso_inv | apply id_left ].
    - apply pathsinv0.
      etrans. eapply transportf_bind.
      eapply cancel_postcomposition_disp, (z_iso_disp_after_inv_mor ii).
      rewrite (@id_left_disp _ _ _ _ _ bb).
      etrans. apply transport_f_f.
      use (@maponpaths_2 _ _ _ _ _ (idpath _)).
      apply homset_property.
    - etrans. eapply transportf_bind, assoc_disp_var.
      rewrite e.
      etrans. eapply transportf_bind, assoc_disp.
      etrans. eapply transportf_bind.
      eapply cancel_postcomposition_disp, (z_iso_disp_after_inv_mor ii).
      rewrite id_left_disp.
      etrans. apply transport_f_f.
      use (@maponpaths_2 _ _ _ _ _ (idpath _)).
      apply homset_property.


  Definition postcomp_with_z_iso_disp_is_inj
             {C : category}
             {D : disp_cat C}
             {x y z : C}
             {f : x --> y}
             {g : x --> y}
             {h : y --> z}
             (Hh : is_z_isomorphism h)
             (p : f = g)
             {xx : D x}
             {yy : D y}
             {zz : D z}
             {ff : xx -->[ f ] yy}
             {gg : xx -->[ g ] yy}
             {hh : yy -->[ h ] zz}
             (Hhh : is_z_iso_disp (h ,, Hh) hh)
             (pp : (ff ;; hh
                    =
                      transportb
                        (λ z, _ -->[ z ] _)
                        (maponpaths (λ z, _ · h) p)
                        (gg ;; hh))%mor_disp)
    : ff = transportb _ p gg.
  Show proof.
    refine (id_right_disp_var _ @ _).
    pose (transportb_transpose_left (inv_mor_after_z_iso_disp Hhh)) as q.
    etrans.
    {
      do 2 apply maponpaths.
      exact (!q).
    }
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite assoc_disp.
    unfold transportb.
    rewrite transport_f_f.
    etrans.
    {
      apply maponpaths.
      apply maponpaths_2.
      exact pp.
    }
    unfold transportb.
    rewrite mor_disp_transportf_postwhisker.
    rewrite transport_f_f.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    etrans.
    {
      do 2 apply maponpaths.
      exact (inv_mor_after_z_iso_disp Hhh).
    }
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite id_right_disp.
    unfold transportb.
    rewrite !transport_f_f.
    apply maponpaths_2.
    apply homset_property.
End Utilities.

Displayed isomorphisms are closed under transporting
Definition is_z_iso_disp_transportf_fun_eq
           {C : category}
           {D : disp_cat C}
           {x y : C}
           {f g : z_iso x y}
           {xx : D x}
           {yy : D y}
           (ff : xx -->[ f ] yy)
           (p : pr1 f = pr1 g)
           (Hff : is_z_iso_disp f ff)
  : is_z_iso_disp
      g
      (transportf
         (λ z, _ -->[ z ] _)
         p
         ff).
Show proof.
  simple refine (_ ,, _ ,, _).
  - refine (transportf
              (λ z, _ -->[ z ] _)
              _
              (inv_mor_disp_from_z_iso Hff)).
    abstract
      (induction f as [ f Hf ] ;
       induction g as [ g Hg ] ;
       cbn in * ;
       induction p ;
       do 2 apply maponpaths ;
       apply isaprop_is_z_isomorphism).
  - abstract
      (induction f as [ f Hf ] ;
       induction g as [ g Hg ] ;
       cbn in * ;
       induction p ;
       cbn ;
       rewrite mor_disp_transportf_postwhisker ;
       refine (maponpaths _ (z_iso_disp_after_inv_mor Hff) @ _) ;
       unfold transportb ;
       rewrite transport_f_f ;
       apply maponpaths_2 ;
       apply homset_property).
  - abstract
      (induction f as [ f Hf ] ;
       induction g as [ g Hg ] ;
       cbn in * ;
       induction p ;
       cbn ;
       rewrite mor_disp_transportf_prewhisker ;
       refine (maponpaths _ (inv_mor_after_z_iso_disp Hff) @ _) ;
       unfold transportb ;
       rewrite transport_f_f ;
       apply maponpaths_2 ;
       apply homset_property).

Definition is_z_iso_disp_transportb_fun_eq
           {C : category}
           {D : disp_cat C}
           {x y : C}
           (f : z_iso x y)
           {g : z_iso x y}
           {xx : D x}
           {yy : D y}
           (ff : xx -->[ f ] yy)
           (p : pr1 g = pr1 f)
           (Hff : is_z_iso_disp f ff)
  : is_z_iso_disp
      g
      (transportb
         (λ z, _ -->[ z ] _)
         p
         ff).
Show proof.
  apply is_z_iso_disp_transportf_fun_eq.
  exact Hff.

Definition disp_z_iso_inv_on_left
  {C : category}
  {D : disp_cat C}
  {x y z : C}
  {f : x --> y}
  {g : y --> z}
  {h : x --> z}
  (Hf : is_z_isomorphism f)
  {xx : D x}
  {yy : D y}
  {zz : D z}
  {ff : xx -->[ f ] yy}
  {gg : yy -->[ g ] zz}
  {hh : xx -->[ h ] zz}
  (Hff : is_z_iso_disp (f ,, Hf) ff)
  (p : f · g = h)
  : gg = transportf _ (z_iso_inv_on_right _ _ _ (f,,Hf) g h (! p)) (pr1 Hff ;; hh)
  -> ff ;; gg = transportb _ p hh.
Show proof.
  intro q.
  rewrite q.
  clear q.
  rewrite mor_disp_transportf_prewhisker.
  use transportf_transpose_right.
  unfold transportb.
  rewrite transport_f_f.
  rewrite assoc_disp.
  unfold transportb.
  rewrite transport_f_f.
  etrans. {
    apply maponpaths.
    apply maponpaths_2.
    exact (pr2 (pr2 Hff)).
  }
  unfold transportb.
  rewrite mor_disp_transportf_postwhisker.
  rewrite transport_f_f.

  etrans. {
    apply maponpaths_2.
    refine (_ @ idpath (id_left _)).
    apply homset_property.
  }
  apply pathsinv0, id_left_disp_var.

Definition disp_z_iso_inv_on_right
  {C : category}
  {D : disp_cat C}
  {x y z : C}
  {f : x --> y}
  {g : y --> z}
  {h : x --> z}
  (Hg : is_z_isomorphism g)
  {xx : D x}
  {yy : D y}
  {zz : D z}
  (ff : xx -->[ f ] yy)
  {gg : yy -->[ g ] zz}
  (hh : xx -->[ h ] zz)
  (Hgg : is_z_iso_disp (g ,, Hg) gg)
  (p : f · g = h)
  : ff = transportb _ (z_iso_inv_on_left _ _ _ f (g,,Hg) h (! p)) (hh ;; pr1 Hgg)
  -> ff ;; gg = transportb _ p hh.
Show proof.
  intro q.
  rewrite q.
  clear q.
  unfold transportb.
  rewrite mor_disp_transportf_postwhisker.
  use transportf_transpose_right.
  unfold transportb.
  rewrite transport_f_f.
  rewrite assoc_disp_var.
  rewrite transport_f_f.
  etrans. {
    do 2 apply maponpaths.
    exact (pr1 (pr2 Hgg)).
  }
  unfold transportb.
  rewrite mor_disp_transportf_prewhisker.
  rewrite transport_f_f.

  etrans. {
    apply maponpaths_2.
    refine (_ @ idpath (id_right _)).
    apply homset_property.
  }
  apply pathsinv0, id_right_disp_var.

Lemma precomp_disp_id_left_inj
  {C : category} {D : disp_cat C}
  {y z : C}
  {f : C⟦y,z⟧}
  {yy : D y} {zz : D z}
  (ff1 ff2 : yy -->[f] zz)
  : id_disp yy ;; ff1 = id_disp yy ;; ff2 → ff1 = ff2.
Show proof.
  intro p.
  rewrite ! id_left_disp in p.
  refine (transportb_transpose_right p @ _).
  rewrite transport_b_b.
  use transportf_set.
  apply homset_property.