proposition: Lemma omega_cocontConstProdFunctor : is_omega_cocont constprod_functor.
proof: Proof. intros hF c L ccL HcL cc. use tpair. - transparent assert (HX : (cocone hF (funset x HcL))). { use make_cocone. * simpl; intro n; apply flip, (curry (Z := λ _,_)), (pr1 cc). * abstract (destruct cc as [f hf]; simpl; intros m n e; rewrite <- (hf m n e); destruct e; simpl; repeat (apply funextfun; intro); apply idpath). } use tpair. + simpl; apply uncurry, flip. apply (colimArrow (make_ColimCocone _ _ _ ccL) (funset x HcL)). apply HX. + cbn. destruct cc as [f hf]; simpl; intro n. apply funextfun; intro p. change p with (pr1 p,,pr2 p). assert (XR := colimArrowCommutes (make_ColimCocone hF c L ccL) _ HX n). unfold flip, curry, colimIn in *; simpl in *. now rewrite <- (toforallpaths _ _ _ (toforallpaths _ _ _ XR (pr2 p)) (pr1 p)). - abstract ( intro p; unfold uncurry; simpl; apply subtypePath; simpl; [ intro g; apply impred; intro t; use (let ff : HSET ⟦(x × dob hF t)%set,HcL⟧ := _ in _); [ simpl; apply (pr1 cc) | apply (@has_homsets_HSET _ HcL _ ff) ] | destruct p as [t p]; simpl; apply funextfun; intro xc; destruct xc as [x' c']; simpl; use (let g : HSET⟦colim (make_ColimCocone hF c L ccL), funset x HcL⟧ := _ in _); [ simpl; apply flip, (curry (Z := λ _,_)), t | rewrite <- (colimArrowUnique _ _ _ g); [apply idpath | ]; destruct cc as [f hf]; unfold is_cocone_mor in p; simpl in *; now intro n; simpl; rewrite <- (p n) ] ]). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Lists UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Chains.All UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.PrecategoryBinProduct