Lean4
/-- The pseudofunctor from `Cat` to `Cat` defined with `WithInitial`. -/
@[simps]
def pseudofunctor : Pseudofunctor Cat Cat
where
toPrelaxFunctor := prelaxfunctor
mapId C := mapId C
mapComp := mapComp
map₂_whisker_left := by
intros
apply NatTrans.ext
funext X
cases X
· rw [NatTrans.comp_app, NatTrans.comp_app]
simp only [prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj,
prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, map_obj, Cat.comp_obj,
prelaxfunctor_toPrelaxFunctorStruct_map₂, map₂_app, Cat.whiskerLeft_app, mapComp_hom_app, Iso.refl_hom,
mapComp_inv_app, Iso.refl_inv, Category.comp_id, Category.id_comp]
· rfl
map₂_whisker_right := by
intros
apply NatTrans.ext
funext X
cases X
· rw [NatTrans.comp_app, NatTrans.comp_app]
simp only [prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj,
prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, map_obj, Cat.comp_obj,
prelaxfunctor_toPrelaxFunctorStruct_map₂, map₂_app, Cat.whiskerRight_app, mapComp_hom_app, Iso.refl_hom,
map_map, mapComp_inv_app, Iso.refl_inv, Category.comp_id, Category.id_comp]
rfl
· rfl
map₂_associator := by
intros
apply NatTrans.ext
funext X
cases X
· rw [NatTrans.comp_app, NatTrans.comp_app, NatTrans.comp_app, NatTrans.comp_app]
simp only [prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj,
prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, map_obj, Cat.comp_obj,
Bicategory.Strict.associator_eqToIso, eqToIso_refl, Iso.refl_hom, prelaxfunctor_toPrelaxFunctorStruct_map₂,
map₂_app, mapComp_hom_app, Cat.whiskerRight_app, map_map, down_id, Functor.map_id, Cat.whiskerLeft_app,
mapComp_inv_app, Iso.refl_inv, Category.comp_id, Category.id_comp]
rw [NatTrans.id_app, NatTrans.id_app]
simp only [Cat.comp_obj, map_obj, Category.comp_id]
· rfl
map₂_left_unitor := by
intros
apply NatTrans.ext
funext X
cases X
· rw [NatTrans.comp_app, NatTrans.comp_app]
simp only [prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj,
prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, map_obj, Cat.comp_obj,
Bicategory.Strict.leftUnitor_eqToIso, eqToIso_refl, Iso.refl_hom, prelaxfunctor_toPrelaxFunctorStruct_map₂,
map₂_app, mapComp_hom_app, Cat.whiskerRight_app, mapId_hom_app, map_map, Category.id_comp]
rw [NatTrans.id_app, NatTrans.id_app]
simp only [Cat.comp_obj, map_obj, Category.comp_id]
rw [← Functor.map_id]
rfl
· rfl
map₂_right_unitor := by
intros
apply NatTrans.ext
funext X
cases X
· rw [NatTrans.comp_app, NatTrans.comp_app]
simp only [prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj,
prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map, map_obj, Cat.comp_obj,
Bicategory.Strict.rightUnitor_eqToIso, eqToIso_refl, Iso.refl_hom, prelaxfunctor_toPrelaxFunctorStruct_map₂,
map₂_app, mapComp_hom_app, Cat.whiskerLeft_app, mapId_hom_app, Category.id_comp]
rw [NatTrans.id_app, NatTrans.id_app]
simp only [Cat.comp_obj, map_obj, Category.comp_id]
rw [← Functor.map_id, Cat.id_map]
rfl
· rfl
