Lean4
/-- Given two refinement morphisms `f, g : E ⟶ F`, this is a (pre-)`1`-hypercover `W` that
admits a morphism `h : W ⟶ E` such that `h ≫ f` and `h ≫ g` are homotopic. Hence
they become equal after quotienting out by homotopy.
This is a `1`-hypercover, if `E` and `F` are (see `OneHypercover.cylinder`). -/
@[simps]
noncomputable def cylinder (f g : E.Hom F) : PreOneHypercover.{max w w'} S
where
I₀ := Σ (i : E.I₀), F.I₁ (f.s₀ i) (g.s₀ i)
X p := cylinderX f g p.2
f p := cylinderf f g p.2
I₁ p q := ULift.{max w w'} (E.I₁ p.1 q.1)
Y {p q}
k :=
pullback
(pullback.map (cylinderf f g p.2) (cylinderf f g q.2) _ _ (pullback.fst _ _) (pullback.fst _ _) (𝟙 S) (by simp)
(by simp))
(pullback.lift _ _ (E.w k.down))
p₁ {p q} k := pullback.fst _ _ ≫ pullback.fst _ _
p₂ {p q} k := pullback.fst _ _ ≫ pullback.snd _ _
w {_ _} k := by simp [pullback.condition]
