proposition: Lemma RightKanExtension_from_limits : GlobalRightKanExtensionExists _ _ K A.
proof: Proof. unfold GlobalRightKanExtensionExists. use left_adjoint_from_partial. - apply R_functor. - apply eps. - intros T S α; simpl in *. transparent assert (cc : (∏ c, cone (QT T c) (S c))). { intro c. use make_cone. + intro mf; apply (# S (pr2 mf) · α (pr1 mf)). + abstract (intros fm fm' h; simpl; rewrite <- assoc; eapply pathscomp0; [apply maponpaths, (pathsinv0 (nat_trans_ax α _ _ (pr1 h)))|]; simpl; rewrite assoc, <- functor_comp; apply cancel_postcomposition, maponpaths, (pr2 h)). } transparent assert (σ : (∏ c, A ⟦ S c, R T c ⟧)). { intro c; apply (limArrow _ _ (cc c)). } set (lambda' := λ c' mf', limOut (LA (c' ↓ K) (QT T c')) mf'). assert (H : ∏ c c' (g : C ⟦ c, c' ⟧) (mf' : c' ↓ K), # S g · σ c' · lambda' _ mf' = σ c · Rmor T c c' g · lambda' _ mf'). { intros c c' g mf'. rewrite <- !assoc. apply pathsinv0; eapply pathscomp0. apply maponpaths, (limArrowCommutes _ _ (Rmor_cone T c c' g) mf'). apply pathsinv0; eapply pathscomp0. eapply maponpaths, (limArrowCommutes _ _ (cc c') mf'). simpl; rewrite assoc, <- functor_comp. set (mf := tpair _ (pr1 mf') (g · pr2 mf') : c ↓ K). apply pathsinv0. exact (limArrowCommutes (LA (c ↓ K) (QT T c)) (S c) (cc c) mf). } assert (is_nat_trans_σ : is_nat_trans S (R_data T) σ). { intros c c' g; simpl. transparent assert (ccc : (cone (QT T c') (S c))). { use make_cone. - intro mf'; apply (σ c · Rmor T c c' g · limOut (LA (c' ↓ K) (QT T c')) mf'). - abstract (intros u v e; simpl; rewrite <- !assoc; apply maponpaths, maponpaths, (limOutCommutes (LA (c' ↓ K) (QT T c')) u v e)). } rewrite (limArrowUnique (LA (c' ↓ K) (QT T c')) _ ccc (# S g · σ c') (H _ _ _)). now apply pathsinv0, limArrowUnique. } use tpair. + apply (tpair _ (tpair _ σ is_nat_trans_σ)). apply nat_trans_eq; [apply homset_property | intro n; cbn]. generalize (limArrowCommutes (LA (K n ↓ K) (QT T (K n))) _ (cc _) (Kid n)); simpl. now rewrite functor_id, id_left. + intro x. apply subtypePath; [intros xx; apply (isaset_nat_trans (homset_property A))|]. apply subtypePath; [intros xx; apply (isaprop_is_nat_trans _ _ (homset_property A))|]; simpl. apply funextsec; intro c. apply limArrowUnique; intro u; simpl. destruct x as [t p]; simpl. assert (temp : α (pr1 u) = nat_trans_comp _ _ T (pre_whisker K t) (eps T) (pr1 u)). now rewrite p. rewrite temp; simpl. destruct u as [n g]; simpl in *. apply pathsinv0; eapply pathscomp0; [rewrite assoc; apply cancel_postcomposition, (nat_trans_ax t _ _ g)|]. rewrite <- !assoc; apply maponpaths. generalize (limArrowCommutes (LA (K n ↓ K) _) _ (Rmor_cone T c (K n) g) (Kid n)). now simpl; rewrite id_right. Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.CommaCategories