English
If the two pushout squares s and t are arranged vertically, their vertical composition is a pushout.
Русский
Если два пушаута соединены вертикально, их вертикальная компоновка остаётся пушаутом.
LaTeX
$$$\text{IsPushout}(h_{11}, v_{11}\circ v_{21}, v_{12}\circ v_{22}, h_{31})$$$
Lean4
/-- Paste two pushout squares "horizontally" to obtain another pushout square.
The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
```
-/
theorem paste_horiz {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂}
{h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
(t : IsPushout h₁₂ v₁₂ v₁₃ h₂₂) : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) :=
(paste_vert s.flip t.flip).flip
