proposition: Lemma pr1_preserves_limit (d : diagram J (total_category D)) (x : total_category D) (CC : cone d x) : preserves_limit π _ x CC.
proof: Proof. intro H1. set (XR := X (mapdiagram π d)). use is_z_iso_isLim. - apply X. - match goal with |[ |- is_z_isomorphism ?foo ] => set (T:= foo) end. destruct X as [[a L] isL]. cbn in isL. set (tL := H _ _ (make_LimCone _ _ _ isL)). clear XR. unfold creates_limit in tL. set (RR := pr1 tL). set (RT1 := pr2 tL). set (RX := isLim_is_z_iso _ (make_LimCone _ _ _ RT1) _ _ H1). set (XR := @functor_on_is_z_isomorphism _ _ π _ _ _ RX). match goal with |[ H : is_z_isomorphism ?f |- _ ] => set (T':= f) end. assert (X0 : T' = T). { clear XR. clear RX. unfold T. unfold T'. apply (limArrowUnique (make_LimCone _ _ _ isL)) . intro j. set (RRt := make_LimCone _ _ _ RT1). set (RRtt := limArrowCommutes RRt x CC j). set (RH := maponpaths (#π) RRtt). cbn in RH. apply RH. } rewrite <- X0. apply XR. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions