Lemma preserves_colimit_slicecat_to_cat_HSET_direct (X : HSET) (g : graph) (d : diagram g (HSET / X)) (L : HSET / X) (ccL : cocone d L) : preserves_colimit (slicecat_to_cat HSET X) d L ccL. Proof. intros HccL y ccy. set (CC := make_ColimCocone _ _ _ HccL). transparent assert (c : (HSET / X)). { use tpair. - exists (∑ (x : pr1 X), pr1 y). abstract (apply isaset_total2; intros; apply setproperty). - cbn. apply pr1. } transparent assert (cc : (cocone d c)). { use make_cocone. - intros n. use tpair; simpl. + intros z. use tpair. * exact (pr2 L (pr1 (coconeIn ccL n) z)). * apply (coconeIn ccy n z). + abstract (now apply funextsec; intro z; apply (toforallpaths _ _ _ (pr2 (coconeIn ccL n)) z)). - abstract (intros m n e; apply eq_mor_slicecat, funextsec; intro z; use total2_paths_f; [ apply (maponpaths _ (toforallpaths _ _ _ (maponpaths pr1 (coconeInCommutes ccL m n e)) z))|]; cbn in *; induction (maponpaths pr1 _); simpl; now rewrite idpath_transportf, <- (coconeInCommutes ccy m n e)). } use unique_exists. - intros l; apply (pr2 (pr1 (colimArrow CC c cc) l)). - simpl; intro n. apply funextsec; intro x; cbn. now etrans; [apply maponpaths, (toforallpaths _ _ _ (maponpaths pr1 (colimArrowCommutes CC c cc n)) x)|]. - intro ; apply impred_isaprop. intro ; apply homset_property. - simpl; intros f Hf. apply funextsec; intro l. transparent assert (k : (HSET/X⟦colim CC,c⟧)). { use tpair. - intros l'. exists (pr2 L l'). apply (f l'). - abstract (now apply funextsec). } assert (Hk : (∏ n, colimIn CC n · k = coconeIn cc n)). { intros n. apply subtypePath; [intros x; apply homset_property|]. apply funextsec; intro z. use total2_paths_f; [apply idpath|]. now rewrite idpath_transportf; cbn; rewrite <- (toforallpaths _ _ _ (Hf n) z). } apply (maponpaths dirprod_pr2 (toforallpaths _ _ _ (maponpaths pr1 (colimArrowUnique CC c cc k Hk)) l)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Slice. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Adjunctions.Examples. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Chains.Chains.