proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Slice UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Adjunctions.Examples UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.RightKanExtension UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Chains.Chains