Definition GlobalRan (H : GlobalRightKanExtensionExists) : [C, E] ⟶ [D, E] := right_adjoint H. End RightKanExtension. Section RightKanExtensionFromLims. Context (M C A : category) (K : functor M C) (LA : Lims A). Local Notation "c ↓ K" := (cComma _ _ K c) (at level 30). Section fix_T. Variable (T : functor M A). Local Definition Q (c : C) : functor (c ↓ K) M := cComma_pr1 _ _ K c. Local Definition QT (c : C) : diagram (c ↓ K) A := diagram_from_functor _ _ (functor_composite (Q c) T). Local Definition R (c : C) : A := lim (LA _ (QT c)). Local Definition lambda (c : C) : cone (QT c) (R c) := limCone (LA _ (QT c)). Local Definition Rmor_cone (c c' : C) (g : C⟦c,c'⟧) : cone (QT c') (R c). Proof. use make_cone. - intro m1f1. transparent assert (m1gf1 : (c ↓ K)). { use tpair. + apply (pr1 m1f1). + apply (g · pr2 m1f1). } exact (coneOut (lambda c) m1gf1). - intros x y f; simpl in *. transparent assert (e : ((c ↓ K) ⟦ pr1 x,, g · pr2 x, pr1 y,, g · pr2 y ⟧)). { use tpair. + exact (pr1 f). + change (g · pr2 x · # K (pr1 f) = g · pr2 y). rewrite <- assoc. rewrite (pr2 f). apply idpath. } exact (coneOutCommutes (lambda c) _ _ e). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.CommaCategories. Section RightKanExtensionFromLims. End RightKanExtensionFromLims.