J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : IsVanKampen H
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ Y
αY : Y' ⟶ X
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX g
hg : IsPullback g' αW αY f
hh : CommSq h' αX αZ i
hi : CommSq i' αY αZ h
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ i ∧ IsPullback i' αY αZ h
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : IsVanKampen H
⊢ IsVanKampen (_ : IsPushout g f i h)
introv W' hf hg hh hi w
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : IsVanKampen H
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ Y
αY : Y' ⟶ X
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX g
hg : IsPullback g' αW αY f
hh : CommSq h' αX αZ i
hi : CommSq i' αY αZ h
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ i ∧ IsPullback i' αY αZ h
simpa only [IsPushout.flip_iff, IsPullback.flip_iff, and_comm] using
  H' g' f' i' h' αW αY αX αZ hg hf hi hh w.flip