liftHom₂ — Mathlib

Lean4
/-- Auxiliary definition for `lift`. -/
def liftHom₂ : ∀ {a b : FreeBicategory B} {f g : a ⟶ b}, Hom₂ f g → (liftHom F f ⟶ liftHom F g)
  | _, _, _, _, Hom₂.id _ => 𝟙 _
  | _, _, _, _, Hom₂.associator _ _ _ => (α_ _ _ _).hom
  | _, _, _, _, Hom₂.associator_inv _ _ _ => (α_ _ _ _).inv
  | _, _, _, _, Hom₂.left_unitor _ => (λ_ _).hom
  | _, _, _, _, Hom₂.left_unitor_inv _ => (λ_ _).inv
  | _, _, _, _, Hom₂.right_unitor _ => (ρ_ _).hom
  | _, _, _, _, Hom₂.right_unitor_inv _ => (ρ_ _).inv
  | _, _, _, _, Hom₂.vcomp η θ => liftHom₂ η ≫ liftHom₂ θ
  | _, _, _, _, Hom₂.whisker_left f η => liftHom F f ◁ liftHom₂ η
  | _, _, _, _, Hom₂.whisker_right h η => liftHom₂ η ▷ liftHom F h
Похожие утверждения