Definition pullbacks_in_iso_comma (HC₁ : Pullbacks C₁) (HC₂ : Pullbacks C₂) : Pullbacks (iso_comma F G). Proof. intros z x y f g. simple refine ((_ ,, _ ,, _) ,, (_ ,, _)). - simple refine ((_ ,, _) ,, _). + exact (PullbackObject (HC₁ _ _ _ (pr11 f) (pr11 g))). + exact (PullbackObject (HC₂ _ _ _ (pr21 f) (pr21 g))). + use (iso_between_pullbacks _ _ (HF _ _ _ _ _ _ _ _ _ _ (isPullback_Pullback (HC₁ _ _ _ (pr11 f) (pr11 g)))) (HG _ _ _ _ _ _ _ _ _ _ (isPullback_Pullback (HC₂ _ _ _ (pr21 f) (pr21 g))))). * abstract (rewrite <- !functor_comp ; apply maponpaths ; apply PullbackSqrCommutes). * abstract (rewrite <- !functor_comp ; apply maponpaths ; apply PullbackSqrCommutes). * exact (pr2 x). * exact (pr2 y). * exact (pr2 z). * exact (!(pr2 f)). * exact (!(pr2 g)). - simple refine ((_ ,, _) ,, _). + apply PullbackPr1. + apply PullbackPr1. + abstract (cbn ; unfold iso_between_pullbacks_map ; refine (!_) ; apply (PullbackArrow_PullbackPr1 (make_Pullback _ (HG _ _ _ _ _ _ _ _ _ _ (isPullback_Pullback (HC₂ _ _ _ (pr21 f) (pr21 g))))))). - simple refine ((_ ,, _) ,, _). + apply PullbackPr2. + apply PullbackPr2. + abstract (cbn ; unfold iso_between_pullbacks_map ; refine (!_) ; apply (PullbackArrow_PullbackPr2 (make_Pullback _ (HG _ _ _ _ _ _ _ _ _ _ (isPullback_Pullback (HC₂ _ _ _ (pr21 f) (pr21 g))))))). - abstract (use eq_iso_comma_mor ; cbn ; [ apply PullbackSqrCommutes | apply PullbackSqrCommutes ]). - use isPullback_iso_comma. + apply PullbackSqrCommutes. + apply isPullback_Pullback. + apply PullbackSqrCommutes. + apply isPullback_Pullback. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.IsoCommaCategory. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation.