Lemma omega_cocontConstProdFunctor : is_omega_cocont constprod_functor. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.