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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis.