English
If the squares with φ: a → b and φ': a → b' are strongly cocartesian, and the outer square with f, g satisfies f' = f ≫ g and f'' = f' ≫ g', then ψ is strongly cocartesian as well. This establishes closure under composition in the base morphisms.
Русский
Если квадраты, где φ: a → b и φ': a → b' являются сильно когартезианальными, и внешний квадрат удовлетворяет f' = f ≫ g и f'' = f' ≫ g', то ψ тоже является сильно когартезианальной. Это даёт closure по композиции базовых морфизмов.
LaTeX
$$$[IsStronglyCocartesian p f φ] [IsStronglyCocartesian p g ψ] → IsStronglyCocartesian p (f ≫ g) (φ ≫ ψ)$$$
Lean4
/-- Given two strongly co-Cartesian morphisms `φ`, `ψ` as follows
```
a --φ--> b --ψ--> c
| | |
v v v
R --f--> S --g--> T
```
Then the composite `φ ≫ ψ` is also strongly co-Cartesian. -/
instance comp [IsStronglyCocartesian p f φ] [IsStronglyCocartesian p g ψ] : IsStronglyCocartesian p (f ≫ g) (φ ≫ ψ)
where
universal_property' := by
intro c' h τ hτ
use map p g ψ (f' := g ≫ h) rfl <| map p f φ (assoc f g h) τ
refine ⟨⟨inferInstance, ?_⟩, ?_⟩
· simp only [assoc, fac]
· intro π' ⟨hπ'₁, hπ'₂⟩
apply map_uniq
apply map_uniq
simp only [← hπ'₂, assoc]
