proposition: 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: 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.
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.FunctorCategory UniMath.CategoryTheory.Adjunctions.Core