Coherence Tactics

 Coherence Tactics for Monoidal Categories and Bicategories in Lean🔗

Author: Yuma Mizuno

Source repository: yuma-mizuno/coherence-tactics

This note explains two tactics in Lean: monoidal for equalities of morphisms in monoidal categories, and bicategory for equalities of 2-morphisms in bicategories. These tactics are available in Mathlib.

Contents

  1. 1. Overview
  2. 2. The Coherence Theorem
  3. 3. Monoidal and Bicategory Tactics