Definition disp_arrow_data : disp_cat_data (cartesian C C). Proof. use tpair. - use tpair. + intro H. exact (pr1 H --> pr2 H). + cbn. intros xy ab f g h. exact (compose f (pr2 h) = compose (pr1 h) g ). - split. + abstract ( intros; apply pathsinv0; refine (id_left xx @ _); refine (!id_right xx @ _); apply maponpaths, pathsinv0; apply (eqtohomot (transportf_const _ (C⟦_, _⟧))) ). + abstract ( intros; refine (maponpaths (λ x, _ (x _)) (transportf_const _ (C⟦_, _⟧)) @ _); refine (assoc _ _ _ @ _); refine (maponpaths_2 _ X _ @ _); refine (!assoc _ _ _ @ _); refine (maponpaths _ X0 @ _); apply assoc ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Examples. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.DisplayedCats.Limits. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.