Lemma right_adjoint_preserves_limit (HF : is_right_adjoint F) {g : graph} (d : diagram g C) (L : C) (ccL : cone d L) : preserves_limit d L ccL. Proof. intros HccL M ccM. set (G := left_adjoint HF). set (H := pr2 HF : are_adjoints G F). apply (@iscontrweqb _ (∑ y : C ⟦ G M, L ⟧, ∏ i, y · coneOut ccL i = φ_adj_inv H (coneOut ccM i))). - eapply (weqcomp (Y := ∑ y : C ⟦ G M, L ⟧, ∏ i, φ_adj H y · # F (coneOut ccL i) = coneOut ccM i)). + apply invweq, (weqbandf (adjunction_hom_weq H M L)); simpl; intro f. abstract (now apply weqiff; try (apply impred; intro; apply D)). + eapply (weqcomp (Y := ∑ y : C ⟦ G M, L ⟧, ∏ i, φ_adj H (y · coneOut ccL i) = coneOut ccM i)). * apply weqfibtototal; simpl; intro f. abstract (apply weqiff; try (apply impred; intro; apply D); split; intros HH i; [ now rewrite φ_adj_natural_postcomp; apply HH | now rewrite <- φ_adj_natural_postcomp; apply HH ]). * apply weqfibtototal; simpl; intro f. abstract (apply weqiff; [ | apply impred; intro; apply D | apply impred; intro; apply C ]; split; intros HH i; [ now rewrite <- (HH i), φ_adj_inv_after_φ_adj | now rewrite (HH i), φ_adj_after_φ_adj_inv ]). - transparent assert (X : (cone d (G M))). { use make_cone. + intro v; apply (φ_adj_inv H (coneOut ccM v)). + intros m n e; simpl. rewrite <- (coneOutCommutes ccM m n e); simpl. now rewrite φ_adj_inv_natural_postcomp. } apply (HccL (G M) X). 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.