Coherence tactic

This file provides a meta framework for the coherence tactic, which solves goals of the form η = θ, where η and θ are 2-morphism in a bicategory or morphisms in a monoidal category made up only of associators, unitors, and identities.

The function defined here is a meta reimplementation of the formalized coherence theorems provided in the following files:

• Mathlib.CategoryTheory.Monoidal.Free.Coherence
• Mathlib.CategoryTheory.Bicategory.Coherence See these files for a mathematical explanation of the proof of the coherence theorem.

The actual tactics that users will use are given in

• Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
• Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

structure Mathlib.Tactic.BicategoryLike.Normalize.Result : Type

The result of normalizing a 1-morphism.

• normalizedHom : NormalizedHom

  The normalized 1-morphism.

• toNormalize : Mor₂Iso

  The 2-morphism from the original 1-morphism to the normalized 1-morphism.

instance Mathlib.Tactic.BicategoryLike.Normalize.instInhabitedResult : Inhabited Result

Equations

• Mathlib.Tactic.BicategoryLike.Normalize.instInhabitedResult = { default := { normalizedHom := default, toNormalize := default } }

def Mathlib.Tactic.BicategoryLike.normalize {ρ : Type} [MonadMor₁ (CoherenceM ρ)] [MonadMor₂Iso (CoherenceM ρ)] (p : NormalizedHom) (f : Mor₁) : CoherenceM ρ Normalize.Result

Meta version of CategoryTheory.FreeBicategory.normalizeIso.

Equations

• One or more equations did not get rendered due to their size.

class Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality (m : Type → Type) : Type

Lemmas to prove the meta version of CategoryTheory.FreeBicategory.normalize_naturality.

• mkNaturalityAssociator (p pf pfg pfgh : NormalizedHom) (f g h : Mor₁) (η_f η_g η_h : Mor₂Iso) : m Lean.Expr

  The naturality for the associator.

• mkNaturalityLeftUnitor (p pf : NormalizedHom) (f : Mor₁) (η_f : Mor₂Iso) : m Lean.Expr

  The naturality for the left unitor.

• mkNaturalityRightUnitor (p pf : NormalizedHom) (f : Mor₁) (η_f : Mor₂Iso) : m Lean.Expr

  The naturality for the right unitor.

• mkNaturalityId (p pf : NormalizedHom) (f : Mor₁) (η_f : Mor₂Iso) : m Lean.Expr

  The naturality for the identity.

• mkNaturalityComp (p pf : NormalizedHom) (f g h : Mor₁) (η θ η_f η_g η_h : Mor₂Iso) (ih_η ih_θ : Lean.Expr) : m Lean.Expr

  The naturality for the composition.

• mkNaturalityWhiskerLeft (p pf pfg : NormalizedHom) (f g h : Mor₁) (η η_f η_fg η_fh : Mor₂Iso) (ih_η : Lean.Expr) : m Lean.Expr

  The naturality for the left whiskering.

• mkNaturalityWhiskerRight (p pf pfh : NormalizedHom) (f g h : Mor₁) (η η_f η_g η_fh : Mor₂Iso) (ih_η : Lean.Expr) : m Lean.Expr

  The naturality for the right whiskering.

• mkNaturalityHorizontalComp (p pf₁ pf₁f₂ : NormalizedHom) (f₁ g₁ f₂ g₂ : Mor₁) (η θ η_f₁ η_g₁ η_f₂ η_g₂ : Mor₂Iso) (ih_η ih_θ : Lean.Expr) : m Lean.Expr

  The naturality for the horizontal composition.

• mkNaturalityInv (p pf : NormalizedHom) (f g : Mor₁) (η η_f η_g : Mor₂Iso) (ih_η : Lean.Expr) : m Lean.Expr

  The naturality for the inverse.

partial def Mathlib.Tactic.BicategoryLike.naturality {ρ : Type} [MonadMor₁ (CoherenceM ρ)] [MonadMor₂Iso (CoherenceM ρ)] [MonadCoherehnceHom (CoherenceM ρ)] [MonadNormalizeNaturality (CoherenceM ρ)] (nm : Lean.Name) (p : NormalizedHom) (η : Mor₂Iso) : CoherenceM ρ Lean.Expr

Meta version of CategoryTheory.FreeBicategory.normalize_naturality.

class Mathlib.Tactic.BicategoryLike.MkEqOfNaturality (m : Type → Type) : Type

Prove the equality between structural isomorphisms using the naturality of normalize.

• mkEqOfNaturality (η θ : Lean.Expr) (η' θ' : IsoLift) (η_f η_g : Mor₂Iso) (Hη Hθ : Lean.Expr) : m Lean.Expr

  Auxiliary function for pureCoherence.

def Mathlib.Tactic.BicategoryLike.pureCoherence (ρ : Type) [Context ρ] [MkMor₂ (CoherenceM ρ)] [MonadMor₁ (CoherenceM ρ)] [MonadMor₂Iso (CoherenceM ρ)] [MonadCoherehnceHom (CoherenceM ρ)] [MonadNormalizeNaturality (CoherenceM ρ)] [MkEqOfNaturality (CoherenceM ρ)] (nm : Lean.Name) (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Close the goal of the form η = θ, where η and θ are 2-isomorphisms made up only of associators, unitors, and identities.

Equations

• One or more equations did not get rendered due to their size.