mk' — Mathlib

Lean4
/-- An alternate constructor for strictly unitary lax functors that does not
require the `mapId` fields, and that adapts the `map₂_leftUnitor` and
`map₂_rightUnitor` to the fact that the functor is strictly unitary. -/
@[simps]
def mk' (S : StrictlyUnitaryPseudofunctorCore B C) : StrictlyUnitaryPseudofunctor B C
    where
  obj := S.obj
  map := S.map
  map_id := S.map_id
  mapId x := eqToIso (S.map_id x)
  mapId_eq_eqToIso x := rfl
  map₂ := S.map₂
  map₂_id := S.map₂_id
  map₂_comp := S.map₂_comp
  mapComp := S.mapComp
  map₂_left_unitor f := by simpa using S.map₂_left_unitor f
  map₂_right_unitor f := by simpa using S.map₂_right_unitor f
  map₂_associator f g h := by simpa using S.map₂_associator f g h
  map₂_whisker_left f _ _ η := by simpa using S.map₂_whisker_left f η
  map₂_whisker_right η f := by simpa using S.map₂_whisker_right η f
Похожие утверждения