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 : StrictlyUnitaryLaxFunctorCore B C) : StrictlyUnitaryLaxFunctor B C
    where
  obj := S.obj
  map := S.map
  map_id := S.map_id
  mapId x := eqToHom (S.map_id x).symm
  mapId_eq_eqToHom x := rfl
  map₂ := S.map₂
  map₂_id := S.map₂_id
  map₂_comp := S.map₂_comp
  mapComp := S.mapComp
  mapComp_naturality_left := S.mapComp_naturality_left
  mapComp_naturality_right := S.mapComp_naturality_right
  map₂_leftUnitor f := by simpa using S.map₂_leftUnitor f
  map₂_rightUnitor f := by simpa using S.map₂_rightUnitor f
  map₂_associator f g h := by simpa using S.map₂_associator f g h
Похожие утверждения