Structures · Tactics and metaprogramming
CategoryTheory.BicategoricalCoherence
A typeclass carrying a choice of bicategorical structural isomorphism between two objects.
Used by the ⊗≫ bicategorical composition operator, and the coherence tactic.
- Shape
- 2 explicit arguments · adds iso
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by25
- CategoryTheory.BicategoricalCoherence.tensorRight
- CategoryTheory.BicategoricalCoherence.right'
- CategoryTheory.bicategoricalIso
- CategoryTheory.BicategoricalCoherence.whiskerRight
- CategoryTheory.BicategoricalCoherence.tensorRight'
- CategoryTheory.BicategoricalCoherence.tensorRight_iso
- CategoryTheory.BicategoricalCoherence.assoc'_iso
- CategoryTheory.BicategoricalCoherence.left
- CategoryTheory.BicategoricalCoherence.assoc_iso
- Mathlib.Tactic.Bicategory.StructuralOfExpr_bicategoricalComp
- CategoryTheory.BicategoricalCoherence.left_iso
- CategoryTheory.BicategoricalCoherence.whiskerLeft
- CategoryTheory.BicategoricalCoherence.left'_iso
- CategoryTheory.BicategoricalCoherence.right_iso
- CategoryTheory.BicategoricalCoherence.left'
- CategoryTheory.BicategoricalCoherence.whiskerLeft_iso
- CategoryTheory.BicategoricalCoherence.assoc'
- CategoryTheory.BicategoricalCoherence.right
- CategoryTheory.BicategoricalCoherence.assoc
- CategoryTheory.bicategoricalComp
- CategoryTheory.BicategoricalCoherence.iso
- CategoryTheory.bicategoricalIsoComp
- CategoryTheory.BicategoricalCoherence.right'_iso
- CategoryTheory.BicategoricalCoherence.whiskerRight_iso
- CategoryTheory.BicategoricalCoherence.tensorRight'_iso
Ancestors0
No ancestors.