Lemma pr1_preserves_limit (d : diagram J (total_category D)) (x : total_category D) (CC : cone d x) : preserves_limit π _ x CC. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.