English
If P and P' are good, then P.trans P' is good.
Русский
Если P и P' хороши, то P.trans P' также хорош.
LaTeX
$$$(P.trans P').IsGood$$$
Lean4
instance [IsFibrant A] (P P' : PathObject A) [P.IsGood] [P'.IsGood] : (P.trans P').IsGood where
fibration_p :=
by
let ψ : (P.trans P').P ⟶ P.P ⨯ A := prod.lift (pullback.fst _ _) (pullback.snd _ _ ≫ P'.p₁)
rw [show (P.trans P').p = ψ ≫ prod.map P.p₀ (𝟙 A) by simp [PrepathObject.p, ψ]]
have fac : ψ ≫ prod.map P.p₁ (𝟙 A) = pullback.snd _ _ ≫ P'.p :=
by
ext
· simp [ψ, pullback.condition]
· simp [ψ]
have sq : IsPullback (ψ ≫ prod.fst) (pullback.snd P.p₁ P'.p₀) P.p₁ (P'.p ≫ prod.fst) := by
simpa [ψ] using IsPullback.of_hasPullback P.p₁ P'.p₀
have : Fibration ψ := by
rw [fibration_iff]
exact
(fibrations C).of_isPullback (IsPullback.of_right sq fac (IsPullback.of_prod_fst_with_id P.p₁ A)).flip
(by rw [← fibration_iff]; infer_instance)
infer_instance
