2.1. Implementation
The implementation has a shared core and two front ends. The shared core carries out the proof of the coherence theorem. The monoidal front end and the bicategorical front end read their respective goals into the syntax expected by that shared core.
2.1.1. Shared Core
A monoidal category enters this implementation through the usual one-object bicategory dictionary:
an object X is treated as a 1-morphism X : \ast \to \ast, a morphism
f : X \to Y is treated as a 2-morphism between those 1-morphisms, and tensor product is treated
as horizontal composition. Mathlib does not define monoidal categories literally as special cases of
bicategories, so the implementation has to carry out the proof in a form that both front ends can
use.
The tactics first convert Lean expressions into internal syntax (there are several such syntactic
categories; for example, Mor₂). This syntax is shared by
the monoidal and bicategorical cases. In practice, one gives abstractly a monad expressing the
requirement that Lean expressions can be converted into internal syntax (in the case of
Mor₂, the corresponding one is
MkMor₂). The concrete conversion method is given later,
in the sections on the front ends.
Then, in the shared part, one runs on this syntax the proof-generating algorithm for the coherence
theorem.
All of this runs in
CoherenceM,
which extends MetaM with the context and caches needed by this proof.
/-- `Context ρ` provides the context for manipulating 2-morphisms in a monoidal category or
bicategory. In particular, we will store `MonoidalCategory` or `Bicategory` instance in a context,
and use this through a reader monad when we construct the lean expressions for 2-morphisms. -/
class Context (ρ : Type) where
/-- Construct a context from a lean expression for a 2-morphism. -/
mkContext? : Expr → MetaM (Option ρ)/-- The state for the `CoherenceM ρ` monad. -/
structure State where
/-- The cache for evaluating lean expressions of 1-morphisms into `Mor₁` terms. -/
cache : PersistentExprMap Mor₁ := {}/-- The monad for manipulating 2-morphisms in a monoidal category or bicategory. -/
abbrev CoherenceM (ρ : Type) := ReaderT ρ <| StateT State MetaMThe declarations below give the syntax corresponding to 2-morphisms and the monad expressing that Lean expressions can be converted into this syntax.
/-- Expressions for 2-morphisms. -/
inductive Mor₂ : Type where
/-- The expression for `Iso.hom`. -/
| isoHom (e : Expr) (isoLift : IsoLift) (iso : Mor₂Iso) : Mor₂
/-- The expression for `Iso.inv`. -/
| isoInv (e : Expr) (isoLift : IsoLift) (iso : Mor₂Iso) : Mor₂
/-- The expression for the identity `𝟙 f`. -/
| id (e : Expr) (isoLift : IsoLift) (f : Mor₁) : Mor₂
/-- The expression for the composition `η ≫ θ`. -/
| comp (e : Expr) (isoLift? : Option IsoLift) (f g h : Mor₁) (η θ : Mor₂) : Mor₂
/-- The expression for the left whiskering `f ◁ η` with `η : g ⟶ h`. -/
| whiskerLeft (e : Expr) (isoLift? : Option IsoLift) (f g h : Mor₁) (η : Mor₂) : Mor₂
/-- The expression for the right whiskering `η ▷ h` with `η : f ⟶ g`. -/
| whiskerRight (e : Expr) (isoLift? : Option IsoLift) (f g : Mor₁) (η : Mor₂) (h : Mor₁) : Mor₂
/-- The expression for the horizontal composition `η ◫ θ` with `η : f₁ ⟶ g₁` and `θ : f₂ ⟶ g₂`. -/
| horizontalComp (e : Expr) (isoLift? : Option IsoLift) (f₁ g₁ f₂ g₂ : Mor₁) (η θ : Mor₂) : Mor₂
/-- The expression for the coherence composition `η ⊗≫ θ := η ≫ α ≫ θ` with `η : f ⟶ g`
and `θ : h ⟶ i`. -/
| coherenceComp (e : Expr) (isoLift? : Option IsoLift) (f g h i : Mor₁)
(α : CoherenceHom) (η θ : Mor₂) : Mor₂
/-- The expression for an atomic non-structural 2-morphism. -/
| of (η : Atom) : Mor₂
deriving Inhabited/-- A monad equipped with the ability to construct `Mor₂` terms. -/
class MkMor₂ (m : Type → Type) where
/-- Construct a `Mor₂` term from a lean expression. -/
ofExpr (e : Expr) : m Mor₂With this setup in place, the declarations below give the algorithm that generates proof terms from the proof of the coherence theorem.
The normalized 1-morphisms from the proof appear in Lean as
NormalizedHom:
/-- Type of normalized 1-morphisms `((... ≫ h) ≫ g) ≫ f`. -/
inductive NormalizedHom : Type
/-- The identity 1-morphism `𝟙 a`. -/
| nil (e : Mor₁) (a : Obj) : NormalizedHom
/-- The `cons` composes an atomic 1-morphism at the end of a normalized 1-morphism. -/
| cons (e : Mor₁) : NormalizedHom → Atom₁ → NormalizedHom
deriving Inhabited
The recursive normalization procedure returns
Normalize.Result,
which packages together the chosen normal form and the coherence isomorphism into it:
/-- The result of normalizing a 1-morphism. -/
structure Normalize.Result where
/-- The normalized 1-morphism. -/
normalizedHom : NormalizedHom
/-- The 2-morphism from the original 1-morphism to the normalized 1-morphism. -/
toNormalize : Mor₂Iso
deriving Inhabited
The function that constructs this data is
normalize:
/-- Meta version of `CategoryTheory.FreeBicategory.normalizeIso`. -/
def normalize (p : NormalizedHom) (f : Mor₁) :
CoherenceM ρ Normalize.Result := do
match f with
| .id _ _ =>
return ⟨p, ← rightUnitorM' p.e⟩
| .comp _ f g =>
let ⟨pf, η_f⟩ ← normalize p f
let η_f' ← whiskerRightM η_f g
let ⟨pfg, η_g⟩ ← normalize pf g
let η ← comp₂M η_f' η_g
let α ← symmM (← associatorM' p.e f g)
let η' ← comp₂M α η
return ⟨pfg, η'⟩
| .of f =>
let pf ← NormalizedHom.consM p f
let α ← id₂M' pf.e
return ⟨pf, α⟩
The key lemma from the mathematical proof appears as
naturality,
and the final theorem proved from it appears as
pureCoherence:
/-- Meta version of `CategoryTheory.FreeBicategory.normalize_naturality`. -/
partial def naturality (nm : Name) (p : NormalizedHom) (η : Mor₂Iso) : CoherenceM ρ Expr := do
let result ← match η with
| .of _ => throwError m!"could not find a structural isomorphism, but {η.e}"
| .coherenceComp _ _ _ _ _ α η θ => withTraceNode nm (fun _ => return m!"monoidalComp") do
let α ← MonadCoherehnceHom.unfoldM α
let αθ ← comp₂M α θ
let ηαθ ← comp₂M η αθ
naturality nm p ηαθ
| .structuralAtom η => match η with
| .coherenceHom α => withTraceNode nm (fun _ => return m!"coherenceHom") do
let α ← MonadCoherehnceHom.unfoldM α
naturality nm p α
| .associator _ f g h => withTraceNode nm (fun _ => return m!"associator") do
let ⟨pf, η_f⟩ ← normalize p f
let ⟨pfg, η_g⟩ ← normalize pf g
let ⟨pfgh, η_h⟩ ← normalize pfg h
mkNaturalityAssociator p pf pfg pfgh f g h η_f η_g η_h
| .leftUnitor _ f => withTraceNode nm (fun _ => return m!"leftUnitor") do
let ⟨pf, η_f⟩ ← normalize p f
mkNaturalityLeftUnitor p pf f η_f
| .rightUnitor _ f => withTraceNode nm (fun _ => return m!"rightUnitor") do
let ⟨pf, η_f⟩ ← normalize p f
mkNaturalityRightUnitor p pf f η_f
| .id _ f => withTraceNode nm (fun _ => return m!"id") do
let ⟨pf, η_f⟩ ← normalize p f
mkNaturalityId p pf f η_f
| .comp _ f g h η θ => withTraceNode nm (fun _ => return m!"comp") do
let ⟨pf, η_f⟩ ← normalize p f
let ⟨_, η_g⟩ ← normalize p g
let ⟨_, η_h⟩ ← normalize p h
let ih_η ← naturality nm p η
let ih_θ ← naturality nm p θ
mkNaturalityComp p pf f g h η θ η_f η_g η_h ih_η ih_θ
| .whiskerLeft _ f g h η => withTraceNode nm (fun _ => return m!"whiskerLeft") do
let ⟨pf, η_f⟩ ← normalize p f
let ⟨pfg, η_fg⟩ ← normalize pf g
let ⟨_, η_fh⟩ ← normalize pf h
let ih ← naturality nm pf η
mkNaturalityWhiskerLeft p pf pfg f g h η η_f η_fg η_fh ih
| .whiskerRight _ f g η h => withTraceNode nm (fun _ => return m!"whiskerRight") do
let ⟨pf, η_f⟩ ← normalize p f
let ⟨_, η_g⟩ ← normalize p g
let ⟨pfh, η_fh⟩ ← normalize pf h
let ih ← naturality nm p η
mkNaturalityWhiskerRight p pf pfh f g h η η_f η_g η_fh ih
| .horizontalComp _ f₁ g₁ f₂ g₂ η θ => withTraceNode nm (fun _ => return m!"hComp") do
let ⟨pf₁, η_f₁⟩ ← normalize p f₁
let ⟨_, η_g₁⟩ ← normalize p g₁
let ⟨pf₁f₂, η_f₂⟩ ← normalize pf₁ f₂
let ⟨_, η_g₂⟩ ← normalize pf₁ g₂
let ih_η ← naturality nm p η
let ih_θ ← naturality nm pf₁ θ
mkNaturalityHorizontalComp p pf₁ pf₁f₂ f₁ g₁ f₂ g₂ η θ η_f₁ η_g₁ η_f₂ η_g₂ ih_η ih_θ
| .inv _ f g η => withTraceNode nm (fun _ => return m!"inv") do
let ⟨pf, η_f⟩ ← normalize p f
let ⟨_, η_g⟩ ← normalize p g
let ih_η ← naturality nm p η
mkNaturalityInv p pf f g η η_f η_g ih_η
withTraceNode nm (fun _ => return m!"{checkEmoji} {← inferType result}") do
if ← isTracingEnabledFor nm then addTrace nm m!"proof: {result}"
return result/-- Close the goal of the form `η = θ`, where `η` and `θ` are 2-isomorphisms made up only of
associators, unitors, and identities. -/
def pureCoherence (ρ : Type) [Context ρ] [MkMor₂ (CoherenceM ρ)]
[MonadMor₁ (CoherenceM ρ)] [MonadMor₂Iso (CoherenceM ρ)]
[MonadCoherehnceHom (CoherenceM ρ)] [MonadNormalizeNaturality (CoherenceM ρ)]
[MkEqOfNaturality (CoherenceM ρ)]
(nm : Name) (mvarId : MVarId) : MetaM (List MVarId) :=
mvarId.withContext do
withTraceNode nm (fun ex => match ex with
| .ok _ => return m!"{checkEmoji} coherence equality: {← mvarId.getType}"
| .error err => return m!"{crossEmoji} {err.toMessageData}") do
let e ← instantiateMVars <| ← mvarId.getType
let some (_, η, θ) := (← whnfR e).eq?
| throwError "coherence requires an equality goal"
let ctx : ρ ← mkContext η
CoherenceM.run (ctx := ctx) do
let some ηIso := (← MkMor₂.ofExpr η).isoLift? |
throwError "could not find a structural isomorphism, but {η}"
let some θIso := (← MkMor₂.ofExpr θ).isoLift? |
throwError "could not find a structural isomorphism, but {θ}"
let f ← ηIso.e.srcM
let g ← ηIso.e.tgtM
let a := f.src
let nil ← normalizedHom.nilM a
let ⟨_, η_f⟩ ← normalize nil f
let ⟨_, η_g⟩ ← normalize nil g
let Hη ← withTraceNode nm (fun ex => do return m!"{exceptEmoji ex} LHS") do
naturality nm nil ηIso.e
let Hθ ← withTraceNode nm (fun ex => do return m!"{exceptEmoji ex} RHS") do
naturality nm nil θIso.e
let H ← mkEqOfNaturality η θ ηIso θIso η_f η_g Hη Hθ
mvarId.apply HThe next two subsections explain how the monoidal and bicategorical front ends feed their goals into this shared core.
2.1.2. Monoidal Front End
The monoidal front end first extracts the monoidal data from the goal. It then reads the relevant
Lean.Expr terms into the syntax expected by the shared core. The declarations
that do this are
mkContext?,
mor₁OfExpr,
Mor₂IsoOfExpr, and
Mor₂OfExpr.
/-- Populate a `context` object for evaluating `e`. -/
def mkContext? (e : Expr) : MetaM (Option Context) := do
let e ← instantiateMVars e
let type ← instantiateMVars <| ← inferType e
match (← whnfR type).getAppFnArgs with
| (``Quiver.Hom, #[_, _, f, _]) =>
let C ← instantiateMVars <| ← inferType f
let .succ level₁ ← getLevel C | return none
let .succ level₂ ← getLevel type | return none
let some instCat ← synthInstance?
(mkAppN (.const ``Category [level₂, level₁]) #[C]) | return none
let instMonoidal? ← synthInstance?
(mkAppN (.const ``MonoidalCategory [level₂, level₁]) #[C, instCat])
return some ⟨level₂, level₁, C, instCat, instMonoidal?⟩
| _ => return none/-- Construct a `Mor₁` expression from a Lean expression. -/
partial def mor₁OfExpr (e : Expr) : MonoidalM Mor₁ := do
if let some f := (← get).cache.find? e then
return f
let f ←
if let some a ← id₁? e then
MonadMor₁.id₁M a
else if let some (f, g) ← comp? e then
MonadMor₁.comp₁M (← mor₁OfExpr f.e) (← mor₁OfExpr g.e)
else
return Mor₁.of ⟨e, ⟨none⟩, ⟨none⟩⟩
modify fun s => { s with cache := s.cache.insert e f }
return f/-- Construct a `Mor₂Iso` term from a Lean expression. -/
partial def Mor₂IsoOfExpr (e : Expr) : MonoidalM Mor₂Iso := do
match (← whnfR e).getAppFnArgs with
| (``MonoidalCategoryStruct.associator, #[_, _, _, f, g, h]) =>
associatorM' (← MkMor₁.ofExpr f) (← MkMor₁.ofExpr g) (← MkMor₁.ofExpr h)
| (``MonoidalCategoryStruct.leftUnitor, #[_, _, _, f]) =>
leftUnitorM' (← MkMor₁.ofExpr f)
| (``MonoidalCategoryStruct.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 θ)
| (``MonoidalCategory.whiskerLeftIso, #[_, _, _, f, _, _, η]) =>
whiskerLeftM (← MkMor₁.ofExpr f) (← Mor₂IsoOfExpr η)
| (``MonoidalCategory.whiskerRightIso, #[_, _, _, _, _, η, h]) =>
whiskerRightM (← Mor₂IsoOfExpr η) (← MkMor₁.ofExpr h)
| (``tensorIso, #[_, _, _, _, _, _, _, η, θ]) =>
horizontalCompM (← Mor₂IsoOfExpr η) (← Mor₂IsoOfExpr θ)
| (``monoidalIsoComp, #[_, _, _, g, h, _, inst, η, θ]) =>
let α ← coherenceHomM (← MkMor₁.ofExpr g) (← MkMor₁.ofExpr h) inst
coherenceCompM α (← Mor₂IsoOfExpr η) (← Mor₂IsoOfExpr θ)
| (``MonoidalCoherence.iso, #[_, _, f, g, inst]) =>
coherenceHomM' (← MkMor₁.ofExpr f) (← MkMor₁.ofExpr g) inst
| _ =>
return .of ⟨e, ← MkMor₁.ofExpr (← srcExprOfIso e), ← MkMor₁.ofExpr (← tgtExprOfIso e)⟩open MonadMor₂ in
/-- Construct a `Mor₂` term from a Lean expression. -/
partial def Mor₂OfExpr (e : Expr) : MonoidalM 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 θ)
| (``MonoidalCategoryStruct.whiskerLeft, #[_, _, _, f, _, _, η]) =>
whiskerLeftM (← MkMor₁.ofExpr f) (← Mor₂OfExpr η)
| (``MonoidalCategoryStruct.whiskerRight, #[_, _, _, _, _, η, h]) =>
whiskerRightM (← Mor₂OfExpr η) (← MkMor₁.ofExpr h)
| (``MonoidalCategoryStruct.tensorHom, #[_, _, _, _, _, _, _, η, θ]) =>
horizontalCompM (← Mor₂OfExpr η) (← Mor₂OfExpr θ)
| (``monoidalComp, #[_, _, _, 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)⟩
In particular, mor₁OfExpr
turns tensor expressions for objects into the 1-morphism language used by the shared core, while
Mor₂IsoOfExpr
and
Mor₂OfExpr
recognize the corresponding coherence isomorphisms and morphisms over those object expressions. Once
this front end has done its work,
monoidal_coherence
just calls the shared core with the monoidal context.
2.1.3. Bicategorical Front End
The bicategorical front end plays the same role for bicategories. It extracts the bicategory from the goal and reads the relevant
Lean.Expr terms directly into the syntax expected by the shared core. The relevant
declarations are
mkContext?,
mor₁OfExpr,
Mor₂IsoOfExpr, and
Mor₂OfExpr.
/-- Populate a `context` object for evaluating `e`. -/
def mkContext? (e : Expr) : MetaM (Option Context) := do
let e ← instantiateMVars e
let type ← instantiateMVars <| ← inferType e
match (← whnfR (← inferType e)).getAppFnArgs with
| (``Quiver.Hom, #[_, _, f, _]) =>
let fType ← instantiateMVars <| ← inferType f
match (← whnfR fType).getAppFnArgs with
| (``Quiver.Hom, #[_, _, a, _]) =>
let B ← inferType a
let .succ level₀ ← getLevel B | return none
let .succ level₁ ← getLevel fType | return none
let .succ level₂ ← getLevel type | return none
let some instBicategory ← synthInstance?
(mkAppN (.const ``Bicategory [level₂, level₁, level₀]) #[B]) | return none
return some ⟨level₂, level₁, level₀, B, instBicategory⟩
| _ => return none
| _ => return none/-- Construct a `Mor₁` expression from a Lean expression. -/
partial def mor₁OfExpr (e : Expr) : BicategoryM Mor₁ := do
if let some f := (← get).cache.find? e then
return f
let f ←
if let some a ← id₁? e then
MonadMor₁.id₁M a
else if let some (f, g) ← comp? e then
MonadMor₁.comp₁M (← mor₁OfExpr f.e) (← mor₁OfExpr g.e)
else
return Mor₁.of ⟨e, ⟨← srcExpr e⟩, ⟨ ← tgtExpr e⟩⟩
modify fun s => { s with cache := s.cache.insert e f }
return f/-- 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)⟩open MonadMor₂ in
/-- 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)⟩
Once this front end has done its work,
bicategory_coherence
just calls the shared core with the bicategorical context.