English
If we have a chain of two strongly cocartesian maps φ: a → b and ψ: b → c, and f', f'' are the corresponding target morphisms with g, g' making the squares commute, then the composition of the induced maps equals the induced map for the composite: map p f φ H φ' ≫ map p f' φ' H' φ'' = map p f φ (f'' = f ≫ (g ≫ g')) φ''.
Русский
Если имеем две последовательные сильно когартезианные стрелы φ: a → b и ψ: b → c и соответствующие f', f'' так, что диаграммы коммутаций выполняются, то композиция индуцированных отображений равна индуцированному отображению для композиции: …
LaTeX
$$$\mathrm{map}\ p\ f\ \phi\ H\ \phi' \;\gg\; \mathrm{map}\ p\ f'\ \phi'\ H'\ \phi'' = \mathrm{map}\ p\ f\ \phi\ (f'' = f \;≫\; (g \;≫\; g'))\ \phi''$$$
Lean4
/-- When its possible to compare the two, the composition of two `IsStronglyCocartesian.map` will
also be given by a `IsStronglyCocartesian.map`. In other words, given diagrams
```
a --φ--> b b' b''
| | | |
v v v v
R --f--> S --g--> S' --g'--> S'
```
and
```
a --φ'--> b'
| |
v v
R --f'--> S'
```
and
```
a --φ''--> b''
| |
v v
R --f''--> S''
```
such that `φ` and `φ'` are strongly co-Cartesian morphisms, and such that `f' = f ≫ g` and
`f'' = f' ≫ g'`. Then composing the induced map from `b ⟶ b'` with the induced map from
`b' ⟶ b''` gives the induced map from `b ⟶ b''`. -/
@[reassoc (attr := simp)]
theorem map_comp_map {S' S'' : 𝒮} {b' b'' : 𝒳} {f' : R ⟶ S'} {f'' : R ⟶ S''} {g : S ⟶ S'} {g' : S' ⟶ S''}
(H : f' = f ≫ g) (H' : f'' = f' ≫ g') (φ' : a ⟶ b') (φ'' : a ⟶ b'') [IsStronglyCocartesian p f' φ']
[IsHomLift p f'' φ''] :
map p f φ H φ' ≫ map p f' φ' H' φ'' = map p f φ (show f'' = f ≫ (g ≫ g') by rwa [← assoc, ← H]) φ'' :=
by
apply map_uniq p f φ
simp only [fac_assoc, fac]
