Definition arrow_disp : disp_cat arrow_base. Proof. use disp_cat_from_SIP_data. - exact (λ xy, pr1 xy --> pr2 xy). - simpl. intros xx' yy' g h ff'. exact (pr1 ff' · h = g · pr2 ff'). - abstract ( intros; use homset_property ). - abstract ( simpl; intros; now rewrite id_left, id_right ). - abstract ( simpl; intros; rewrite assoc, <- X; symmetry; now rewrite <- assoc, <- X0, assoc ). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.