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 : Mathlib.Tactic.BicategoryLike.NormalizedHom

  The normalized 1-morphism.

• toNormalize : Mathlib.Tactic.BicategoryLike.Mor₂Iso

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

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

Equations

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

def Mathlib.Tactic.BicategoryLike.normalize {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] (p : Mathlib.Tactic.BicategoryLike.NormalizedHom) (f : Mathlib.Tactic.BicategoryLike.Mor₁) : Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.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 : Mathlib.Tactic.BicategoryLike.NormalizedHom) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁) (η_f η_g η_h : Mathlib.Tactic.BicategoryLike.Mor₂Iso) : m Lean.Expr

  The naturality for the associator.

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

  The naturality for the left unitor.

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

  The naturality for the right unitor.

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

  The naturality for the identity.

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

  The naturality for the composition.

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

  The naturality for the left whiskering.

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

  The naturality for the right whiskering.

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

  The naturality for the horizontal composition.

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

  The naturality for the inverse.

partial def Mathlib.Tactic.BicategoryLike.naturality {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] (nm : Lean.Name) (p : Mathlib.Tactic.BicategoryLike.NormalizedHom) (η : Mathlib.Tactic.BicategoryLike.Mor₂Iso) : Mathlib.Tactic.BicategoryLike.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) (η' θ' : Mathlib.Tactic.BicategoryLike.IsoLift) (η_f η_g : Mathlib.Tactic.BicategoryLike.Mor₂Iso) (Hη Hθ : Lean.Expr) : m Lean.Expr

  Auxiliary function for pureCoherence.

def Mathlib.Tactic.BicategoryLike.pureCoherence (ρ : Type) [Mathlib.Tactic.BicategoryLike.Context ρ] [Mathlib.Tactic.BicategoryLike.MkMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEqOfNaturality (Mathlib.Tactic.BicategoryLike.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.