functorEquiv — Mathlib

Lean4
/-- The universal property of categorical pullbacks, stated as an equivalence
of categories between functors `X ⥤ (F ⊡ G)` and categorical commutative squares
over X. -/
@[simps]
def functorEquiv : (X ⥤ F ⊡ G) ≌ CatCommSqOver F G X
    where
  functor := toCatCommSqOver F G X
  inverse := CatCommSqOver.toFunctorToCategoricalPullback F G X
  unitIso := NatIso.ofComponents (fun _ ↦ NatIso.ofComponents (fun _ ↦ CategoricalPullback.mkIso (.refl _) (.refl _)))
  counitIso :=
    NatIso.ofComponents
      (fun _ ↦
        CategoricalPullback.mkIso (NatIso.ofComponents (fun _ ↦ .refl _)) (NatIso.ofComponents (fun _ ↦ .refl _)))
Похожие утверждения