Definition comp_coslice_precat {a b c : coslice_precat_ob_mor} (f : a --> b) (g : b --> c) : a --> c. Proof. use tpair. - exact (coslicecat_mor_morphism f · coslicecat_mor_morphism g). - abstract (refine (assoc _ _ _ @ _); refine (maponpaths (λ f, f · _) (coslicecat_mor_comm f) @ _); refine (coslicecat_mor_comm g)). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.