widePullbackShapeEquiv — Mathlib

Lean4
/-- In the case of a discrete category, `WithTerminal` is the same category as `WidePullbackShape`

TODO: Should we simply replace `WidePullbackShape J` with `WithTerminal (Discrete J)` everywhere? -/
@[simps! functor_obj inverse_obj]
def widePullbackShapeEquiv {J : Type*} : WidePullbackShape J ≌ WithTerminal (Discrete J)
    where
  functor.obj := widePullbackShapeEquivObj
  functor.map := widePullbackShapeEquivMap _ _
  inverse.obj := widePullbackShapeEquivObj.symm
  inverse.map f := (widePullbackShapeEquivMap _ _).symm (eqToHom (by simp) ≫ f ≫ eqToHom (by simp))
  unitIso := NatIso.ofComponents fun x ↦ eqToIso (by aesop)
  counitIso := NatIso.ofComponents fun x ↦ eqToIso (by aesop)
Похожие утверждения