Lean4
/-- Construct a `Mor₂Iso` term from a Lean expression. -/
partial def Mor₂IsoOfExpr (e : Expr) : BicategoryM Mor₂Iso := do
match (← whnfR e).getAppFnArgs with
| (``Bicategory.associator, #[_, _, _, _, _, _, f, g, h]) =>
associatorM' (← MkMor₁.ofExpr f) (← MkMor₁.ofExpr g) (← MkMor₁.ofExpr h)
| (``Bicategory.leftUnitor, #[_, _, _, _, f]) =>
leftUnitorM' (← MkMor₁.ofExpr f)
| (``Bicategory.rightUnitor, #[_, _, _, _, f]) =>
rightUnitorM' (← MkMor₁.ofExpr f)
| (``Iso.refl, #[_, _, f]) =>
id₂M' (← MkMor₁.ofExpr f)
| (``Iso.symm, #[_, _, _, _, η]) =>
symmM (← Mor₂IsoOfExpr η)
| (``Iso.trans, #[_, _, _, _, _, η, θ]) =>
comp₂M (← Mor₂IsoOfExpr η) (← Mor₂IsoOfExpr θ)
| (``Bicategory.whiskerLeftIso, #[_, _, _, _, _, f, _, _, η]) =>
whiskerLeftM (← MkMor₁.ofExpr f) (← Mor₂IsoOfExpr η)
| (``Bicategory.whiskerRightIso, #[_, _, _, _, _, _, _, η, h]) =>
whiskerRightM (← Mor₂IsoOfExpr η) (← MkMor₁.ofExpr h)
| (``bicategoricalIsoComp, #[_, _, _, _, _, g, h, _, inst, η, θ]) =>
let α ← coherenceHomM (← MkMor₁.ofExpr g) (← MkMor₁.ofExpr h) inst
coherenceCompM α (← Mor₂IsoOfExpr η) (← Mor₂IsoOfExpr θ)
| (``BicategoricalCoherence.iso, #[_, _, _, _, f, g, inst]) =>
coherenceHomM' (← MkMor₁.ofExpr f) (← MkMor₁.ofExpr g) inst
| _ =>
return .of ⟨e, ← MkMor₁.ofExpr (← srcExprOfIso e), ← MkMor₁.ofExpr (← tgtExprOfIso e)⟩
