proposition: Lemma comp_disp_cartesian (D := disp_cartesian) {c c' c'' : C} {F : C⟦c, c'⟧} {F' : C⟦c', c''⟧} {A : D c} {A' : D c'} {A'' : D c''} (G : A -->[F] A') (G' : A' -->[F'] A'') : (G ;; G') = G · G'.
proof: Proof. unfold comp_disp. simpl. unfold transportb. rewrite transportf_set. - apply idpath. - apply isasetaprop, isasetunit. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Examples UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing UniMath.CategoryTheory.DisplayedCats.Examples.Sigma UniMath.CategoryTheory.DisplayedCats.Limits UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Fiber