proposition: Lemma wfs_closed_coproducts {C : category} {I : hSet} (w : wfs C) {a b : I -> C} {f : ∏ (i : I), a i --> b i} (hf : ∀ (i : I), (wfs_L w _ _) (f i)) (CCa : Coproduct _ _ a) (CCb : Coproduct _ _ b) (aoc : AxiomOfChoice) : (wfs_L w _ _) (CoproductOfArrows _ _ CCa CCb f).
proof: Proof. unfold wfs_L in *. rewrite (wfs_llp w) in *. intros x y g hg. intros h k s. set (hi := λ i, (CoproductIn _ _ CCa i) · h). set (ki := λ i, (CoproductIn _ _ CCb i) · k). assert (∏ i, ∃ li, ((f i) · li = hi i) × (li · g = ki i)) as ilift. { intro i. specialize (hf i _ _ g hg) as H. specialize (H (hi i) (ki i)). use H. unfold hi, ki. rewrite <- assoc, s, assoc, assoc. now rewrite (CoproductOfArrowsIn _ _). } assert (∥∏ i, ∑ li, ((f i) · li = hi i) × (li · g = ki i)∥) as ilift_aoc. { set (aocI := aoc I). simpl in aocI. apply (aocI). exact ilift. } assert (∃ (li : (∏ i, (b i --> x))), (∏ i, (f i) · (li i) = hi i × ((li i) · g = ki i))) as ilifts. { use (hinhuniv _ ilift_aoc). intro ilift_aoc_sig. apply hinhpr. use tpair. - intro i. set (li := ilift_aoc_sig i). destruct li as [l hl]. exact l. - intro i. set (li := ilift_aoc_sig i). simpl. destruct li as [l hl]. exact hl. } use (hinhuniv _ ilifts). intro ilift_sig. destruct ilift_sig as [li hli]. set (hl := isCoproduct_Coproduct _ _ CCb x li). destruct hl as [[l hl] uniqueness]. apply hinhpr. exists l. split; rewrite CoproductArrowEta, (CoproductArrowEta _ _ _ _ _ l). - rewrite (precompWithCoproductArrow). apply CoproductArrowUnique. intro i. rewrite CoproductInCommutes. destruct (hli i) as [hlicomm _]. change (CoproductIn _ _ _ _ · h) with (hi i). rewrite (hl i). exact hlicomm. - apply CoproductArrowUnique. intro i. rewrite assoc. rewrite CoproductInCommutes. destruct (hli i) as [_ klicomm]. change (CoproductIn _ _ _ _ · k) with (ki i). rewrite (hl i). exact klicomm. 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