Lean4
/-- Composition of oplax functors. -/
--@[simps]
def comp (F : OplaxFunctor B C) (G : OplaxFunctor C D) : OplaxFunctor B D
where
toPrelaxFunctor := F.toPrelaxFunctor.comp G.toPrelaxFunctor
mapId := fun a => (G.mapFunctor _ _).map (F.mapId a) ≫ G.mapId (F.obj a)
mapComp := fun f g => (G.mapFunctor _ _).map (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)
mapComp_naturality_left := fun η g => by
dsimp
rw [← G.map₂_comp_assoc, mapComp_naturality_left, G.map₂_comp_assoc, mapComp_naturality_left, assoc]
mapComp_naturality_right := fun η => by
dsimp
intros
rw [← G.map₂_comp_assoc, mapComp_naturality_right, G.map₂_comp_assoc, mapComp_naturality_right, assoc]
map₂_associator := fun f g h => by
dsimp
simp only [map₂_associator, ← PrelaxFunctor.map₂_comp_assoc, ← mapComp_naturality_right_assoc, whiskerLeft_comp,
assoc]
simp only [map₂_associator, PrelaxFunctor.map₂_comp, mapComp_naturality_left_assoc, comp_whiskerRight, assoc]
map₂_leftUnitor := fun f => by
dsimp
simp only [map₂_leftUnitor, PrelaxFunctor.map₂_comp, mapComp_naturality_left_assoc, comp_whiskerRight, assoc]
map₂_rightUnitor := fun f => by
dsimp
simp only [map₂_rightUnitor, PrelaxFunctor.map₂_comp, mapComp_naturality_right_assoc, whiskerLeft_comp, assoc]
