Lemma LimFunctorCone (A C : category) (g : graph) (D : diagram g [A, C]^op) (HC : ∏ a : A^op, LimCone _ (diagram_pointwise (get_diagram A C g D) a)) : LimCone _ D. Proof. set (HColim := ColimFunctorCocone (get_diagram _ _ _ D) HC). destruct HColim as [pr1x pr2x]. destruct pr1x as [pr1pr1x pr2pr1x]. destruct pr2pr1x as [pr1pr2pr1x pr2pr2pr1x]. simpl in *. use (make_ColimCocone _ (from_op_op_to_op _ _ pr1pr1x)). - use make_cocone. + simpl; intros. use tpair. * intro a; apply (pr1pr2pr1x v a). * abstract (intros a b f; apply pathsinv0, (nat_trans_ax (pr1pr2pr1x v) )). + abstract (intros u v e; apply (nat_trans_eq C); simpl; intro a; now rewrite <- (pr2pr2pr1x u v e)). - intros F ccF. set (H := pr2x (from_opp_to_opp_opp _ _ _ F) (get_cocone _ _ _ _ _ ccF)). destruct H as [H1 H2]. destruct H1 as [α Hα]. simpl in *. use tpair. + use tpair. * exists α. abstract (intros a b f; simpl; now apply pathsinv0, (nat_trans_ax α b a f)). * abstract (intro u; apply (nat_trans_eq C); intro a; destruct ccF as [t p]; apply (toforallpaths _ _ _ (maponpaths pr1 (Hα u)) a)). + intro H; destruct H as [f Hf]; apply subtypePath. * abstract (intro β; repeat (apply impred; intro); now apply (has_homsets_opp (functor_category_has_homsets A C C))). * match goal with |[ H2 : ∏ _ : ?TT , _ = _ ,,_ |- _ ] => transparent assert (T : TT) end. { use (tpair _ (tpair _ (pr1 f) _)); simpl. - abstract (intros x y fxy; apply pathsinv0, (pr2 f y x fxy)). - abstract (intro u; apply (nat_trans_eq (has_homsets_opp C)); intro x; destruct ccF as [t p]; apply (toforallpaths _ _ _ (maponpaths pr1 (Hf u)) x)). } set (T' := maponpaths pr1 (H2 T)); simpl in T'. apply (nat_trans_eq C); intro a; simpl. now rewrite <- T'. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Import UniMath.CategoryTheory.opp_precat.