mathlib documentation

category_theory.bicategory.coherence_tactic

A coherence tactic for bicategories, and ⊗≫ (composition up to associators) #

We provide a coherence tactic, which proves that any two 2-morphisms (with the same source and target) in a bicategory which are built out of associators and unitors are equal.

We also provide f ⊗≫ g, the bicategorical_comp operation, which automatically inserts associators and unitors as needed to make the target of f match the source of g.

This file mainly deals with the type class setup for the coherence tactic. The actual front end tactic is given in category_theory/monooidal/coherence.lean at the same time as the coherence tactic for monoidal categories.

@[class]
structure category_theory.bicategory.lift_hom {B : Type u} [category_theory.bicategory B] {a b : B} (f : a b) :
Type (max u v)

A typeclass carrying a choice of lift of a 1-morphism from B to free_bicategory B.

Instances of this typeclass
Instances of other typeclasses for category_theory.bicategory.lift_hom
  • category_theory.bicategory.lift_hom.has_sizeof_inst

Construct an isomorphism between two objects in a bicategorical category out of unitors and associators.

Equations

Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.

Equations

Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.

Equations
@[simp]
theorem category_theory.bicategory.bicategorical_comp_refl {B : Type u} [category_theory.bicategory B] {a b : B} {f g h : a b} (η : f g) (θ : g h) :

Coherence tactic for bicategories.

Simp lemmas for rewriting a 2-morphism into a normal form.

@[nolint]

Auxiliary simp lemma for the coherence tactic: this move brackets to the left in order to expose a maximal prefix built out of unitors and associators.