proposition: Proposition terminal_mor_factorization_eq {x y : C} {f : x --> x} (p : identity _ = f) {g g' : x --> y} (q : g = g') {xx : D x} (ff : xx -->[ f ] pr1 (HD y x g (terminal_obj_in_fib T y))) (gg : xx -->[ g' ] terminal_obj_in_fib T y) : (ff ;; HD y x g (terminal_obj_in_fib T y))%mor_disp = transportb (λ z, _ -->[ z ] _) (maponpaths (λ z, z · _) (!p) @ id_left _ @ q) gg.
proof: Proof. induction p, q. refine (_ @ cartesian_factorisation_commutes (pr22 (HD y x g (terminal_obj_in_fib T y))) _ _). apply maponpaths_2. apply (TerminalArrowEq (T := lift_terminal_in_fib T g)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Preservation