proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.Graphs.Colimits