Library UniMath.CategoryTheory.DisplayedCats.Fibrations

Definitions of various kinds of fibrations, using displayed categories.
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.

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.

#[reversible] 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 make_cartesian_disp_functor
           {C₁ C₂ : category}
           {F : C₁ C₂}
           {D₁ : disp_cat C₁}
           {D₂ : disp_cat C₂}
           (FF : disp_functor F D₁ D₂)
           (HFF : is_cartesian_disp_functor FF)
  : cartesian_disp_functor F D₁ D₂
  := FF ,, HFF.

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₁ C₂ : category}
           {F : C₁ C₂}
           {D₁ : disp_cat C₁}
           {D₂ : disp_cat C₂}
           (FF : cartesian_disp_functor F D₁ D₂)
           {x y : C₁}
           {f : x --> y}
           {xx : D₁ x}
           {yy : D₁ y}
           {ff : xx -->[ f ] yy}
           (Hff : is_cartesian ff)
  : is_cartesian (FF ff)
  := pr2 FF y x f yy xx ff Hff.

Definition id_cartesian_disp_functor
           {C : category}
           (D : disp_cat C)
  : cartesian_disp_functor (functor_identity C) D D.
Show proof.

Definition comp_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 : cartesian_disp_functor F D₁ D₂)
           (GG : cartesian_disp_functor G D₂ D₃)
  : cartesian_disp_functor (F G) D₁ D₃.
Show proof.
  use make_cartesian_disp_functor.
  - exact (disp_functor_composite FF GG).
  - exact (disp_functor_composite_is_cartesian_disp_functor
             (cartesian_disp_functor_is_cartesian FF)
             (cartesian_disp_functor_is_cartesian GG)).

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.

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.

#[reversible] 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.

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.

#[reversible] 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.

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.

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 : Cc', 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.

  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.

  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).

  Definition fiber_functor_from_cleaving_comp_nat_z_iso
    : nat_z_iso
        (fiber_functor_from_cleaving D HD f fiber_functor_from_cleaving D HD g)
        (fiber_functor_from_cleaving D HD (g · f)).
  Show proof.
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
Section FiberFunctorNatural.
  Context {C₁ C₂ : category}
          {F : C₁ C₂}
          {D₁ : disp_cat C₁}
          {D₂ : disp_cat C₂}
          (HD₁ : cleaving D₁)
          (HD₂ : cleaving D₂)
          (FF : cartesian_disp_functor F D₁ D₂)
          {x y : C₁}
          (f : y --> x).

  Definition fiber_functor_natural_data
    : nat_trans_data
        (fiber_functor FF x fiber_functor_from_cleaving D₂ HD₂ (#F f)%cat)
        (fiber_functor_from_cleaving D₁ HD₁ f fiber_functor FF y).
  Show proof.
    intro xx.
    refine (cartesian_factorisation
              (cartesian_disp_functor_on_cartesian FF (HD₁ x y f xx))
              _
              (transportf
                 (λ z, _ -->[ z ] _)
                 _
                 (HD₂ _ _ _ (FF 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 FF (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 !mor_disp_transportf_prewhisker.
    rewrite !mor_disp_transportf_postwhisker.
    rewrite !transport_f_f.
    etrans.
    {
      do 3 apply maponpaths.
      refine (!_).
      apply (disp_functor_comp_var FF).
    }
    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 FF x fiber_functor_from_cleaving D₂ HD₂ (#F f)%cat
      
      fiber_functor_from_cleaving D₁ HD₁ f fiber_functor FF 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)
    : FF y (HD₁ x y f xx) -->[ identity _ ] pr1 (HD₂ _ _ (#F f)%cat (FF x xx)).
  Show proof.
    refine (cartesian_factorisation
              (HD₂ _ _ _ _)
              _
              (transportf
                 (λ z, _ -->[ z ] _)
                 _
                 (FF (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 _)
        (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 FF (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 FF x fiber_functor_from_cleaving D₂ HD₂ (#F f)%cat)
        (fiber_functor_from_cleaving D₁ HD₁ f fiber_functor FF y).
  Show proof