Lean4
/-- 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 H
