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 : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr

  The naturality for the associator.

• mkNaturalityLeftUnitor : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr

  The naturality for the left unitor.

• mkNaturalityRightUnitor : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr

  The naturality for the right unitor.

• mkNaturalityId : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr

  The naturality for the identity.

• mkNaturalityComp : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → Lean.Expr → m Lean.Expr

  The naturality for the composition.

• mkNaturalityWhiskerLeft : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → m Lean.Expr

  The naturality for the left whiskering.

• mkNaturalityWhiskerRight : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → m Lean.Expr

  The naturality for the right whiskering.

• mkNaturalityHorizontalComp : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → Lean.Expr → m Lean.Expr

  The naturality for the horizontal composition.

• mkNaturalityInv : Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.NormalizedHom → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → 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 → Lean.Expr → Mathlib.Tactic.BicategoryLike.IsoLift → Mathlib.Tactic.BicategoryLike.IsoLift → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → 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.