proposition: Lemma pullback_to_slice_pullback (A B C : ob (E / I)) (k : A --> C) (l : B --> C) (PB : Pullback ($$ k) ($$ l)) : Pullback k l.
proof: Proof. assert (eq : PullbackPr1 PB · $ A = PullbackPr2 PB · $ B). { assert (eq1 : $ A = $$ k · $ C) by (apply slicecat_mor_comm). assert (eq2 : $ B = $$ l · $ C) by (apply slicecat_mor_comm). rewrite eq2, eq1. do 2 rewrite assoc. apply (maponpaths (fun x => x · _)). apply PullbackSqrCommutes. } pose (PBtoI := PullbackPr1 PB · $ A). use make_Pullback. - use tpair. + exact (PullbackObject PB). + exact PBtoI. - use tpair. + exact (PullbackPr1 PB). + reflexivity. - use tpair. + exact (PullbackPr2 PB). + exact eq. - apply eq_mor_slicecat, PullbackSqrCommutes. - intros PB' prA' prB' commSq'. use iscontrweqb; [exact (∑ kk : % PB' --> PullbackObject PB, kk · PullbackPr1 PB = ($$ prA') × kk · PullbackPr2 PB = ($$ prB') × slicecat_ob_morphism _ _ PB' = kk · PBtoI)| | ]. use weqcomp. + exact (∑ kk : PB' --> (PullbackObject PB,, PBtoI), ($$ kk) · PullbackPr1 PB = ($$ prA') × ($$ kk) · PullbackPr2 PB = ($$ prB')). + apply weqfibtototal; intro. apply weqdirprodf; (apply weqiff; [|apply has_homsets_slice_precat|apply homset_property]; apply weq_to_iff). * eapply weqcomp; [apply invweq, eq_mor_slicecat_weq|]. apply idweq. * eapply weqcomp; [apply invweq, eq_mor_slicecat_weq|]. apply idweq. + cbn. eapply weqcomp. * apply (@weqtotal2asstor (E⟦% PB', PB⟧) (fun f => $ PB' = f · PBtoI) _). * apply weqfibtototal; intro; cbn. eapply weqcomp. apply weqdirprodcomm. apply weqdirprodasstor. + apply (iscontr_cond_dirprod_weq (isPullback_Pullback PB _ _ _ (maponpaths pr1 commSq'))). * intro; apply homset_property. * intro; apply homset_property. * intro; apply homset_property. * unfold PBtoI. change (pr1 (iscontrpr1 (isPullback_Pullback PB (pr1 PB') (pr1 prA') (pr1 prB') (maponpaths pr1 commSq')))) with (PullbackArrow PB _ _ _ (maponpaths pr1 commSq')). cbn. rewrite assoc. rewrite PullbackArrow_PullbackPr1. apply slicecat_mor_comm. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis