proposition: Lemma wfs_closed_products {C : category} {I : hSet} (w : wfs C) {a b : I -> C} {f : ∏ (i : I), b i --> a i} (hf : ∀ (i : I), (wfs_R w _ _) (f i)) (CCa : Product _ _ a) (CCb : Product _ _ b) (aoc : AxiomOfChoice) : (wfs_R w _ _) (ProductOfArrows _ _ CCa CCb f).
proof: Proof. apply (wfs_closed_coproducts (opp_wfs w)). - exact hf. - exact aoc. Qed.
imports: UniMath.MoreFoundations.All UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Lifting