Lean4
/-- Given a term of type `∀ ..., η = θ`, where `η θ : f ⟶ g` are 2-morphisms in some bicategory
`B`, which is bound by the `∀` binder, get the corresponding equation in the bicategory `Cat`.
It is important here that the levels in the term are level metavariables, as otherwise these will
not be reassignable to the corresponding levels of `Cat`. -/
def toCatExpr (e : Expr) : MetaM Expr := do
let (args, binderInfos, conclusion) ←
forallMetaTelescope
(← inferType e)
-- Find the expression corresponding to the bicategory, by analyzing `η = θ` (i.e. conclusion)
let B ←
match conclusion.getAppFnArgs with
| (`Eq, #[_, η, _]) =>
match (← inferType η).getAppFnArgs with
| (`Quiver.Hom, #[_, _, f, _]) =>
match (← inferType f).getAppFnArgs with
| (`Quiver.Hom, #[_, _, a, _]) =>
inferType a
| _ =>
throwError "The conclusion {conclusion} is not an equality of 2-morphisms!"
| _ =>
throwError "The conclusion {conclusion} is not an equality of 2-morphisms!"
| _ =>
throwError "The conclusion {conclusion} is not an equality!"
let u ← mkFreshLevelMVar
let v ← mkFreshLevelMVar
let _ ←
isDefEq B
(.const ``Cat [v, u])
-- Assign the right bicategory instance to `Cat.{v, u}`
let some inst ←
args.findM? fun x => do
return (← inferType x).getAppFnArgs == (`CategoryTheory.Bicategory, #[B]) |
throwError"Cannot find the argument for the bicategory instance of the bicategory in which \
the equality is taking place."
let _ ←
isDefEq inst
(.const ``CategoryTheory.Cat.bicategory [v, u])
-- Construct the new expression
let value := mkAppN e args
let rec /-- Recursive function which applies `mkLambdaFVars` stepwise
(so that each step can have different binderinfos) -/
apprec (i : Nat) (e : Expr) : MetaM Expr := do
if h : i < args.size then
let arg := args[i]
let bi := binderInfos[i]!
let e' ← apprec (i + 1) e
unless arg != B && arg != inst do
return e'
mkLambdaFVars #[arg] e' (binderInfoForMVars := bi)
else
return e
let value ← apprec 0 value
return value
