lift — Mathlib

Lean4
/-- A prefunctor from a quiver `B` to a bicategory `C` can be lifted to a pseudofunctor from
`free_bicategory B` to `C`.
-/
@[simps]
def lift : Pseudofunctor (FreeBicategory B) C where
  obj := F.obj
  map := liftHom F
  mapId _ := Iso.refl _
  mapComp _ _ := Iso.refl _
  map₂ := Quot.lift (liftHom₂ F) fun _ _ H => liftHom₂_congr F H
  map₂_comp := by
    intro a b f g h η θ
    induction η using Quot.rec
    · induction θ using Quot.rec <;> rfl
    · rfl
  map₂_whisker_left := by
    intro a b c f g h η
    induction η using Quot.rec
    · cat_disch
    · rfl
  map₂_whisker_right := by intro _ _ _ _ _ η h; dsimp; induction η using Quot.rec <;> cat_disch
Похожие утверждения