Library UniMath.CategoryTheory.DisplayedCats.Fibrations

Definitions of various kinds of fibrations, using displayed categories.

Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.MonoEpiIso.
Require Import UniMath.CategoryTheory.categories.HSET.Univalence.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Presheaf.
Local Open Scope cat.

Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.

Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Opposite.

Local Open Scope type_scope.
Local Open Scope mor_disp_scope.
Fibratons, opfibrations, and isofibrations are all displayed categories with extra lifting conditions.
Classically, these lifting conditions are usually taken by default as mere existence conditions; when they are given by operations, one speaks of a cloven fibration, etc.
We make the cloven version the default, so is_fibration etc are the cloven notions, and call the mere-existence versions un-cloven.
(This conventional is provisional and and might change in future.)

Isofibrations

The easiest to define are isofibrations, since they do not depend on a definition of (co-)cartesian-ness (because all displayed isomorphisms are cartesian).

Section Isofibrations.

Given an iso φ : c' =~ c in C, and an object d in D c, there’s some object d' in D c', and an iso φbar : d' =~ d over φ.

Definition iso_cleaving {C : category} (D : disp_cat C) : UU
:=
  forall (c c' : C) (i : z_iso c' c) (d : D c),
          ∑ d' : D c', z_iso_disp i d' d.

Definition iso_fibration (C : category) : UU
  := ∑ D : disp_cat C, iso_cleaving D.

Definition is_uncloven_iso_cleaving {C : category} (D : disp_cat C) : UU
:=
  forall (c c' : C) (i : z_iso c' c) (d : D c),
          ∃ d' : D c', z_iso_disp i d' d.

Definition weak_iso_fibration (C : category) : UU
  := ∑ D : disp_cat C, is_uncloven_iso_cleaving D.

As with fibrations, there is an evident dual version. However, in the iso case, it is self-dual: having forward (i.e. cocartesian) liftings along isos is equivalent to having backward (cartesian) liftings.

Definition is_op_isofibration {C : category} (D : disp_cat C) : UU
:=
  forall (c c' : C) (i : z_iso c c') (d : D c),
          ∑ d' : D c', z_iso_disp i d d'.

Lemma is_isofibration_iff_is_op_isofibration
    {C : category} (D : disp_cat C)
  : iso_cleaving D <-> is_op_isofibration D.
Show proof.
Abort.

End Isofibrations.

Fibrations

Section Fibrations.

