A coherence
tactic for bicategories, and ⊗≫
(composition up to associators) #
We provide a bicategory_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 bicategoricalComp
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 Mathlib.Tactic.CategoryTheory.Coherence
at the same time as the coherence
tactic for monoidal categories.
- lift : CategoryTheory.FreeBicategory.of.obj a ⟶ CategoryTheory.FreeBicategory.of.obj b
A lift of a morphism to the free bicategory. This should only exist for "structural" morphisms.
A typeclass carrying a choice of lift of a 1-morphism from B
to FreeBicategory B
.
Instances
- lift : Mathlib.Tactic.BicategoryCoherence.LiftHom.lift f ⟶ Mathlib.Tactic.BicategoryCoherence.LiftHom.lift g
A lift of a 2-morphism to the free bicategory. This should only exist for "structural" 2-morphisms.
A typeclass carrying a choice of lift of a 2-morphism from B
to FreeBicategory B
.
Instances
- hom' : f ⟶ g
The chosen structural isomorphism between to 1-morphisms.
- isIso : CategoryTheory.IsIso Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom'
A typeclass carrying a choice of bicategorical structural isomorphism between two objects.
Used by the ⊗≫
bicategorical composition operator, and the coherence
tactic.
Instances
The chosen structural isomorphism between to 1-morphisms.
Instances For
Construct an isomorphism between two objects in a bicategorical category out of unitors and associators.
Instances For
Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.
Instances For
Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.
Instances For
Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.
Instances For
Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.
Instances For
Helper function for throwing exceptions.
Instances For
Helper function for throwing exceptions with respect to the main goal.
Instances For
Auxiliary definition for bicategorical_coherence
.
Instances For
Coherence tactic for bicategories.
Instances For
Coherence tactic for bicategories.
Use pure_coherence
instead, which is a frontend to this one.
Instances For
Simp lemmas for rewriting a 2-morphism into a normal form.
Instances For
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.