Definition isPullback_iso_comma_mor : w --> pb. Proof. simple refine ((_ ,, _) ,, _). - refine (PullbackArrow P₁ _ (pr11 h₁) (pr11 h₂) _). abstract (exact (maponpaths (λ z, pr11 z) p)). - refine (PullbackArrow P₂ _ (pr21 h₁) (pr21 h₂) _). abstract (exact (maponpaths (λ z, dirprod_pr2 (pr1 z)) p)). - use (MorphismsIntoPullbackEqual (HG _ _ _ _ _ _ _ _ _ _ (pr22 P₂))). + abstract (rewrite <- !functor_comp ; apply maponpaths ; exact (PullbackSqrCommutes P₂)). + abstract (cbn ; rewrite !assoc' ; rewrite <- !functor_comp ; rewrite (PullbackArrow_PullbackPr1 P₂) ; refine (_ @ pr2 h₁) ; rewrite <- (pr2 π₁) ; rewrite !assoc ; apply maponpaths_2 ; rewrite <- !functor_comp ; apply maponpaths ; apply (PullbackArrow_PullbackPr1 P₁)). + abstract (cbn ; rewrite !assoc' ; rewrite <- !functor_comp ; rewrite (PullbackArrow_PullbackPr2 P₂) ; refine (_ @ pr2 h₂) ; rewrite <- (pr2 π₂) ; rewrite !assoc ; apply maponpaths_2 ; rewrite <- !functor_comp ; apply maponpaths ; apply (PullbackArrow_PullbackPr2 P₁)). 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.