Definition is_cartesian {C : category} {D : disp_cat C}
    {c c' : C} {f : c' --> c}
    {d : D c} {d' : D c'} (ff : d' -->[f] d)
  : UU
:= forall c'' (g : c'' --> c') (d'' : D c'') (hh : d'' -->[g·f] d),
  ∃! (gg : d'' -->[g] d'), gg ;; ff = hh.

See also cartesian_factorisation' below, for when the map one wishes to factor is not judgementally over g;;f, but over some equal map.
Definition cartesian_factorisation {C : category} {D : disp_cat C}
    {c c' : C} {f : c' --> c}
    {d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_cartesian ff)
    {c''} (g : c'' --> c') {d'' : D c''} (hh : d'' -->[g·f] d)
  : d'' -->[g] d'
:= pr1 (pr1 (H _ g _ hh)).

Definition cartesian_factorisation_commutes
    {C : category} {D : disp_cat C}
    {c c' : C} {f : c' --> c}
    {d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_cartesian ff)
    {c''} (g : c'' --> c') {d'' : D c''} (hh : d'' -->[g·f] d)
  : cartesian_factorisation H g hh ;; ff = hh
:= pr2 (pr1 (H _ g _ hh)).

While cartesian_factorisation_commutes shows that composition with and factorisation through a cartesian morphism are one-sided inverses in one direction, the following shows the other direction.
Definition cartesian_factorisation_of_composite
    {C : category} {D : disp_cat C}
    {c c' : C} {f : c' --> c}
    {d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_cartesian ff)
    {c'' : C} {g : c'' --> c'} {d'' : D c''} (gg : d'' -->[g] d')
  : gg = cartesian_factorisation H g (gg ;; ff).
Proof.
  exact (maponpaths pr1 (pr2 (H _ _ _ _) (_,, idpath _))).

This is essentially the third access function for is_cartesian, but given in a more usable form than pr2 (H …) would be.
Definition cartesian_factorisation_unique
    {C : category} {D : disp_cat C}
    {c c' : C} {f : c' --> c}
    {d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_cartesian ff)
    {c''} {g : c'' --> c'} {d'' : D c''} (gg gg' : d'' -->[g] d')
  : (gg ;; ff = gg' ;; ff) -> gg = gg'.
Show proof.
  intro Hggff.
  eapply pathscomp0. apply (cartesian_factorisation_of_composite H).
  eapply pathscomp0. apply maponpaths, Hggff.
  apply pathsinv0, cartesian_factorisation_of_composite.

Definition cartesian_factorisation' {C : category} {D : disp_cat C}
    {c c' : C} {f : c' --> c}
    {d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_cartesian ff)
    {c''} (g : c'' --> c')
    {h : c'' --> c} {d'' : D c''} (hh : d'' -->[h] d)
    (e : (g · f = h))
  : d'' -->[g] d'.
Show proof.
  use (cartesian_factorisation H g).
  exact (transportb _ e hh).

Definition cartesian_factorisation_commutes'
    {C : category} {D : disp_cat C}
    {c c' : C} {f : c' --> c}
    {d : D c} {d' : D c'} {ff : d' -->[f] d} (H : is_cartesian ff)
    {c''} (g : c'' --> c')
    {h : c'' --> c} {d'' : D c''} (hh : d'' -->[h] d)
    (e : (g · f = h))
  : (cartesian_factorisation' H g hh e) ;; ff
  = transportb _ e hh.
Show proof.
  apply cartesian_factorisation_commutes.

Definition cartesian_lift {C : category} {D : disp_cat C}
    {c} (d : D c) {c' : C} (f : c' --> c)
  : UU
:= ∑ (d' : D c') (ff : d' -->[f] d), is_cartesian ff.

Definition object_of_cartesian_lift {C : category} {D : disp_cat C}
    {c} (d : D c) {c' : C} (f : c' --> c)
    (fd : cartesian_lift d f)
  : D c'
:= pr1 fd.
Coercion object_of_cartesian_lift : cartesian_lift >-> ob_disp.

Definition mor_disp_of_cartesian_lift {C : category} {D : disp_cat C}
    {c} (d : D c) {c' : C} (f : c' --> c)
    (fd : cartesian_lift d f)
  : (fd : D c') -->[f] d
:= pr1 (pr2 fd).
Coercion mor_disp_of_cartesian_lift : cartesian_lift >-> mor_disp.

Definition cartesian_lift_is_cartesian {C : category} {D : disp_cat C}
    {c} (d : D c) {c' : C} (f : c' --> c)
    (fd : cartesian_lift d f)
  : is_cartesian fd
:= pr2 (pr2 fd).
Coercion cartesian_lift_is_cartesian : cartesian_lift >-> is_cartesian.

Definition is_cartesian_disp_functor
  {C C' : category} {F : functor C C'}
  {D : disp_cat C} {D' : disp_cat C'} (FF : disp_functor F D D') : UU
:= ∏ (c c' : C) (f : c' --> c)
      (d : D c) (d' : D c') (ff : d' -->[f] d),
   is_cartesian ff -> is_cartesian (♯ FF ff).

Definition disp_functor_identity_is_cartesian_disp_functor
           {C : category}
           (D : disp_cat C)
  : is_cartesian_disp_functor (disp_functor_identity D).
Show proof.
  intros x y f xx yy ff Hff.
  exact Hff.

Definition disp_functor_composite_is_cartesian_disp_functor
           {C₁ C₂ C₃ : category}
           {F : C₁ ⟶ C₂}
           {G : C₂ ⟶ C₃}
           {D₁ : disp_cat C₁}
           {D₂ : disp_cat C₂}
           {D₃ : disp_cat C₃}
           {FF : disp_functor F D₁ D₂}
           {GG : disp_functor G D₂ D₃}
           (HFF : is_cartesian_disp_functor FF)
           (HGG : is_cartesian_disp_functor GG)
  : is_cartesian_disp_functor (disp_functor_composite FF GG).
Show proof.
  intros x y f xx yy ff Hff.
  apply HGG.
  apply HFF.
  exact Hff.

Definition disp_functor_over_id_composite_is_cartesian
           {C : category}
           {D₁ D₂ D₃ : disp_cat C}
           {FF : disp_functor (functor_identity C) D₁ D₂}
           {GG : disp_functor (functor_identity C) D₂ D₃}
           (HFF : is_cartesian_disp_functor FF)
           (HGG : is_cartesian_disp_functor GG)
  : is_cartesian_disp_functor (disp_functor_over_id_composite FF GG).
Show proof.
  intros x y f xx yy ff Hff.
  apply HGG.
  apply HFF.
  exact Hff.

Definition cartesian_disp_functor
           {C₁ C₂ : category}
           (F : C₁ ⟶ C₂)
           (D₁ : disp_cat C₁)
           (D₂ : disp_cat C₂)
  : UU
  := ∑ (FF : disp_functor F D₁ D₂), is_cartesian_disp_functor FF.

Coercion disp_functor_of_cartesian_disp_functor
         {C₁ C₂ : category}
         {F : C₁ ⟶ C₂}
         {D₁ : disp_cat C₁}
         {D₂ : disp_cat C₂}
         (FF : cartesian_disp_functor F D₁ D₂)
  : disp_functor F D₁ D₂
  := pr1 FF.

Definition cartesian_disp_functor_is_cartesian
           {C₁ C₂ : category}
           {F : C₁ ⟶ C₂}
           {D₁ : disp_cat C₁}
           {D₂ : disp_cat C₂}
           (FF : cartesian_disp_functor F D₁ D₂)
  : is_cartesian_disp_functor FF
  := pr2 FF.

Definition cartesian_disp_functor_on_cartesian
           {C : category}
           {D₁ D₂ : disp_cat C}
           (F : cartesian_disp_functor (functor_identity C) D₁ D₂)
           {x y : C}
           {f : x --> y}
           {xx : D₁ x}
           {yy : D₁ y}
           {ff : xx -->[ f ] yy}
           (Hff : is_cartesian ff)
  : is_cartesian (♯ F ff)
  := pr2 F y x f yy xx ff Hff.

Lemma isaprop_is_cartesian
    {C : category} {D : disp_cat C}
    {c c' : C} {f : c' --> c}
    {d : D c} {d' : D c'} (ff : d' -->[f] d)
  : isaprop (is_cartesian ff).
Show proof.
  repeat (apply impred_isaprop; intro).
  apply isapropiscontr.

Proposition isaprop_is_cartesian_disp_functor
            {C₁ C₂ : category}
            {F : C₁ ⟶ C₂}
            {D₁ : disp_cat C₁}
            {D₂ : disp_cat C₂}
            (FF : disp_functor F D₁ D₂)
  : isaprop (is_cartesian_disp_functor FF).
Show proof.
  do 7 (use impred ; intro).
  apply isaprop_is_cartesian.

Definition cleaving {C : category} (D : disp_cat C) : UU
:=
  forall (c c' : C) (f : c' --> c) (d : D c), cartesian_lift d f.

(Cloven) fibration


Definition fibration (C : category) : UU
:=
  ∑ D : disp_cat C, cleaving D.

Weak fibration



Definition is_cleaving {C : category} (D : disp_cat C) : UU
:=
  forall (c c' : C) (f : c' --> c) (d : D c), ∥ cartesian_lift d f ∥.

Definition weak_fibration (C : category) : UU
:= ∑ D : disp_cat C, is_cleaving D.

Connection with isofibrations


Lemma is_z_iso_from_is_cartesian {C : category} {D : disp_cat C}
    {c c' : C} (i : z_iso c' c) {d : D c} {d'} (ff : d' -->[i] d)
  : is_cartesian ff -> is_z_iso_disp i ff.
Show proof.
  intros Hff.
  use (_,,_); try split.
  - use
      (cartesian_factorisation' Hff (inv_from_z_iso i) (id_disp _)).
    apply z_iso_after_z_iso_inv.
  - apply cartesian_factorisation_commutes'.
  - apply (cartesian_factorisation_unique Hff).
    etrans. apply assoc_disp_var.
    rewrite cartesian_factorisation_commutes'.
    etrans. eapply transportf_bind.
      etrans. apply mor_disp_transportf_prewhisker.
      eapply transportf_bind, id_right_disp.
    apply pathsinv0.
    etrans. apply mor_disp_transportf_postwhisker.
    etrans. eapply transportf_bind, id_left_disp.
    apply maponpaths_2, homset_property.

Lemma is_isofibration_from_is_fibration {C : category} {D : disp_cat C}
  : cleaving D -> iso_cleaving D.
Show proof.
  intros D_fib c c' f d.
  assert (fd := D_fib _ _ f d).
  exists (fd : D _).
  exists (fd : _ -->[_] _).
  apply is_z_iso_from_is_cartesian; exact fd.

Uniqueness of cartesian lifts


Definition cartesian_lifts_iso {C : category} {D : disp_cat C}
    {c} {d : D c} {c' : C} {f : c' --> c} (fd fd' : cartesian_lift d f)
  : z_iso_disp (identity_z_iso c') fd fd'.
Show proof.
  use (_,,(_,,_)).
  - exact (cartesian_factorisation' fd' (identity _) fd (id_left _)).
  - exact (cartesian_factorisation' fd (identity _) fd' (id_left _)).
  - cbn; split.
    + apply (cartesian_factorisation_unique fd').
      etrans. apply assoc_disp_var.
      rewrite cartesian_factorisation_commutes'.
      etrans. eapply transportf_bind, mor_disp_transportf_prewhisker.
      rewrite cartesian_factorisation_commutes'.
      etrans. apply transport_f_f.
      apply pathsinv0.
      etrans. apply mor_disp_transportf_postwhisker.
      rewrite id_left_disp.
      etrans. apply transport_f_f.
      apply maponpaths_2, homset_property.
    + apply (cartesian_factorisation_unique fd).
      etrans. apply assoc_disp_var.
      rewrite cartesian_factorisation_commutes'.
      etrans. eapply transportf_bind, mor_disp_transportf_prewhisker.
      rewrite cartesian_factorisation_commutes'.
      etrans. apply transport_f_f.
      apply pathsinv0.
      etrans. apply mor_disp_transportf_postwhisker.
      rewrite id_left_disp.
      etrans. apply transport_f_f.
      apply maponpaths_2, homset_property.

Definition cartesian_lifts_iso_commutes {C : category} {D : disp_cat C}
    {c} {d : D c} {c' : C} {f : c' --> c} (fd fd' : cartesian_lift d f)
  : (cartesian_lifts_iso fd fd') ;; fd'
  = transportb _ (id_left _) (fd : _ -->[_] _).
Show proof.
  cbn. apply cartesian_factorisation_commutes'.

In a displayed category (i.e. univalent), cartesian lifts are literally unique, if they exist; that is, the type of cartesian lifts is always a proposition.
Definition isaprop_cartesian_lifts
    {C : category} {D : disp_cat C} (D_cat : is_univalent_disp D)
    {c} (d : D c) {c' : C} (f : c' --> c)
  : isaprop (cartesian_lift d f).
Show proof.
  apply invproofirrelevance; intros fd fd'.
  use total2_paths_f.
  { apply (isotoid_disp D_cat (idpath _)); cbn.
    apply cartesian_lifts_iso. }
  apply subtypePath.
  { intros ff. repeat (apply impred; intro).
    apply isapropiscontr. }
  etrans.
  { exact (! transport_map (λ x:D c', pr1) _ _). }
  cbn. etrans. apply transportf_precompose_disp.
  rewrite idtoiso_isotoid_disp.
  use (pathscomp0 (maponpaths _ _) (transportfbinv _ _ _)).
  apply (precomp_with_z_iso_disp_is_inj (cartesian_lifts_iso fd fd')).
  etrans. apply assoc_disp.
  etrans. eapply transportf_bind, cancel_postcomposition_disp.
    use inv_mor_after_z_iso_disp.
  etrans. eapply transportf_bind, id_left_disp.
  apply pathsinv0.
  etrans. apply mor_disp_transportf_prewhisker.
  etrans. eapply transportf_bind, cartesian_lifts_iso_commutes.
  apply maponpaths_2, homset_property.

Definition univalent_fibration_is_cloven
    {C : category} {D : disp_cat C} (D_cat : is_univalent_disp D)
  : is_cleaving D -> cleaving D.
Show proof.
  intros D_fib c c' f d.
  apply (squash_to_prop (D_fib c c' f d)).
  apply isaprop_cartesian_lifts; assumption.
  auto.

End Fibrations.

Definition isaprop_cleaving
           {C : univalent_category}
           (D : disp_cat C)
           (HD : is_univalent_disp D)
  : isaprop (cleaving D).
Show proof.
  repeat (use impred ; intro).
  apply isaprop_cartesian_lifts.
  exact HD.

Section Discrete_Fibrations.

Definition is_discrete_fibration {C : category} (D : disp_cat C) : UU
:=
  (forall (c c' : C) (f : c' --> c) (d : D c),
          ∃! d' : D c', d' -->[f] d)
  ×
  (forall c, isaset (D c)).

Definition discrete_fibration C : UU
  := ∑ D : disp_cat C, is_discrete_fibration D.

Coercion disp_cat_from_discrete_fibration C (D : discrete_fibration C)
  : disp_cat C := pr1 D.
Definition unique_lift {C} {D : discrete_fibration C} {c c'}
           (f : c' --> c) (d : D c)
  : ∃! d' : D c', d' -->[f] d
  := pr1 (pr2 D) c c' f d.
Definition isaset_fiber_discrete_fibration {C} (D : discrete_fibration C)
           (c : C) : isaset (D c) := pr2 (pr2 D) c.

TODO: move upstream
Lemma pair_inj {A : UU} {B : A -> UU} (is : isaset A) {a : A}
   {b b' : B a} : (a,,b) = (a,,b') -> b = b'.
Show proof.
  intro H.
  use (invmaponpathsincl _ _ _ _ H).
  apply isofhlevelffib. intro. apply is.

Lemma disp_mor_unique_disc_fib C (D : discrete_fibration C)
  : ∏ (c c' : C) (f : c --> c') (d : D c) (d' : D c')
      (ff ff' : d -->[f] d'), ff = ff'.
Show proof.
  intros.
  assert (XR := unique_lift f d').
  assert (foo : ((d,,ff) : ∑ d0, d0 -->[f] d') = (d,,ff')).
  { apply proofirrelevancecontr. apply XR. }
  apply (pair_inj (isaset_fiber_discrete_fibration _ _ ) foo).

Lemma isaprop_disc_fib_hom C (D : discrete_fibration C)
  : ∏ (c c' : C) (f : c --> c') (d : D c) (d' : D c'),
    isaprop (d -->[f] d').
Show proof.
  intros.
  apply invproofirrelevance.
  intros x x'. apply disp_mor_unique_disc_fib.

Definition fibration_from_discrete_fibration C (D : discrete_fibration C)
  : cleaving D.
Show proof.
  intros c c' f d.
  use tpair.
  - exact (pr1 (iscontrpr1 (unique_lift f d))).
  - use tpair.
    + exact (pr2 (iscontrpr1 (unique_lift f d))).
    + intros c'' g db hh.
      set (ff := pr2 (iscontrpr1 (unique_lift f d)) ). cbn in ff.
      set (d' := pr1 (iscontrpr1 (unique_lift f d))) in *.
      set (ggff := pr2 (iscontrpr1 (unique_lift (g·f) d)) ). cbn in ggff.
      set (d'' := pr1 (iscontrpr1 (unique_lift (g·f) d))) in *.
      set (gg := pr2 (iscontrpr1 (unique_lift g d'))). cbn in gg.
      set (d3 := pr1 (iscontrpr1 (unique_lift g d'))) in *.
      assert (XR : ((d'',, ggff) : ∑ r, r -->[g·f] d) = (db,,hh)).
      { apply proofirrelevancecontr. apply (pr2 D). }
      assert (XR1 : ((d'',, ggff) : ∑ r, r -->[g·f] d) = (d3 ,,gg;;ff)).
      { apply proofirrelevancecontr. apply (pr2 D). }
      assert (XT := maponpaths pr1 XR). cbn in XT.
      assert (XT1 := maponpaths pr1 XR1). cbn in XT1.
      generalize XR.
      generalize XR1; clear XR1.
      destruct XT.
      generalize gg; clear gg.
      destruct XT1.
      intros gg XR1 XR0.
      apply iscontraprop1.
      * apply invproofirrelevance.
        intros x x'. apply subtypePath.
        { intro. apply homsets_disp. }
        apply disp_mor_unique_disc_fib.
      * exists gg.
        cbn.
        assert (XX := pair_inj (isaset_fiber_discrete_fibration _ _ ) XR1).
        assert (YY := pair_inj (isaset_fiber_discrete_fibration _ _ ) XR0).
        etrans. apply (!XX). apply YY.

Section Equivalence_disc_fibs_presheaves.


Variable C : category.

Definition precat_of_discrete_fibs_ob_mor : precategory_ob_mor.
Show proof.
  exists (discrete_fibration C).
  intros a b. exact (disp_functor (functor_identity _ ) a b).

Definition precat_of_discrete_fibs_data : precategory_data.
Show proof.
  exists precat_of_discrete_fibs_ob_mor.
  split.
  - intro.
    exact (@disp_functor_identity _ _ ).
  - intros ? ? ? f g. exact (disp_functor_composite f g ).

Lemma eq_discrete_fib_mor (F G : precat_of_discrete_fibs_ob_mor)
      (a b : F --> G)
      (H : ∏ x y, pr1 (pr1 a) x y = pr1 (pr1 b) x y)
  : a = b.
Show proof.
  apply subtypePath.
  { intro. apply isaprop_disp_functor_axioms. }
  use total2_paths_f.
  - apply funextsec. intro x.
    apply funextsec. intro y.
    apply H.
  - repeat (apply funextsec; intro).
    apply disp_mor_unique_disc_fib.

Definition precat_axioms_of_discrete_fibs : is_precategory precat_of_discrete_fibs_data.
Show proof.
  repeat split; intros;
  apply eq_discrete_fib_mor; intros; apply idpath.

Definition precat_of_discrete_fibs : precategory
  := (_ ,, precat_axioms_of_discrete_fibs).

Lemma has_homsets_precat_of_discrete_fibs : has_homsets precat_of_discrete_fibs.
Show proof.
  intros f f'.
  apply (isofhleveltotal2 2).
  - apply (isofhleveltotal2 2).
    + do 2 (apply impred; intro).
      apply isaset_fiber_discrete_fibration.
    + intro. do 6 (apply impred; intro).
      apply homsets_disp.
  - intro. apply isasetaprop. apply isaprop_disp_functor_axioms.

Definition Precat_of_discrete_fibs : category
  := ( precat_of_discrete_fibs ,, has_homsets_precat_of_discrete_fibs).

Functor from discrete fibrations to presheaves

Functor on objects



Definition preshv_data_from_disc_fib_ob (D : discrete_fibration C)
  : functor_data C^op HSET_univalent_category.
Show proof.
  use tpair.
  + intro c. exists (D c). apply isaset_fiber_discrete_fibration.
  + intros c' c f x. cbn in *.
    exact (pr1 (iscontrpr1 (unique_lift f x))).

Definition preshv_ax_from_disc_fib_ob (D : discrete_fibration C)
  : is_functor (preshv_data_from_disc_fib_ob D).
Show proof.
  split.
  + intro c; cbn.
    apply funextsec; intro x. simpl.
    apply pathsinv0. apply path_to_ctr.
      apply id_disp.
  + intros c c' c'' f g. cbn in *.
    apply funextsec; intro x.
    apply pathsinv0.
    apply path_to_ctr.
    eapply comp_disp.
    * apply (pr2 (iscontrpr1 (unique_lift g _))).
    * apply (pr2 (iscontrpr1 (unique_lift f _ ))).

Definition preshv_from_disc_fib_ob (D : discrete_fibration C)
  : PreShv C := (_ ,, preshv_ax_from_disc_fib_ob D).

Functor on morphisms


Definition foo : functor_data Precat_of_discrete_fibs (PreShv C).
Show proof.
  exists preshv_from_disc_fib_ob.
  intros D D' a.
  use tpair.
  - intro c. simpl.
    exact (pr1 a c).
  - abstract (
        intros x y f; cbn in *;
        apply funextsec; intro d;
        apply path_to_ctr;
        apply ♯a;
        apply (pr2 (iscontrpr1 (unique_lift f _ )))
      ).

Functor properties


Definition bar : is_functor foo.
Show proof.
  split.
  - intro D. apply nat_trans_eq. { apply has_homsets_HSET. }
    intro c . apply idpath.
  - intros D E F a b. apply nat_trans_eq. { apply has_homsets_HSET. }
    intro c. apply idpath.

Definition functor_Disc_Fibs_to_preShvs : functor _ _
  := ( _ ,, bar).

Functor from presheaves to discrete fibrations

Functor on objects


Definition disp_cat_from_preshv (D : PreShv C) : disp_cat C.
Show proof.
  use tpair.
  - use tpair.
    + exists (λ c, pr1hSet (pr1 D c)).
      intros x y c d f. exact (functor_on_morphisms (pr1 D) f d = c).
    + split.
      * intros; cbn in *; apply (toforallpaths _ _ _ (functor_id D x ) _ ).
      * intros ? ? ? ? ? ? ? ? X X0; cbn in *;
        etrans; [apply (toforallpaths _ _ _ (functor_comp D g f ) _ ) |];
        cbn; etrans; [ apply maponpaths; apply X0 |];
        apply X.
  - abstract (
         repeat use tpair; cbn; intros; try apply setproperty;
         apply isasetaprop; apply setproperty
       ).

Definition disc_fib_from_preshv (D : PreShv C) : discrete_fibration C.
Show proof.
  use tpair.
  - apply (disp_cat_from_preshv D).
  - cbn.
    split.
    + intros c c' f d. simpl.
      use unique_exists.
      * apply (functor_on_morphisms (pr1 D) f d).
      * apply idpath.
      * intro. apply setproperty.
      * intros. apply pathsinv0. assumption.
    + intro. simpl. apply setproperty.

Functor on morphisms


Definition functor_data_preShv_Disc_fibs
  : functor_data (PreShv C) Precat_of_discrete_fibs.
Show proof.
  use tpair.
  - apply disc_fib_from_preshv.
  - intros F G a.
    use tpair.
    + use tpair.
      * intros c. apply (pr1 a c).
      * intros x y X Y f H;
        assert (XR := nat_trans_ax a);
        apply pathsinv0; etrans; [|apply (toforallpaths _ _ _ (XR _ _ f))];
        cbn; apply maponpaths, (!H).
    + cbn. abstract (repeat use tpair; cbn; intros; apply setproperty).

Functor properties


Definition is_functor_functor_data_preShv_Disc_fibs
  : is_functor functor_data_preShv_Disc_fibs .
Show proof.
  split; unfold functor_idax, functor_compax; intros;
  apply eq_discrete_fib_mor; intros; apply idpath.

Definition functor_preShvs_to_Disc_Fibs : functor _ _
  := ( _ ,, is_functor_functor_data_preShv_Disc_fibs ).

Definition η_disc_fib : nat_trans (functor_identity _ )
                          (functor_preShvs_to_Disc_Fibs ∙ functor_Disc_Fibs_to_preShvs).
Show proof.
  use tpair.
  - intro F.
    cbn. use tpair.
    + red. cbn. intro c; apply idfun.
    + intros c c' f. cbn in *. apply idpath.
  - abstract (
        intros F G a;
        apply nat_trans_eq; [ apply has_homsets_HSET |];
        intro c ; apply idpath
      ).

Definition ε_disc_fib
  : nat_trans (functor_Disc_Fibs_to_preShvs ∙ functor_preShvs_to_Disc_Fibs)
              (functor_identity _ ).
Show proof.
  use tpair.
  - intro D.
    use tpair.
    + use tpair.
      * cbn. intro c; apply idfun.
      * cbn. intros c c' x y f H.
        set (XR := pr2 (iscontrpr1 (unique_lift f y))). cbn in XR.
        apply (transportf (λ t, t -->[f] y) H XR).
    + abstract (split; cbn; intros; apply disp_mor_unique_disc_fib).
  - abstract (intros c c' f; apply eq_discrete_fib_mor; intros; apply idpath).

Definition ε_inv_disc_fib
  : nat_trans (functor_identity _ )
      (functor_Disc_Fibs_to_preShvs ∙ functor_preShvs_to_Disc_Fibs).
Show proof.
  use tpair.
  - intro D.
    cbn.
    use tpair.
    + use tpair.
      * cbn. intro c; apply idfun.
      * abstract (
            intros c c' x y f H; cbn;
            apply pathsinv0; apply path_to_ctr; apply H
          ).
    + abstract (
          split;
          [ intros x y; apply isaset_fiber_discrete_fibration |];
          intros; apply isaset_fiber_discrete_fibration
        ).
  - abstract (intros c c' f; apply eq_discrete_fib_mor; intros; apply idpath).

Definition adjunction_data_disc_fib
  : adjunction_data (PreShv C) Precat_of_discrete_fibs.
Show proof.
  exists functor_preShvs_to_Disc_Fibs.
  exists functor_Disc_Fibs_to_preShvs.
  exists η_disc_fib.
  exact ε_disc_fib.

Lemma forms_equivalence_disc_fib
  : forms_equivalence adjunction_data_disc_fib.
Show proof.
  split.
  - intro F.
    apply nat_trafo_z_iso_if_pointwise_z_iso.
    intro c. cbn.
    set (XR := hset_equiv_is_z_iso _ _ (idweq (pr1 F c : hSet) )).
    apply XR.
  - intro F.
    use (_ ,, (_,,_ )).
    + apply ε_inv_disc_fib.
    + apply eq_discrete_fib_mor.
      intros. apply idpath.
    + apply eq_discrete_fib_mor.
      intros. apply idpath.

Definition adj_equivalence_disc_fib : adj_equivalence_of_cats _ :=
  adjointification (_ ,, forms_equivalence_disc_fib).

End Equivalence_disc_fibs_presheaves.

End Discrete_Fibrations.

The notion of an opcartesian morphism
Section Opcartesian.
  Context {C : category}
          {D : disp_cat C}.

  Definition is_opcartesian
             {c₁ c₂ : C}
             {f : c₁ --> c₂}
             {cc₁ : D c₁}
             {cc₂ : D c₂}
             (ff : cc₁ -->[ f ] cc₂)
    : UU
    := ∏ (c₃ : C)
         (cc₃ : D c₃)
         (g : c₂ --> c₃)
         (hh : cc₁ -->[ f · g ] cc₃),
       ∃! (gg : cc₂ -->[ g ] cc₃),
       ff ;; gg = hh.

  Section ProjectionsOpcartesian.
    Context {c₁ c₂ : C}
            {f : c₁ --> c₂}
            {cc₁ : D c₁}
            {cc₂ : D c₂}
            {ff : cc₁ -->[ f ] cc₂}
            (Hff : is_opcartesian ff)
            {c₃ : C}
            {cc₃ : D c₃}
            (g : c₂ --> c₃)
            (hh : cc₁ -->[ f · g ] cc₃).

    Definition opcartesian_factorisation
      : cc₂ -->[ g ] cc₃
      := pr11 (Hff c₃ cc₃ g hh).

    Definition opcartesian_factorisation_commutes
      : ff ;; opcartesian_factorisation = hh
      := pr21 (Hff c₃ cc₃ g hh).

    Definition opcartesian_factorisation_unique
               (gg₁ gg₂ : cc₂ -->[ g ] cc₃)
               (H : ff ;; gg₁ = ff ;; gg₂)
      : gg₁ = gg₂.
    Show proof.
      exact (maponpaths
               pr1
               (proofirrelevance
               _
               (isapropifcontr
                  (Hff c₃ cc₃ g (ff ;; gg₁)))
               (gg₁ ,, idpath _)
               (gg₂ ,, !H))).
  End ProjectionsOpcartesian.
End Opcartesian.

Opcartesian morphism
Definition is_cartesian_weq_is_opcartesian
           {C : category}
           {D : disp_cat C}
           {c₁ c₂ : C}
           {f : c₁ --> c₂}
           {cc₁ : D c₁}
           {cc₂ : D c₂}
           (ff : cc₁ -->[ f ] cc₂)
  : is_cartesian ff ≃ @is_opcartesian _ (op_disp_cat D) _ _ _ _ _ ff.
Show proof.
  use make_weq.
  - exact (λ Hff c₃ cc₃ g hh, Hff c₃ g cc₃ hh).
  - use isweq_iso.
    + exact (λ Hff c₃ cc₃ g hh, Hff c₃ g cc₃ hh).
    + intro ; apply idpath.
    + intro ; apply idpath.

Definition is_opcartesian_weq_is_cartesian
           {C : category}
           {D : disp_cat C}
           {c₁ c₂ : C}
           {f : c₁ --> c₂}
           {cc₁ : D c₁}
           {cc₂ : D c₂}
           (ff : cc₁ -->[ f ] cc₂)
  : is_opcartesian ff ≃ @is_cartesian _ (op_disp_cat D) _ _ _ _ _ ff.
Show proof.
  use make_weq.
  - exact (λ Hff c₃ cc₃ g hh, Hff c₃ g cc₃ hh).
  - use isweq_iso.
    + exact (λ Hff c₃ cc₃ g hh, Hff c₃ g cc₃ hh).
    + intro ; apply idpath.
    + intro ; apply idpath.

Definition is_cartesian_to_is_opcartesian
           {C : category}
           {D : disp_cat C}
           {c₁ c₂ : C}
           {f : c₁ --> c₂}
           {cc₁ : D c₁}
           {cc₂ : D c₂}
           {ff : cc₁ -->[ f ] cc₂}
           (Hff : @is_cartesian _ (op_disp_cat D) _ _ _ _ _ ff)
  : is_opcartesian ff
  := invmap (is_opcartesian_weq_is_cartesian ff) Hff.

Definition isaprop_is_opcartesian
           {C : category}
           {D : disp_cat C}
           {c₁ c₂ : C}
           {f : c₁ --> c₂}
           {cc₁ : D c₁}
           {cc₂ : D c₂}
           (ff : cc₁ -->[ f ] cc₂)
  : isaprop (is_opcartesian ff).
Show proof.
  apply (isofhlevelweqb 1 (is_opcartesian_weq_is_cartesian ff)).
  apply isaprop_is_cartesian.

Opcleavings
Section Opcleaving.
  Context {C : category}
          (D : disp_cat C).

  Definition opcartesian_lift
             {c₁ c₂ : C}
             (cc₁ : D c₁)
             (f : c₁ --> c₂)
    : UU
    := ∑ (cc₂ : D c₂) (ff : cc₁ -->[ f ] cc₂), is_opcartesian ff.

  Definition ob_of_opcartesian_lift
             {c₁ c₂ : C}
             {cc₁ : D c₁}
             {f : c₁ --> c₂}
             (ℓ : opcartesian_lift cc₁ f)
    : D c₂
    := pr1 ℓ.

  Definition mor_of_opcartesian_lift
             {c₁ c₂ : C}
             {cc₁ : D c₁}
             {f : c₁ --> c₂}
             (ℓ : opcartesian_lift cc₁ f)
    : cc₁ -->[ f ] ob_of_opcartesian_lift ℓ
    := pr12 ℓ.

  Definition mor_of_opcartesian_lift_is_opcartesian
             {c₁ c₂ : C}
             {cc₁ : D c₁}
             {f : c₁ --> c₂}
             (ℓ : opcartesian_lift cc₁ f)
    : is_opcartesian (mor_of_opcartesian_lift ℓ)
    := pr22 ℓ.

  Definition opcleaving
    : UU
    := ∏ (c₁ c₂ : C)
         (cc₁ : D c₁)
         (f : c₁ --> c₂),
       opcartesian_lift cc₁ f.

  Definition is_opcleaving
    : UU
    := ∏ (c₁ c₂ : C)
         (cc₁ : D c₁)
         (f : c₁ --> c₂),
       ∥ opcartesian_lift cc₁ f ∥.
End Opcleaving.

Definition opcleaving_ob
           {C : category}
           {D : disp_cat C}
           (HD : opcleaving D)
           {c c' : C}
           (f : c --> c')
           (d : D c)
  : D c'
  := ob_of_opcartesian_lift _ (HD c c' d f).

Definition opcleaving_mor
           {C : category}
           {D : disp_cat C}
           (HD : opcleaving D)
           {c c' : C}
           (f : c --> c')
           (d : D c)
  : d -->[ f ] opcleaving_ob HD f d
  := mor_of_opcartesian_lift _ (HD c c' d f).

Definition cleaving_weq_opcleaving
           {C : category}
           (D : disp_cat C)
  : cleaving D ≃ @opcleaving _ (op_disp_cat D).
Show proof.
  use make_weq.
  - exact (λ HD c₁ c₂ cc₁ f,
           let ℓ := HD c₁ c₂ f cc₁ in

           tpair
             (fun cc₂ => total2 (fun ff => @is_opcartesian _ _ _ _ _ cc₁ cc₂ ff))
             (pr1 ℓ)
             (tpair
                (@is_opcartesian _ _ _ _ _ cc₁ ℓ) (pr12 ℓ)
                (pr1weq (is_cartesian_weq_is_opcartesian ℓ) ℓ))).
  - use isweq_iso.
    + refine (λ HD c₁ c₂ cc₁ f,
              let ℓ := HD c₁ c₂ f cc₁ in
              pr1 ℓ ,, pr12 ℓ ,, _).
      exact (invmap (is_cartesian_weq_is_opcartesian _) (pr22 ℓ)).
    + intro ; apply idpath.
    + intro ; apply idpath.

Definition opcleaving_weq_cleaving
           {C : category}
           (D : disp_cat C)
  : opcleaving D ≃ @cleaving _ (op_disp_cat D).
Show proof.
  use make_weq.
  - exact (λ HD c₁ c₂ cc₁ f,
           let ℓ := HD c₁ c₂ f cc₁ in

           tpair
             (fun d' => total2 (fun ff => @is_cartesian _ _ _ _ _ f d' ff))
             (pr1 ℓ)
             (tpair
                (@is_cartesian _ _ _ _ _ f (pr1 ℓ)) (pr12 ℓ)
                (pr1weq
                   (@is_opcartesian_weq_is_cartesian _ D _ _ _ _ _ (pr12 ℓ))
                   (pr22 ℓ)))).
  - use isweq_iso.
    + refine (λ HD c₁ c₂ cc₁ f,
              let ℓ := HD c₁ c₂ f cc₁ in
              pr1 ℓ ,, pr12 ℓ ,, _).
      exact (invmap (is_opcartesian_weq_is_cartesian _) (pr22 ℓ)).
    + intro ; apply idpath.
    + intro ; apply idpath.

Definition isaprop_opcleaving
           {C : univalent_category}
           (D : disp_cat C)
           (HD : is_univalent_disp D)
  : isaprop (opcleaving D).
Show proof.
  use (isofhlevelweqb
         1
         (opcleaving_weq_cleaving D)).
  use (@isaprop_cleaving (op_unicat C) (op_disp_cat _) _).
  apply is_univalent_op_disp_cat.
  exact HD.

Cloven opfibration
Definition opfibration
           (C : category)
  : UU
  := ∑ (D : disp_cat C), opcleaving D.

Weak opfibration
Definition weak_opfibration
           (C : category)
  : UU
  := ∑ (D : disp_cat C), is_opcleaving D.

Definition is_opcartesian_disp_functor
           {C₁ C₂ : category}
           {F : C₁ ⟶ C₂}
           {D : disp_cat C₁}
           {D' : disp_cat C₂}
           (FF : disp_functor F D D')
  : UU
  := ∏ (c c' : C₁)
        (f : c' --> c)
        (d : D c)
        (d' : D c')
        (ff : d' -->[f] d),
     is_opcartesian ff -> is_opcartesian (♯ FF ff).

Proposition isaprop_is_opcartesian_disp_functor
            {C₁ C₂ : category}
            {F : C₁ ⟶ C₂}
            {D₁ : disp_cat C₁}
            {D₂ : disp_cat C₂}
            (FF : disp_functor F D₁ D₂)
  : isaprop (is_opcartesian_disp_functor FF).
Show proof.
  do 7 (use impred ; intro).
  apply isaprop_is_opcartesian.

Definition disp_functor_identity_is_opcartesian_disp_functor
           {C : category}
           (D : disp_cat C)
  : is_opcartesian_disp_functor (disp_functor_identity D).
Show proof.
  intros x y f xx yy ff Hff.
  exact Hff.

Definition disp_functor_composite_is_opcartesian_disp_functor
           {C₁ C₂ C₃ : category}
           {F : C₁ ⟶ C₂}
           {G : C₂ ⟶ C₃}
           {D₁ : disp_cat C₁}
           {D₂ : disp_cat C₂}
           {D₃ : disp_cat C₃}
           {FF : disp_functor F D₁ D₂}
           {GG : disp_functor G D₂ D₃}
           (HFF : is_opcartesian_disp_functor FF)
           (HGG : is_opcartesian_disp_functor GG)
  : is_opcartesian_disp_functor (disp_functor_composite FF GG).
Show proof.
  intros x y f xx yy ff Hff.
  apply HGG.
  apply HFF.
  exact Hff.

Definition disp_functor_over_id_composite_is_opcartesian
           {C : category}
           {D₁ D₂ D₃ : disp_cat C}
           {FF : disp_functor (functor_identity C) D₁ D₂}
           {GG : disp_functor (functor_identity C) D₂ D₃}
           (HFF : is_opcartesian_disp_functor FF)
           (HGG : is_opcartesian_disp_functor GG)
  : is_opcartesian_disp_functor (disp_functor_over_id_composite FF GG).
Show proof.
  intros x y f xx yy ff Hff.
  apply HGG.
  apply HFF.
  exact Hff.

Definition opcartesian_disp_functor
           {C₁ C₂ : category}
           (F : C₁ ⟶ C₂)
           (D₁ : disp_cat C₁)
           (D₂ : disp_cat C₂)
  : UU
  := ∑ (FF : disp_functor F D₁ D₂), is_opcartesian_disp_functor FF.

Coercion disp_functor_of_opcartesian_disp_functor
         {C₁ C₂ : category}
         {F : C₁ ⟶ C₂}
         {D₁ : disp_cat C₁}
         {D₂ : disp_cat C₂}
         (FF : opcartesian_disp_functor F D₁ D₂)
  : disp_functor F D₁ D₂
  := pr1 FF.

Definition opcartesian_disp_functor_is_opcartesian
           {C₁ C₂ : category}
           {F : C₁ ⟶ C₂}
           {D₁ : disp_cat C₁}
           {D₂ : disp_cat C₂}
           (FF : opcartesian_disp_functor F D₁ D₂)
  : is_opcartesian_disp_functor FF
  := pr2 FF.

Opfibrations are isofibrations
Section IsoCleavingFromOpcleaving.
  Context {C : category}
          (D : disp_cat C)
          (HD : opcleaving D).

  Section Lift.
    Context {x y : C}
            (f : z_iso x y)
            (d : D y).

    Definition z_iso_cleaving_from_opcleaving_ob
      : D x
      := opcleaving_ob HD (inv_from_z_iso f) d.

    Let ℓ : d -->[ inv_from_z_iso f ] z_iso_cleaving_from_opcleaving_ob
      := opcleaving_mor HD (inv_from_z_iso f) d.
    Let ℓ_opcart : is_opcartesian (pr12 (HD y x d (inv_from_z_iso f)))
      := pr22 (HD _ _ d (inv_from_z_iso f)).

    Definition z_iso_cleaving_from_opcleaving_ob_disp_iso_map
      : z_iso_cleaving_from_opcleaving_ob -->[ f ] d.
    Show proof.
      use (opcartesian_factorisation ℓ_opcart).
      refine (transportb
                (λ z, _ -->[ z ] _)
                _
                (id_disp d)).
      apply z_iso_after_z_iso_inv.

    Definition z_iso_cleaving_from_opcleaving_ob_disp_iso
      : z_iso_disp f z_iso_cleaving_from_opcleaving_ob d.
    Show proof.
      use make_z_iso_disp.
      - exact z_iso_cleaving_from_opcleaving_ob_disp_iso_map.
      - simple refine (_ ,, _ ,, _).
        + exact ℓ.
        + abstract
            (apply opcartesian_factorisation_commutes).
        + abstract
            (apply (opcartesian_factorisation_unique ℓ_opcart) ;
             unfold transportb ;
             rewrite mor_disp_transportf_prewhisker ;
             rewrite assoc_disp ;
             unfold transportb ;
             etrans ;
               [ apply maponpaths ;
                 apply maponpaths_2 ;
                 apply (opcartesian_factorisation_commutes ℓ_opcart)
               | ] ;
             unfold transportb ;
             rewrite mor_disp_transportf_postwhisker ;
             rewrite id_left_disp, id_right_disp ;
             unfold transportb ;
             rewrite !transport_f_f ;
             apply maponpaths_2 ;
             apply homset_property).
  End Lift.

  Definition iso_cleaving_from_opcleaving
    : iso_cleaving D
    := λ x y f d,
       z_iso_cleaving_from_opcleaving_ob f d
       ,,
       z_iso_cleaving_from_opcleaving_ob_disp_iso f d.
End IsoCleavingFromOpcleaving.

Section isofibration_from_disp_over_univalent.

Context (C : category)
        (Ccat : is_univalent C)
        (D : disp_cat C).

Definition iso_cleaving_category : iso_cleaving D.
Show proof.
  intros c c' i d.
  use tpair.
  - exact (transportb D (isotoid _ Ccat i) d).
  - generalize i. clear i.
    apply forall_isotoid.
    { apply Ccat. }
    intro e. induction e.
    cbn.
    rewrite isotoid_identity_iso.
    cbn.
    apply identity_z_iso_disp.

End isofibration_from_disp_over_univalent.

Split fibrations


Definition cleaving_ob {C : category} {D : disp_cat C}
           (X : cleaving D) {c c' : C} (f : c' --> c) (d : D c)
  : D c' := X _ _ f d.

Definition cleaving_mor {C : category} {D : disp_cat C}
           (X : cleaving D) {c c' : C} (f : c' --> c) (d : D c)
  : cleaving_ob X f d -->[f] d := X _ _ f d.

Definition is_split_id {C : category} {D : disp_cat C}
           (X : cleaving D) : UU
  := ∏ c (d : D c),
      ∑ e : cleaving_ob X (identity _) d = d,
            cleaving_mor X (identity _) d =
            transportb (λ x, x -->[ _ ] _ ) e (id_disp d).

Definition is_split_comp {C : category} {D : disp_cat C}
           (X : cleaving D) : UU
  :=
    ∏ (c c' c'' : C) (f : c' --> c) (g : c'' --> c') (d : D c),
      ∑ e : cleaving_ob X (g · f) d =
                cleaving_ob X g (cleaving_ob X f d),
            cleaving_mor X (g · f) d =
            transportb (λ x, x -->[ _ ] _ ) e
                       (cleaving_mor X g (cleaving_ob X f d) ;;
                                     cleaving_mor X f d).

Definition is_split {C : category} {D : disp_cat C}
           (X : cleaving D) : UU
  := is_split_id X × is_split_comp X × (∏ c, isaset (D c)).

Lemma is_split_fibration_from_discrete_fibration
      {C : category} {D : disp_cat C}
      (X : is_discrete_fibration D)
: is_split (fibration_from_discrete_fibration _ (D,,X)).
Show proof.
  repeat split.
  - intros c d.
    cbn.
    use tpair.
    + apply pathsinv0.
      apply path_to_ctr.
      apply id_disp.
    + cbn.
      apply (disp_mor_unique_disc_fib _ (D,,X)).
  - intros c c' c'' f g d.
    cbn.
    use tpair.
    + set (XR := unique_lift f d).
      set (d' := pr1 (iscontrpr1 XR)).
      set (f' := pr2 (iscontrpr1 XR)). cbn in f'.
      set (g' := pr2 (iscontrpr1 (unique_lift g d'))).
      cbn in g'.
      set (gf' := g' ;; f').
      match goal with |[ |- ?a = ?b ] =>
                       assert (X0 : (a,,pr2 (iscontrpr1 (unique_lift (g · f) d))) =
                                    (b,,gf')) end.

      { apply proofirrelevancecontr. apply X. }
      apply (maponpaths pr1 X0).
    + apply (disp_mor_unique_disc_fib _ (D,,X)).
  - apply isaset_fiber_discrete_fibration.

Some standard cartesian cells
Definition is_cartesian_id_disp
           {C : category}
           {D : disp_cat C}
           {x : C}
           (xx : D x)
  : is_cartesian (id_disp xx).
Show proof.
  intros z g zz hh.
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros f₁ f₂ ;
       use subtypePath ; [ intro ; intros ; apply D | ] ;
       refine (id_right_disp_var _ @ _ @ !(id_right_disp_var _)) ;
       rewrite (pr2 f₁), (pr2 f₂) ;
       apply idpath).
  - use tpair.
    + exact (transportf _ (id_right _) hh).
    + abstract
        (simpl ;
         rewrite id_right_disp ;
         unfold transportb ;
         rewrite transport_f_f ;
         rewrite pathsinv0r ;
         apply idpath).

Definition is_cartesian_comp_disp
           {C : category}
           {D : disp_cat C}
           {x : C}
           {xx : D x}
           {y : C}
           {yy : D y}
           {z : C}
           {zz : D z}
           {f : x --> y} {g : y --> z}
           {ff : xx -->[ f ] yy} {gg : yy -->[ g ] zz}
           (Hff : is_cartesian ff) (Hgg : is_cartesian gg)
  : is_cartesian (ff ;; gg)%mor_disp.
Show proof.
  intros w h ww hh'.
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros f₁ f₂ ;
       use subtypePath ; [ intro ; apply D | ] ;
       use (cartesian_factorisation_unique Hff) ;
       use (cartesian_factorisation_unique Hgg) ;
       rewrite !assoc_disp_var ;
       rewrite (pr2 f₁), (pr2 f₂) ;
       apply idpath).
  - simple refine (_ ,, _).
    + exact (cartesian_factorisation
               Hff
               h
               (cartesian_factorisation
                  Hgg
                  (h · f)
                  (transportf
                     (λ z, _ -->[ z ] _)
                     (assoc _ _ _)
                     hh'))).
    + abstract
        (simpl ;
         rewrite assoc_disp ;
         rewrite !cartesian_factorisation_commutes ;
         unfold transportb ;
         rewrite transport_f_f ;
         apply transportf_set ;
         apply homset_property).

Definition is_cartesian_z_iso_disp
           {C : category}
           {D : disp_cat C}
           {x : C}
           {xx : D x}
           {y : C}
           {yy : D y}
           {f : x --> y}
           {Hf : is_z_isomorphism f}
           {ff : xx -->[ f ] yy}
           (Hff : is_z_iso_disp (make_z_iso' f Hf) ff)
  : is_cartesian ff.
Show proof.
  intros z g zz gf.
  use iscontraprop1.
  - abstract
      (apply invproofirrelevance ;
       intros φ₁ φ₂ ;
       use subtypePath ; [ intro ; apply D | ] ;
       pose (pr2 φ₁ @ !(pr2 φ₂)) as r ;
       refine (id_right_disp_var _ @ _ @ !(id_right_disp_var _)) ;
       pose (transportf_transpose_left (inv_mor_after_z_iso_disp Hff)) as r' ;
       rewrite <- !r' ; clear r' ;
       rewrite !mor_disp_transportf_prewhisker ;
       rewrite !assoc_disp ;
       unfold transportb ;
       rewrite !transport_f_f ;
       apply maponpaths ;
       apply maponpaths_2 ;
       exact r).
  - simple refine (_ ,, _).
    + refine (transportf
                (λ z, _ -->[ z ] _)
                _
                (gf ;; inv_mor_disp_from_z_iso Hff)%mor_disp).
      abstract
        (rewrite assoc' ;
         refine (_ @ id_right _) ;
         apply maponpaths ;
         apply (z_iso_inv_after_z_iso (make_z_iso' f Hf))).
    + abstract
        (simpl ;
         rewrite mor_disp_transportf_postwhisker ;
         rewrite assoc_disp_var ;
         rewrite transport_f_f ;
         etrans ;
           [ do 2 apply maponpaths ;
             apply (z_iso_disp_after_inv_mor Hff)
           | ] ;
         unfold transportb ;
         rewrite mor_disp_transportf_prewhisker ;
         rewrite transport_f_f ;
         rewrite id_right_disp ;
         unfold transportb ;
         rewrite transport_f_f ;
         apply transportf_set ;
         apply homset_property ;
         rewrite disp_id_right).

Definition is_cartesian_transportf
           {C : category}
           {D : disp_cat C}
           {x y : C}
           {f f' : x --> y}
           (p : f = f')
           {xx : D x}
           {yy : D y}
           {ff : xx -->[ f ] yy}
           (Hff : is_cartesian ff)
  : is_cartesian (transportf (λ z, _ -->[ z ] _) p ff).
Show proof.
  intros c g cc gg.
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros φ₁ φ₂ ;
       use subtypePath ; [ intro ; apply D | ] ;
       use (cartesian_factorisation_unique Hff) ;
       pose (p₁ := pr2 φ₁) ;
       pose (p₂ := pr2 φ₂) ;
       cbn in p₁, p₂ ;
       rewrite mor_disp_transportf_prewhisker in p₁ ;
       rewrite mor_disp_transportf_prewhisker in p₂ ;
       pose (transportb_transpose_right p₁) as r₁ ;
       pose (transportb_transpose_right p₂) as r₂ ;
       exact (r₁ @ !r₂)).
  - simple refine (_ ,, _).
    + exact (cartesian_factorisation
               Hff
               g
               (transportb
                  (λ z, _ -->[ z ] _)
                  (maponpaths (λ z, g · z) p)
                  gg)).
    + abstract
        (cbn ;
         rewrite mor_disp_transportf_prewhisker ;
         rewrite cartesian_factorisation_commutes ;
         unfold transportb ;
         rewrite transport_f_f ;
         apply transportf_set ;
         apply homset_property).

Definition is_cartesian_precomp
           {C : category}
           {D : disp_cat C}
           {x y z : C}
           {f : x --> y}
           {g : y --> z}
           {h : x --> z}
           {xx : D x}
           {yy : D y}
           {zz : D z}
           {ff : xx -->[ f ] yy}
           {gg : yy -->[ g ] zz}
           {hh : xx -->[ h ] zz}
           (p : h = f · g)
           (pp : (ff ;; gg = transportf (λ z, _ -->[ z ] _) p hh)%mor_disp)
           (Hgg : is_cartesian gg)
           (Hhh : is_cartesian hh)
  : is_cartesian ff.
Show proof.
  intros w φ ww φφ.
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros ψ₁ ψ₂ ;
       use subtypePath ; [ intro ; apply D | ] ;
       use (cartesian_factorisation_unique Hhh) ;
       rewrite <- (transportb_transpose_left pp) ;
       unfold transportb ;
       rewrite !mor_disp_transportf_prewhisker ;
       rewrite !assoc_disp ;
       rewrite (pr2 ψ₁), (pr2 ψ₂) ;
       apply idpath).
  - simple refine (_ ,, _).
    + refine (cartesian_factorisation
                Hhh
                φ
                (transportf (λ z, _ -->[ z ] _) _ (φφ ;; gg)%mor_disp)).
      abstract
        (rewrite p ;
         rewrite assoc ;
         apply idpath).
    + abstract
        (simpl ;
         use (cartesian_factorisation_unique Hgg) ;
         rewrite assoc_disp_var ;
         rewrite pp ;
         rewrite mor_disp_transportf_prewhisker ;
         rewrite transport_f_f ;
         rewrite cartesian_factorisation_commutes ;
         rewrite transport_f_f ;
         apply transportf_set ;
         apply homset_property).

Definition z_iso_disp_to_is_cartesian
           {C : category}
           {D : disp_cat C}
           {x y z : C}
           {f : x --> z}
           {g : y --> z}
           {h : y --> x}
           (Hh : is_z_isomorphism h)
           {p : h · f = g}
           {xx : D x}
           {yy : D y}
           {zz : D z}
           {ff : xx -->[ f ] zz}
           {gg : yy -->[ g ] zz}
           {hh : yy -->[ h ] xx}
           (Hff : is_cartesian ff)
           (Hhh : is_z_iso_disp (make_z_iso' h Hh) hh)
           (pp : (hh ;; ff = transportb _ p gg)%mor_disp)
  : is_cartesian gg.
Show proof.
  intros q k qq kg.
  assert (f = inv_from_z_iso (make_z_iso' h Hh) · g) as r.
  {
    abstract
      (refine (!_) ;
       use z_iso_inv_on_right ;
       exact (!p)).
  }
  assert (transportf (λ z, _ -->[ z ] _) r ff
          =
          inv_mor_disp_from_z_iso Hhh ;; gg)%mor_disp as rr.
  {
    abstract
      (rewrite <- (transportb_transpose_left pp) ;
       unfold transportb ;
       rewrite mor_disp_transportf_prewhisker ;
       rewrite assoc_disp ;
       refine (!_) ;
       etrans ;
       [ do 2 apply maponpaths ;
         apply maponpaths_2 ;
         exact (z_iso_disp_after_inv_mor Hhh)
       | ] ;
       unfold transportb ;
       rewrite mor_disp_transportf_postwhisker ;
       rewrite id_left_disp ;
       unfold transportb ;
       rewrite !transport_f_f ;
       apply maponpaths_2 ;
       apply homset_property).
  }
  use iscontraprop1.
  - abstract
      (use invproofirrelevance ;
       intros φ₁ φ₂ ;
       use subtypePath ; [ intro ; apply D | ] ;
       use (postcomp_with_z_iso_disp_is_inj Hh (idpath _) Hhh) ; cbn ;
       use (cartesian_factorisation_unique Hff) ;
       rewrite !assoc_disp_var ;
       rewrite pp ;
       unfold transportb ;
       rewrite !mor_disp_transportf_prewhisker ;
       rewrite !transport_f_f ;
       apply maponpaths ;
       exact (pr2 φ₁ @ !(pr2 φ₂))).
  - simple refine (_ ,, _).
    + refine (transportf
                (λ z, _ -->[ z ] _)
                _
                (cartesian_factorisation
                   Hff
                   (k · h)
                   (transportf
                      (λ z, _ -->[ z ] _)
                      _
                      kg)
                 ;; inv_mor_disp_from_z_iso Hhh)%mor_disp).
      * abstract
          (rewrite assoc' ;
           etrans ; [ apply maponpaths ; apply (z_iso_inv_after_z_iso (make_z_iso' h Hh)) | ] ;
           apply id_right).
      * abstract
          (rewrite assoc' ;
           rewrite p ;
           apply idpath).
    + abstract
        (simpl ;
         rewrite mor_disp_transportf_postwhisker ;
         rewrite assoc_disp_var ;
         etrans ; [ do 3 apply maponpaths ; exact (!rr) | ] ;
         rewrite transport_f_f ;
         rewrite mor_disp_transportf_prewhisker ;
         rewrite cartesian_factorisation_commutes ;
         rewrite !transport_f_f ;
         apply transportf_set ;
         apply homset_property).

Definition is_opcartesian_id_disp
           {C : category}
           {D : disp_cat C}
           {x : C}
           (xx : D x)
  : is_opcartesian (id_disp xx).
Show proof.
  apply is_cartesian_to_is_opcartesian.
  exact (@is_cartesian_id_disp _ (op_disp_cat D) _ xx).

Definition is_opcartesian_comp_disp
           {C : category}
           {D : disp_cat C}
           {x : C}
           {xx : D x}
           {y : C}
           {yy : D y}
           {z : C}
           {zz : D z}
           {f : x --> y} {g : y --> z}
           {ff : xx -->[ f ] yy} {gg : yy -->[ g ] zz}
           (Hff : is_opcartesian ff) (Hgg : is_opcartesian gg)
  : is_opcartesian (ff ;; gg)%mor_disp.
Show proof.
  apply is_cartesian_to_is_opcartesian.
  use (@is_cartesian_comp_disp _ (op_disp_cat D)).
  - apply is_opcartesian_weq_is_cartesian.
    exact Hgg.
  - apply is_opcartesian_weq_is_cartesian.
    exact Hff.

Definition is_opcartesian_postcomp
           {C : category}
           {D : disp_cat C}
           {x y z : C}
           {f : x --> y}
           {g : y --> z}
           {h : x --> z}
           {xx : D x}
           {yy : D y}
           {zz : D z}
           {ff : xx -->[ f ] yy}
           {gg : yy -->[ g ] zz}
           {hh : xx -->[ h ] zz}
           (p : h = f · g)
           (pp : (ff ;; gg = transportf (λ z, _ -->[ z ] _) p hh)%mor_disp)
           (Hff : is_opcartesian ff)
           (Hhh : is_opcartesian hh)
  : is_opcartesian gg.
Show proof.
  apply is_cartesian_to_is_opcartesian.
  use (@is_cartesian_precomp _ (op_disp_cat D) _ _ _ g f h zz yy xx gg ff hh p pp).
  - apply is_opcartesian_weq_is_cartesian.
    exact Hff.
  - apply is_opcartesian_weq_is_cartesian.
    exact Hhh.

Definition is_opcartesian_z_iso_disp
           {C : category}
           {D : disp_cat C}
           {x : C}
           {xx : D x}
           {y : C}
           {yy : D y}
           {f : x --> y}
           {Hf : is_z_isomorphism f}
           {ff : xx -->[ f ] yy}
           (Hff : is_z_iso_disp (make_z_iso' f Hf) ff)
  : is_opcartesian ff.
Show proof.
  apply is_cartesian_to_is_opcartesian.
  use (@is_cartesian_z_iso_disp _ (op_disp_cat D) _ _ _ _ _ _ ff).
  - exact (pr2 (@opp_z_iso C _ _ (make_z_iso' f Hf))).
  - use (@to_z_iso_disp_op_disp_cat C D y x (make_z_iso' f Hf) yy xx ff).
    exact Hff.

Definition is_opcartesian_transportf
           {C : category}
           {D : disp_cat C}
           {x y : C}
           {f f' : x --> y}
           (p : f = f')
           {xx : D x}
           {yy : D y}
           {ff : xx -->[ f ] yy}
           (Hff : is_opcartesian ff)
  : is_opcartesian (transportf (λ z, _ -->[ z ] _) p ff).
Show proof.
  apply is_cartesian_to_is_opcartesian.
  apply (@is_cartesian_transportf _ (op_disp_cat D)).
  apply is_opcartesian_weq_is_cartesian.
  exact Hff.

Cartesian factorisation of disp nat trans and functor
Section CartesianFactorisationDispNatTrans.
  Context {C₁ C₂ : category}
          {F₁ F₂ F₃ : C₁ ⟶ C₂}
          {α : F₂ ⟹ F₃}
          {β : F₁ ⟹ F₂}
          {D₁ : disp_cat C₁}
          {D₂ : disp_cat C₂}
          {FF₁ : disp_functor F₁ D₁ D₂}
          {FF₂ : disp_functor F₂ D₁ D₂}
          {FF₃ : disp_functor F₃ D₁ D₂}
          (αα : disp_nat_trans α FF₂ FF₃)
          (ββ : disp_nat_trans (nat_trans_comp _ _ _ β α) FF₁ FF₃)
          (Hαα : ∏ (x : C₁) (xx : D₁ x), is_cartesian (αα x xx)).

  Definition cartesian_factorisation_disp_nat_trans_data
    : disp_nat_trans_data β FF₁ FF₂
    := λ x xx, cartesian_factorisation (Hαα x xx) (β x) (ββ x xx).

  Definition cartesian_factorisation_disp_nat_trans_axioms
    : disp_nat_trans_axioms cartesian_factorisation_disp_nat_trans_data.
  Show proof.
    intros x y f xx yy ff ; cbn in *.
    unfold cartesian_factorisation_disp_nat_trans_data.
    use (cartesian_factorisation_unique (Hαα y yy)).
    rewrite assoc_disp_var.
    rewrite cartesian_factorisation_commutes.
    refine (maponpaths _ (disp_nat_trans_ax ββ ff) @ _).
    unfold transportb.
    rewrite !transport_f_f.
    rewrite mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    refine (!_).
    etrans.
    {
      do 2 apply maponpaths.
      exact (disp_nat_trans_ax αα ff).
    }
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite assoc_disp.
    unfold transportb.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    apply maponpaths_2.
    apply homset_property.

  Definition cartesian_factorisation_disp_nat_trans
    : disp_nat_trans β FF₁ FF₂.
  Show proof.
    simple refine (_ ,, _).
    - exact cartesian_factorisation_disp_nat_trans_data.
    - exact cartesian_factorisation_disp_nat_trans_axioms.
End CartesianFactorisationDispNatTrans.

Section CartesianFactorisationDispFunctor.
  Context {C₁ C₂ : category}
          {D₁ : disp_cat C₁}
          {D₂ : disp_cat C₂}
          (HD₁ : cleaving D₂)
          {F G : C₁ ⟶ C₂}
          (GG : disp_functor G D₁ D₂)
          (α : F ⟹ G).

  Definition cartesian_factorisation_disp_functor_data
    : disp_functor_data F D₁ D₂.
  Show proof.
    simple refine (_ ,, _).
    - exact (λ x xx, pr1 (HD₁ (G x) (F x) (α x) (GG x xx))).
    - exact (λ x y xx yy f ff,
             cartesian_factorisation
               (pr22 (HD₁ (G y) (F y) (α y) (GG y yy)))
               _
               (transportb
                  (λ z, _ -->[ z ] _)
                  (nat_trans_ax α _ _ f)
                  (pr12 (HD₁ (G x) (F x) (α x) (GG x xx)) ;; ♯ GG ff))).

  Definition cartesian_factorisation_disp_functor_axioms
    : disp_functor_axioms cartesian_factorisation_disp_functor_data.
  Show proof.
    repeat split.
    - intros x xx ; cbn.
      use (cartesian_factorisation_unique
             (pr22 (HD₁ (G x) (F x) (α x) (GG x xx)))).
      rewrite cartesian_factorisation_commutes.
      rewrite disp_functor_id.
      unfold transportb.
      rewrite mor_disp_transportf_prewhisker.
      rewrite transport_f_f.
      rewrite id_right_disp.
      unfold transportb.
      rewrite transport_f_f.
      rewrite mor_disp_transportf_postwhisker.
      rewrite id_left_disp.
      unfold transportb.
      rewrite transport_f_f.
      apply maponpaths_2.
      apply homset_property.
    - intros x y z xx yy zz f g ff hh ; cbn.
      use (cartesian_factorisation_unique
             (pr22 (HD₁ (G z) (F z) (α z) (GG z zz)))).
      unfold transportb.
      rewrite cartesian_factorisation_commutes.
      rewrite disp_functor_comp.
      unfold transportb.
      rewrite mor_disp_transportf_prewhisker.
      rewrite transport_f_f.
      rewrite mor_disp_transportf_postwhisker.
      rewrite assoc_disp_var.
      rewrite transport_f_f.
      rewrite cartesian_factorisation_commutes.
      rewrite mor_disp_transportf_prewhisker.
      rewrite transport_f_f.
      rewrite !assoc_disp.
      unfold transportb.
      rewrite transport_f_f.
      rewrite cartesian_factorisation_commutes.
      rewrite mor_disp_transportf_postwhisker.
      rewrite !transport_f_f.
      apply maponpaths_2.
      apply homset_property.

  Definition cartesian_factorisation_disp_functor
    : disp_functor F D₁ D₂.
  Show proof.
    simple refine (_ ,, _).
    - exact cartesian_factorisation_disp_functor_data.
    - exact cartesian_factorisation_disp_functor_axioms.

  Definition cartesian_factorisation_disp_functor_is_cartesian
             (HGG : is_cartesian_disp_functor GG)
    : is_cartesian_disp_functor cartesian_factorisation_disp_functor.
  Show proof.
    intros x y f xx yy ff Hff ; cbn.
    pose (HGff := HGG _ _ _ _ _ _ Hff).
    refine (is_cartesian_precomp
              (idpath _)
              _
              (pr22 (HD₁ (G x) (F x) (α x) (GG x xx)))
              (is_cartesian_transportf
                 (!(nat_trans_ax α _ _ f))
                 (is_cartesian_comp_disp
                    (pr22 (HD₁ (G y) (F y) (α y) (GG y yy)))
                    HGff))).
    rewrite cartesian_factorisation_commutes.
    apply idpath.

  Definition cartesian_factorisation_disp_functor_cell_data
    : disp_nat_trans_data α cartesian_factorisation_disp_functor_data GG
    := λ x xx, pr12 (HD₁ (G x) (F x) (α x) (GG x xx)).

  Definition cartesian_factorisation_disp_functor_cell_axioms
    : disp_nat_trans_axioms cartesian_factorisation_disp_functor_cell_data.
  Show proof.
    intros x y f xx yy ff ; cbn ; unfold cartesian_factorisation_disp_functor_cell_data.
    unfold transportb.
    rewrite cartesian_factorisation_commutes.
    apply idpath.

  Definition cartesian_factorisation_disp_functor_cell
    : disp_nat_trans
        α
        cartesian_factorisation_disp_functor_data
        GG.
  Show proof.
    simple refine (_ ,, _).
    - exact cartesian_factorisation_disp_functor_cell_data.
    - exact cartesian_factorisation_disp_functor_cell_axioms.

  Definition cartesian_factorisation_disp_functor_cell_is_cartesian
             {x : C₁}
             (xx : D₁ x)
    : is_cartesian (cartesian_factorisation_disp_functor_cell x xx).
  Show proof.
    exact (pr22 (HD₁ (G x) (F x) (α x) (GG x xx))).
End CartesianFactorisationDispFunctor.

Cartesian factorisation of disp nat trans and functor
Section OpCartesianFactorisationDispNatTrans.
  Context {C₁ C₂ : category}
          {F₁ F₂ F₃ : C₁ ⟶ C₂}
          {α : F₁ ⟹ F₂}
          {β : F₂ ⟹ F₃}
          {D₁ : disp_cat C₁}
          {D₂ : disp_cat C₂}
          {FF₁ : disp_functor F₁ D₁ D₂}
          {FF₂ : disp_functor F₂ D₁ D₂}
          {FF₃ : disp_functor F₃ D₁ D₂}
          (αα : disp_nat_trans α FF₁ FF₂)
          (ββ : disp_nat_trans (nat_trans_comp _ _ _ α β) FF₁ FF₃)
          (Hαα : ∏ (x : C₁) (xx : D₁ x), is_opcartesian (αα x xx)).

  Definition opcartesian_factorisation_disp_nat_trans_data
    : disp_nat_trans_data β FF₂ FF₃
    := λ x xx, opcartesian_factorisation (Hαα x xx) (β x) (ββ x xx).

  Definition opcartesian_factorisation_disp_nat_trans_axioms
    : disp_nat_trans_axioms opcartesian_factorisation_disp_nat_trans_data.
  Show proof.
    intros x y f xx yy ff ; cbn in *.
    unfold opcartesian_factorisation_disp_nat_trans_data.
    use (opcartesian_factorisation_unique (Hαα x xx)).
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite !assoc_disp.
    unfold transportb.
    rewrite transport_f_f.
    rewrite opcartesian_factorisation_commutes.
    etrans.
    {
      apply maponpaths.
      apply maponpaths_2.
      apply (disp_nat_trans_ax_var αα ff).
    }
    rewrite mor_disp_transportf_postwhisker.
    rewrite transport_f_f.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    rewrite opcartesian_factorisation_commutes.
    etrans.
    {
      apply maponpaths.
      exact (disp_nat_trans_ax ββ ff).
    }
    unfold transportb.
    rewrite transport_f_f.
    apply maponpaths_2.
    apply homset_property.

  Definition opcartesian_factorisation_disp_nat_trans
    : disp_nat_trans β FF₂ FF₃.
  Show proof.
    simple refine (_ ,, _).
    - exact opcartesian_factorisation_disp_nat_trans_data.
    - exact opcartesian_factorisation_disp_nat_trans_axioms.
End OpCartesianFactorisationDispNatTrans.

Section OpCartesianFactorisationDispFunctor.
  Context {C₁ C₂ : category}
          {D₁ : disp_cat C₁}
          {D₂ : disp_cat C₂}
          (HD₁ : opcleaving D₂)
          {F G : C₁ ⟶ C₂}
          (FF : disp_functor F D₁ D₂)
          (α : F ⟹ G).

  Definition opcartesian_factorisation_disp_functor_data
    : disp_functor_data G D₁ D₂.
  Show proof.
    simple refine (_ ,, _).
    - exact (λ x xx, ob_of_opcartesian_lift _ (HD₁ (F x) (G x) (FF x xx) (α x))).
    - exact (λ x y xx yy f ff,
             opcartesian_factorisation
               (mor_of_opcartesian_lift_is_opcartesian
                  _
                  (HD₁ (F x) (G x) (FF x xx) (α x)))
               _
               (transportf
                  (λ z, _ -->[ z ] _)
                  (nat_trans_ax α _ _ f)
                  (♯ FF ff
                   ;;
                   mor_of_opcartesian_lift
                     _
                     (HD₁ (F y) (G y) (FF y yy) (α y))))).

  Definition opcartesian_factorisation_disp_functor_axioms
    : disp_functor_axioms opcartesian_factorisation_disp_functor_data.
  Show proof.
    repeat split.
    - intros x xx ; cbn.
      use (opcartesian_factorisation_unique
             (pr22 (HD₁ (F x) (G x) (FF x xx) (α x)))).
      rewrite opcartesian_factorisation_commutes.
      rewrite disp_functor_id.
      unfold transportb.
      rewrite mor_disp_transportf_prewhisker.
      rewrite id_right_disp.
      unfold transportb.
      rewrite transport_f_f.
      rewrite mor_disp_transportf_postwhisker.
      rewrite id_left_disp.
      unfold transportb.
      rewrite !transport_f_f.
      apply maponpaths_2.
      apply homset_property.
    - intros x y z xx yy zz f g ff hh ; cbn.
      use (opcartesian_factorisation_unique
             (pr22 (HD₁ (F x) (G x) (FF x xx) (α x)))).
      unfold transportb.
      rewrite opcartesian_factorisation_commutes.
      rewrite disp_functor_comp.
      unfold transportb.
      rewrite mor_disp_transportf_prewhisker.
      rewrite mor_disp_transportf_postwhisker.
      rewrite !transport_f_f.
      rewrite !assoc_disp.
      unfold transportb.
      rewrite !transport_f_f.
      rewrite opcartesian_factorisation_commutes.
      rewrite mor_disp_transportf_postwhisker.
      rewrite transport_f_f.
      rewrite !assoc_disp_var.
      unfold transportb.
      rewrite transport_f_f.
      rewrite opcartesian_factorisation_commutes.
      rewrite mor_disp_transportf_prewhisker.
      rewrite !transport_f_f.
      apply maponpaths_2.
      apply homset_property.

  Definition opcartesian_factorisation_disp_functor
    : disp_functor G D₁ D₂.
  Show proof.
    simple refine (_ ,, _).
    - exact opcartesian_factorisation_disp_functor_data.
    - exact opcartesian_factorisation_disp_functor_axioms.

  Definition opcartesian_factorisation_disp_functor_is_opcartesian
             (HFF : is_opcartesian_disp_functor FF)
    : is_opcartesian_disp_functor opcartesian_factorisation_disp_functor.
  Show proof.
    intros x y f xx yy ff Hff ; cbn.
    pose (HFff := HFF _ _ _ _ _ _ Hff).
    use (is_opcartesian_postcomp
           (idpath _)
           _
           (pr22 (HD₁ (F y) (G y) (FF y yy) (α y)))
           (is_opcartesian_transportf
              (nat_trans_ax α _ _ f)
              (is_opcartesian_comp_disp
                 HFff
                 (pr22 (HD₁ (F x) (G x) (FF x xx) (α x)))))).
    rewrite opcartesian_factorisation_commutes.
    apply idpath.

  Definition opcartesian_factorisation_disp_functor_cell_data
    : disp_nat_trans_data α FF opcartesian_factorisation_disp_functor_data
    := λ x xx, pr12 (HD₁ (F x) (G x) (FF x xx) (α x)).

  Definition opcartesian_factorisation_disp_functor_cell_axioms
    : disp_nat_trans_axioms opcartesian_factorisation_disp_functor_cell_data.
  Show proof.
    intros x y f xx yy ff ; cbn ; unfold opcartesian_factorisation_disp_functor_cell_data.
    unfold transportb.
    rewrite opcartesian_factorisation_commutes.
    rewrite transport_f_f.
    refine (!_).
    apply transportf_set.
    apply homset_property.

  Definition opcartesian_factorisation_disp_functor_cell
    : disp_nat_trans
        α
        FF
        opcartesian_factorisation_disp_functor_data.
  Show proof.
    simple refine (_ ,, _).
    - exact opcartesian_factorisation_disp_functor_cell_data.
    - exact opcartesian_factorisation_disp_functor_cell_axioms.

  Definition opcartesian_factorisation_disp_functor_cell_is_opcartesian
             {x : C₁}
             (xx : D₁ x)
    : is_opcartesian (opcartesian_factorisation_disp_functor_cell x xx).
  Show proof.
    exact (pr22 (HD₁ (F x) (G x) (FF x xx) (α x))).
End OpCartesianFactorisationDispFunctor.

Section fiber_functor_from_cleaving.

  Context {C : category} (D : disp_cat C) (F : cleaving D).
  Context {c c' : C} (f : C⟦c', c⟧).

  Let lift_f : ∏ d : D c, cartesian_lift d f := F _ _ f.

  Definition fiber_functor_from_cleaving_data : functor_data (D [{c}]) (D [{c'}]).
  Show proof.
    use tpair.
    + intro d. exact (object_of_cartesian_lift _ _ (lift_f d)).
    + intros d' d ff. cbn.

      set (XR' := @cartesian_factorisation C D _ _ f).
      specialize (XR' _ _ _ (lift_f d)).
      use XR'.
      * use (transportf (mor_disp _ _ )
                        _
                        (mor_disp_of_cartesian_lift _ _ (lift_f d') ;; ff)).
        etrans; [ apply id_right |]; apply pathsinv0; apply id_left.

  Lemma is_functor_from_cleaving_data : is_functor fiber_functor_from_cleaving_data.
  Show proof.
    split.
    - intro d; cbn.
      apply pathsinv0.
      apply path_to_ctr.
      etrans; [apply id_left_disp |].
      apply pathsinv0.
      etrans. { apply maponpaths. apply id_right_disp. }
      etrans; [ apply transport_f_f |].
      unfold transportb.
      apply maponpaths_2.
      apply homset_property.
    - intros d'' d' d ff' ff; cbn.
      apply pathsinv0.
      apply path_to_ctr.
      etrans; [apply mor_disp_transportf_postwhisker |].
      apply pathsinv0.
      etrans. { apply maponpaths; apply mor_disp_transportf_prewhisker. }
      etrans; [apply transport_f_f |].
      apply transportf_comp_lemma.
      apply pathsinv0.
      etrans; [apply assoc_disp_var |].
      apply pathsinv0.
      apply transportf_comp_lemma.
      apply pathsinv0.
      etrans ; [ apply maponpaths, cartesian_factorisation_commutes |].
      etrans ; [ apply mor_disp_transportf_prewhisker |].
      apply pathsinv0.
      apply transportf_comp_lemma.
      apply pathsinv0.
      etrans; [ apply assoc_disp |].
      apply pathsinv0.
      apply transportf_comp_lemma.
      apply pathsinv0.
      etrans; [ apply maponpaths_2, cartesian_factorisation_commutes |].
      etrans; [ apply mor_disp_transportf_postwhisker |].
      etrans. { apply maponpaths. apply assoc_disp_var. }
      etrans. { apply transport_f_f. }
      apply maponpaths_2, homset_property.

  Definition fiber_functor_from_cleaving : D [{c}] ⟶ D [{c'}]
    := make_functor _ is_functor_from_cleaving_data.

End fiber_functor_from_cleaving.

Section Essential_Surjectivity.

  Definition fiber_functor_ess_split_surj
             {C C' : category} {D} {D'}
             {F : functor C C'} (FF : disp_functor F D D')
             (H : disp_functor_ff FF)
             {X : disp_functor_ess_split_surj FF}
             {Y : is_op_isofibration D}
             
             (x : C)
    : ∏ yy : D'[{F x}], ∑ xx : D[{x}],
          z_iso (fiber_functor FF _ xx) yy.
  Show proof.
    intro yy.
    set (XR := X _ yy).
    destruct XR as [c'' [i [xx' ii]]].
    set (YY := Y _ _ i xx').
    destruct YY as [ dd pe ].
    use tpair.
    - apply dd.
    -
      set (XR := disp_functor_on_z_iso_disp FF pe).
      set (XR' := z_iso_inv_from_z_iso_disp XR).
      apply (invweq (z_iso_disp_z_iso_fiber _ _ _ _)).
      set (XRt := z_iso_disp_comp XR' ii).
      transparent assert (XH :
                           (z_iso_comp (z_iso_inv_from_z_iso (functor_on_z_iso F i))
                                     (functor_on_z_iso F i) = identity_z_iso _ )).
      { apply z_iso_eq. cbn.
        etrans.
        { apply pathsinv0, functor_comp. }
        apply functor_id_id.
        apply z_iso_after_z_iso_inv.
      }
      set (XRT := transportf (λ r, z_iso_disp r (FF x dd) yy )
                             XH).
      apply XRT.
      assumption.

End Essential_Surjectivity.

A sufficient condition for when a cartesian factorization is an isomorphism
Definition is_z_iso_disp_cartesian_factorisation
           {C : category}
           {D : disp_cat C}
           {w x y : C}
           {f : w --> x}
           (Hf : is_z_isomorphism f)
           (fiso := (f ,, Hf) : z_iso w x)
           {g : x --> y}
           (Hg : is_z_isomorphism g)
           (giso := (g ,, Hg) : z_iso x y)
           {ww : D w}
           {xx : D x}
           {yy : D y}
           {gg : xx -->[ g ] yy}
           (Hgg : is_cartesian gg)
           (hh : ww -->[ f · g ] yy)
           (Hhh : is_z_iso_disp (z_iso_comp fiso giso) hh)
  : is_z_iso_disp
      fiso
      (cartesian_factorisation Hgg f hh).
Show proof.
  simple refine (_ ,, _ ,, _).
  - refine (transportf
              (λ z, _ -->[ z ] _)
              _
              (gg ;; inv_mor_disp_from_z_iso Hhh)%mor_disp).
    abstract
      (cbn ;
       rewrite !assoc ;
       refine (_ @ id_left _) ;
       apply maponpaths_2 ;
       exact (z_iso_inv_after_z_iso giso)).
  - use (cartesian_factorisation_unique Hgg).
    rewrite mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite !mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite !transport_f_f.
    rewrite assoc_disp_var.
    rewrite !mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    etrans ;
      [ do 2 apply maponpaths ;
        apply (z_iso_disp_after_inv_mor Hhh)
      | ].
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite id_right_disp.
    rewrite mor_disp_transportf_postwhisker.
    rewrite id_left_disp.
    unfold transportb.
    rewrite !transport_f_f.
    apply maponpaths_2.
    apply homset_property.
  - cbn.
    rewrite mor_disp_transportf_prewhisker.
    rewrite assoc_disp.
    unfold transportb.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    refine (maponpaths _ (inv_mor_after_z_iso_disp Hhh) @ _).
    unfold transportb.
    rewrite transport_f_f.
    apply maponpaths_2.
    apply homset_property.

The fiber functor of the identity
Section FiberFunctorCleavingIdenttiy.
  Context {C : category}
          {D : disp_cat C}
          (HD : cleaving D)
          (x : C).

  Definition fiber_functor_from_cleaving_identity_data
    : nat_trans_data
        (functor_identity _)
        (fiber_functor_from_cleaving D HD (identity x)).
  Show proof.
    intros xx.
    refine (cartesian_factorisation
              (cartesian_lift_is_cartesian _ _ (HD x x (identity x) xx))
              (identity x)
              (transportb
                 (λ z, _ -->[ z ] _)
                 _
                 (id_disp _))).
    abstract (exact (id_left _)).

  Proposition fiber_functor_from_cleaving_identity_laws
    : is_nat_trans
        _ _
        fiber_functor_from_cleaving_identity_data.
  Show proof.
    intros xx yy f ; cbn.
    unfold fiber_functor_from_cleaving_identity_data.
    use (cartesian_factorisation_unique (HD x x (identity x) yy)).
    rewrite !mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite !transport_f_f.
    rewrite id_right_disp.
    unfold transportb.
    rewrite transport_f_f.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_prewhisker.
    rewrite !transport_f_f.
    rewrite assoc_disp.
    unfold transportb.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_postwhisker.
    rewrite transport_f_f.
    rewrite id_left_disp.
    unfold transportb.
    rewrite transport_f_f.
    apply maponpaths_2.
    apply homset_property.

  Definition fiber_functor_from_cleaving_identity
    : functor_identity _
      ⟹
      fiber_functor_from_cleaving D HD (identity x).
  Show proof.
    use make_nat_trans.
    - exact fiber_functor_from_cleaving_identity_data.
    - exact fiber_functor_from_cleaving_identity_laws.

  Definition is_nat_z_iso_fiber_functor_from_cleaving_identity
    : is_nat_z_iso fiber_functor_from_cleaving_identity.
  Show proof.
    intros xx ; cbn.
    use is_z_iso_fiber_from_is_z_iso_disp.
    use is_z_iso_disp_cartesian_factorisation.
    {
      apply is_z_isomorphism_identity.
    }
    cbn in x.
    use (is_z_iso_disp_transportb_fun_eq
           (identity_z_iso x)
           (id_disp xx)).
    apply id_is_z_iso_disp.
End FiberFunctorCleavingIdenttiy.

Arguments fiber_functor_from_cleaving_identity_data {C D} HD x /.

The fiber functor of a compositio
Section FiberFunctorCleavingComp.
  Context {C : category}
          {D : disp_cat C}
          (HD : cleaving D)
          {x y z : C}
          (f : y --> x)
          (g : z --> y).

  Definition fiber_functor_from_cleaving_comp_data
    : nat_trans_data
        (fiber_functor_from_cleaving D HD f ∙ fiber_functor_from_cleaving D HD g)
        (fiber_functor_from_cleaving D HD (g · f)).
  Show proof.
    intros xx.
    refine (cartesian_factorisation
              (cartesian_lift_is_cartesian _ _ (HD x z (g · f) xx))
              _
              (transportb
                 (λ z, _ -->[ z ] _)
                 _
                 (HD y z g (HD x y f xx) ;; HD x y f xx)%mor_disp)).
    abstract
      (exact (id_left _)).

  Proposition fiber_functor_from_cleaving_comp_laws
    : is_nat_trans
        _ _
        fiber_functor_from_cleaving_comp_data.
  Show proof.
    intros xx yy gg ; cbn.
    unfold fiber_functor_from_cleaving_comp_data.
    use (cartesian_factorisation_unique (HD _ _ _ _)).
    rewrite !mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite !transport_f_f.
    rewrite cartesian_factorisation_commutes.
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite assoc_disp.
    unfold transportb.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_postwhisker.
    rewrite transport_f_f.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    refine (!_).
    rewrite assoc_disp.
    unfold transportb.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_postwhisker.
    rewrite transport_f_f.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    apply maponpaths_2.
    apply homset_property.

  Definition fiber_functor_from_cleaving_comp
    : fiber_functor_from_cleaving D HD f ∙ fiber_functor_from_cleaving D HD g
      ⟹
      fiber_functor_from_cleaving D HD (g · f).
  Show proof.
    use make_nat_trans.
    - exact fiber_functor_from_cleaving_comp_data.
    - exact fiber_functor_from_cleaving_comp_laws.

  Definition fiber_functor_from_cleaving_comp_inv
             (xx : D x)
    : D[{z}] ⟦ pr1 (HD x z (g · f) xx) , pr1 (HD y z g (HD x y f xx)) ⟧.
  Show proof.
    refine (cartesian_factorisation
              (HD y z g (HD x y f xx))
              _
              (cartesian_factorisation
                 (HD x y f xx)
                 _
                 (transportf
                    (λ z, _ -->[ z ] _)
                    _
                    (HD x z (g · f) xx)))).
    abstract
      (rewrite !assoc' ;
       rewrite id_left ;
       apply idpath).

  Proposition fiber_functor_from_cleaving_comp_inv_left
              (xx : D x)
    : fiber_functor_from_cleaving_comp xx · fiber_functor_from_cleaving_comp_inv xx
      =
      identity _.
  Show proof.
    cbn.
    unfold fiber_functor_from_cleaving_comp_data, fiber_functor_from_cleaving_comp_inv.
    unfold transportb.
    use (cartesian_factorisation_unique (HD _ _ _ _)).
    rewrite mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    use (cartesian_factorisation_unique (HD _ _ _ _)).
    rewrite mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite transport_f_f.
    rewrite id_left_disp.
    unfold transportb.
    rewrite mor_disp_transportf_postwhisker.
    apply maponpaths_2.
    apply homset_property.

  Proposition fiber_functor_from_cleaving_comp_inv_right
              (xx : D x)
    : fiber_functor_from_cleaving_comp_inv xx · fiber_functor_from_cleaving_comp xx
      =
      identity _.
  Show proof.
    cbn.
    unfold fiber_functor_from_cleaving_comp_data, fiber_functor_from_cleaving_comp_inv.
    unfold transportb.
    use (cartesian_factorisation_unique (HD _ _ _ _)).
    rewrite mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite assoc_disp.
    unfold transportb.
    rewrite transport_f_f.
    rewrite !cartesian_factorisation_commutes.
    rewrite transport_f_f.
    rewrite id_left_disp.
    unfold transportb.
    apply maponpaths_2.
    apply homset_property.

  Definition is_nat_z_iso_fiber_functor_from_cleaving_comp
    : is_nat_z_iso fiber_functor_from_cleaving_comp.
  Show proof.
    intros xx.
    use make_is_z_isomorphism.
    - cbn -[fiber_category].
      exact (fiber_functor_from_cleaving_comp_inv xx).
    - split.
      + exact (fiber_functor_from_cleaving_comp_inv_left xx).
      + exact (fiber_functor_from_cleaving_comp_inv_right xx).
End FiberFunctorCleavingComp.

Arguments fiber_functor_from_cleaving_comp_data {C D} HD {x y z} f g /.

The fiber functor of a cartesian functor is natural
Locate cartesian_disp_functor_on_cartesian.
Section FiberFunctorNatural.
  Context {C : category}
          {D₁ D₂ : disp_cat C}
          (HD₁ : cleaving D₁)
          (HD₂ : cleaving D₂)
          (F : cartesian_disp_functor (functor_identity C) D₁ D₂)
          {x y : C}
          (f : y --> x).

  Definition fiber_functor_natural_data
    : nat_trans_data
        (fiber_functor F x ∙ fiber_functor_from_cleaving D₂ HD₂ f)
        (fiber_functor_from_cleaving D₁ HD₁ f ∙ fiber_functor F y).
  Show proof.
    intro xx.
    refine (cartesian_factorisation
              (cartesian_disp_functor_on_cartesian F (HD₁ x y f xx))
              _
              (transportf
                 (λ z, _ -->[ z ] _)
                 _
                 (HD₂ x y f (F x xx)))).
    abstract
      (exact (!(id_left _))).
  Proposition fiber_functor_natural_laws
    : is_nat_trans
        _ _
        fiber_functor_natural_data.
  Show proof.
    intros xx yy ff.
    unfold fiber_functor_natural_data ; cbn.
    use (cartesian_factorisation_unique
           (cartesian_disp_functor_on_cartesian F (HD₁ _ _ _ _))).
    rewrite !mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite !transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite transport_f_f.
    refine (!_).
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    etrans.
    {
      do 2 apply maponpaths.
      refine (!_).
      apply (disp_functor_comp_var F).
    }
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite disp_functor_transportf.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite disp_functor_comp.
    unfold transportb.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite assoc_disp.
    unfold transportb.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_postwhisker.
    rewrite transport_f_f.
    apply maponpaths_2.
    apply homset_property.

  Definition fiber_functor_natural
    : fiber_functor F x ∙ fiber_functor_from_cleaving D₂ HD₂ f
      ⟹
      fiber_functor_from_cleaving D₁ HD₁ f ∙ fiber_functor F y.
  Show proof.
    use make_nat_trans.
    - exact fiber_functor_natural_data.
    - exact fiber_functor_natural_laws.

  Definition fiber_functor_natural_inv
             (xx : D₁ x)
    : F y (HD₁ x y f xx) -->[ identity y] pr1 (HD₂ x y f (F x xx)).
  Show proof.
    refine (cartesian_factorisation
              (HD₂ _ _ _ _)
              _
              (transportf
                 (λ z, _ -->[ z ] _)
                 _
                 (♯ F (pr12 (HD₁ x y f xx)))))%mor_disp.
    abstract
      (exact (!(id_left _))).

  Proposition fiber_functor_natural_inv_left
              (xx : D₁ x)
    : fiber_functor_natural xx · fiber_functor_natural_inv xx
      =
      identity _.
  Show proof.
    cbn.
    unfold fiber_functor_natural_data, fiber_functor_natural_inv ; cbn.
    use (cartesian_factorisation_unique (HD₂ _ _ _ _)).
    rewrite id_left_disp.
    rewrite mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite transport_f_f.
    unfold transportb.
    apply maponpaths_2.
    apply homset_property.

  Proposition fiber_functor_natural_inv_right
              (xx : D₁ x)
    : transportf
        (λ z, _ -->[ z ] _)
        (id_right (identity y))
        (fiber_functor_natural_inv xx ;; fiber_functor_natural_data xx)%mor_disp
      =
      id_disp _.
  Show proof.
    cbn.
    unfold fiber_functor_natural_data, fiber_functor_natural_inv ; cbn.
    use (cartesian_factorisation_unique
           (cartesian_disp_functor_on_cartesian F (HD₁ _ _ _ _))).
    rewrite id_left_disp.
    rewrite mor_disp_transportf_postwhisker.
    rewrite assoc_disp_var.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite mor_disp_transportf_prewhisker.
    rewrite transport_f_f.
    rewrite cartesian_factorisation_commutes.
    rewrite transport_f_f.
    unfold transportb.
    apply maponpaths_2.
    apply homset_property.

  Definition is_nat_z_iso_fiber_functor_natural
    : is_nat_z_iso fiber_functor_natural.
  Show proof.
    intros xx.
    use make_is_z_isomorphism.
    - exact (fiber_functor_natural_inv xx).
    - split.
      + exact (fiber_functor_natural_inv_left xx).
      + exact (fiber_functor_natural_inv_right xx).

  Definition fiber_functor_natural_nat_z_iso
    : nat_z_iso
        (fiber_functor F x ∙ fiber_functor_from_cleaving D₂ HD₂ f)
        (fiber_functor_from_cleaving D₁ HD₁ f ∙ fiber_functor F y).
  Show proof.
    use make_nat_z_iso.
    - exact fiber_functor_natural.
    - exact is_nat_z_iso_fiber_functor_natural.
End FiberFunctorNatural.

Arguments fiber_functor_natural_data {C D₁ D₂} HD₁ HD₂ F {x y} f /.

Lemma for composing `idtoiso` with a cartesian lift
Proposition idtoiso_disp_cartesian_lift
            {C : category}
            (D : disp_cat C)
            (HD : cleaving D)
            {x y : C}
            {f g : x --> y}
            (yy : D y)
            (p : g = f)
  : (idtoiso_disp
       (idpath _)
       (maponpaths (λ (h : x --> y), pr1 (HD _ _ h _)) p)
     ;; HD y x f yy
    =
    transportf
      (λ z, _ -->[ z ] _)
      (p @ !(id_left _))
      (HD y x g yy))%mor_disp.
Show proof.
  induction p ; cbn.
  rewrite id_left_disp.
  apply idpath.

Transporting the object of a cartesian lift
Proposition transportf_object_cartesian_lift
            {C : category}
            {D : disp_cat C}
            (HD : cleaving D)
            {x : C}
            (xx : D x)
            {f g : x --> x}
            (p : f = g)
            (ff : xx -->[ identity x ] object_of_cartesian_lift _ _ (HD x x f xx))
  : transportf
      (λ (h : x --> x),
      _ -->[ identity x ] object_of_cartesian_lift _ _ (HD x x h xx))
      p
      ff
    =
    cartesian_factorisation
      (HD x x g xx)
      _
      (ff ;; transportf (λ z, _ -->[ z ] _) p (HD x x f xx))%mor_disp.
Show proof.
  induction p ; cbn.
  use (cartesian_factorisation_unique (HD x x f xx)).
  rewrite cartesian_factorisation_commutes.
  apply idpath.