Lean4
/-- Pullback cones to `X` are the same thing as binary fans in `Over X`. -/
@[simps]
def pullbackConeEquivBinaryFan : PullbackCone f g ≌ BinaryFan (Over.mk f) (.mk g)
where
functor.obj
c :=
.mk (Over.homMk (U := .mk (c.fst ≫ f)) (V := .mk f) c.fst rfl)
(Over.homMk (U := .mk (c.fst ≫ f)) (V := .mk g) c.snd c.condition.symm)
functor.map {c₁ c₂} a := { hom := Over.homMk a.hom, w := by rintro (_ | _) <;> cat_disch }
inverse.obj c := PullbackCone.mk c.fst.left c.snd.left (c.fst.w.trans c.snd.w.symm)
inverse.map {c₁ c₂}
a :=
{ hom := a.hom.left
w := by rintro (_ | _ | _) <;> simp [← Over.comp_left_assoc, ← Over.comp_left] }
unitIso := NatIso.ofComponents (fun c ↦ c.eta) (by intros; ext; simp)
counitIso :=
NatIso.ofComponents
(fun X ↦ BinaryFan.ext (Over.isoMk (Iso.refl _) (by simpa using X.fst.w.symm)) (by ext; simp) (by ext; simp))
(by intros; ext; simp [BinaryFan.ext])
functor_unitIso_comp c := by ext; simp [BinaryFan.ext]
