Lemma left_adjoint_preserves_colimit {C D : category} (F : functor C D) (HF : is_left_adjoint F) {g : graph} (d : diagram g C) (L : C) (ccL : cocone d L) : preserves_colimit F d L ccL. Proof. intros HccL M ccM. set (G := right_adjoint HF). set (H := pr2 HF : are_adjoints F G). apply (@iscontrweqb _ (∑ y : C ⟦ L, G M ⟧, ∏ i, coconeIn ccL i · y = φ_adj H (coconeIn ccM i))). - eapply (weqcomp (Y := ∑ y : C ⟦ L, G M ⟧, ∏ i, # F (coconeIn ccL i) · φ_adj_inv H y = coconeIn ccM i)). + apply (weqbandf (adjunction_hom_weq H L M)); simpl; intro f. abstract (apply weqiff; try (apply impred; intro; apply D); now rewrite φ_adj_inv_after_φ_adj). + eapply (weqcomp (Y := ∑ y : C ⟦ L, G M ⟧, ∏ i, φ_adj_inv H (coconeIn ccL i · y) = coconeIn ccM i)). * apply weqfibtototal; simpl; intro f. abstract (apply weqiff; try (apply impred; intro; apply D); split; [ intros HH i; rewrite φ_adj_inv_natural_precomp; apply HH | intros HH i; rewrite <- φ_adj_inv_natural_precomp; 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_after_φ_adj_inv | now rewrite (HH i), φ_adj_inv_after_φ_adj ]). - transparent assert (X : (cocone d (G M))). { use make_cocone. + intro v; apply (φ_adj H (coconeIn ccM v)). + abstract (intros m n e; simpl; rewrite <- (coconeInCommutes ccM m n e); simpl; now rewrite φ_adj_natural_precomp). } 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.FunctorCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core.