Lean4
/-- Construct a `Mor₂` term from a Lean expression. -/
partial def Mor₂OfExpr (e : Expr) : BicategoryM Mor₂ := do
match ← whnfR e with
-- whnfR version of `Iso.hom η`
| .proj ``Iso 0 η =>
homM
(← Mor₂IsoOfExpr η)
-- whnfR version of `Iso.inv η`
| .proj ``Iso 1 η =>
invM (← Mor₂IsoOfExpr η)
| .app .. =>
match (← whnfR e).getAppFnArgs with
| (``CategoryStruct.id, #[_, _, f]) =>
id₂M (← MkMor₁.ofExpr f)
| (``CategoryStruct.comp, #[_, _, _, _, _, η, θ]) =>
comp₂M (← Mor₂OfExpr η) (← Mor₂OfExpr θ)
| (``Bicategory.whiskerLeft, #[_, _, _, _, _, f, _, _, η]) =>
whiskerLeftM (← MkMor₁.ofExpr f) (← Mor₂OfExpr η)
| (``Bicategory.whiskerRight, #[_, _, _, _, _, _, _, η, h]) =>
whiskerRightM (← Mor₂OfExpr η) (← MkMor₁.ofExpr h)
| (``bicategoricalComp, #[_, _, _, _, _, g, h, _, inst, η, θ]) =>
let α ← coherenceHomM (← MkMor₁.ofExpr g) (← MkMor₁.ofExpr h) inst
coherenceCompM α (← Mor₂OfExpr η) (← Mor₂OfExpr θ)
| _ =>
return .of ⟨e, ← MkMor₁.ofExpr (← srcExpr e), ← MkMor₁.ofExpr (← tgtExpr e)⟩
| _ =>
return .of ⟨e, ← MkMor₁.ofExpr (← srcExpr e), ← MkMor₁.ofExpr (← tgtExpr e)⟩
