Lean4
/-- Evaluate the expression `f ◁ η` into a normalized form. -/
def evalWhiskerLeft : Mor₁ → NormalExpr → CoherenceM ρ Eval.Result
| f, .nil _ α => do
return ⟨← nilM (← whiskerLeftM f α), ← mkEvalWhiskerLeftNil f α⟩
| .of f, .cons _ α η ηs => do
let η' ← MonadWhiskerLeft.whiskerLeftM f η
let ⟨θ, e_θ⟩ ← evalWhiskerLeft (.of f) ηs
let η'' ← consM (← whiskerLeftM (.of f) α) η' θ
return ⟨η'', ← mkEvalWhiskerLeftOfCons f α η ηs θ e_θ⟩
| .comp _ f g, η => do
let ⟨θ, e_θ⟩ ← evalWhiskerLeft g η
let ⟨ι, e_ι⟩ ← evalWhiskerLeft f θ
let h ← η.srcM
let h' ← η.tgtM
let ⟨ι', e_ι'⟩ ← evalComp ι (← NormalExpr.associatorInvM f g h')
let ⟨ι'', e_ι''⟩ ← evalComp (← NormalExpr.associatorM f g h) ι'
return ⟨ι'', ← mkEvalWhiskerLeftComp f g η θ ι ι' ι'' e_θ e_ι e_ι' e_ι''⟩
| .id _ _, η => do
let f ← η.srcM
let g ← η.tgtM
let ⟨η', e_η'⟩ ← evalComp η (← NormalExpr.leftUnitorInvM g)
let ⟨η'', e_η''⟩ ← evalComp (← NormalExpr.leftUnitorM f) η'
return ⟨η'', ← mkEvalWhiskerLeftId η η' η'' e_η' e_η''⟩
