Library UniMath.CategoryTheory.IndexedCategories.CartesianToIndexedFunctor

1. The data
2. The laws
  Proposition cartesian_disp_functor_to_indexed_functor_laws
    : indexed_functor_laws
        cartesian_disp_functor_to_indexed_functor_data.
  Show proof.
    split.
    - intros x xx ; 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.
      unfold transportb.
      rewrite transport_f_f.
      refine (!_).
      etrans.
      {
        refine (!_).
        apply (disp_functor_comp_var F).
      }
      rewrite cartesian_factorisation_commutes.
      rewrite disp_functor_transportf.
      rewrite transport_f_f.
      rewrite disp_functor_id.
      unfold transportb.
      rewrite transport_f_f.
      apply maponpaths_2.
      apply homset_property.
    - intros x y z f g xx ; cbn.
      rewrite mor_disp_transportf_postwhisker.
      use (cartesian_factorisation_unique
             (cartesian_disp_functor_on_cartesian F (HD₁ _ _ _ _))).
      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 cartesian_factorisation_commutes.
      unfold transportb.
      rewrite transport_f_f.
      refine (!_).
      rewrite assoc_disp_var.
      rewrite transport_f_f.
      rewrite assoc_disp_var.
      rewrite transport_f_f.
      etrans.
      {
        do 3 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.
      etrans.
      {
        do 2 apply maponpaths.
        rewrite assoc_disp.
        apply idpath.
      }
      unfold transportb.
      rewrite mor_disp_transportf_prewhisker.
      rewrite transport_f_f.
      rewrite cartesian_factorisation_commutes.
      rewrite mor_disp_transportf_postwhisker.
      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.
      apply maponpaths_2.
      apply homset_property.

3. The indexed functor from a cartesian functor