mkOfOplax — Mathlib

Lean4
/-- Construct a pseudofunctor from an oplax functor whose `mapId` and `mapComp` are isomorphisms. -/
@[simps]
def mkOfOplax (F : OplaxFunctor B C) (F' : F.PseudoCore) : Pseudofunctor B C
    where
  toPrelaxFunctor := F.toPrelaxFunctor
  mapId := F'.mapIdIso
  mapComp := F'.mapCompIso
  map₂_whisker_left := fun f g h η => by
    rw [F'.mapCompIso_hom f g, ← F.mapComp_naturality_right_assoc, ← F'.mapCompIso_hom f h, hom_inv_id, comp_id]
  map₂_whisker_right := fun η h => by
    rw [F'.mapCompIso_hom _ h, ← F.mapComp_naturality_left_assoc, ← F'.mapCompIso_hom _ h, hom_inv_id, comp_id]
  map₂_associator := fun f g h => by
    rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ← F'.mapCompIso_hom f (g ≫ h), ←
      F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc, hom_inv_id, comp_id]
Похожие утверждения