Structures · Tactics and metaprogramming
CategoryTheory.MonoidalCoherence
A typeclass carrying a choice of monoidal structural isomorphism between two objects.
Used by the ⊗≫ monoidal 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.MonoidalCoherence.right'_iso
- CategoryTheory.MonoidalCoherence.assoc'
- CategoryTheory.MonoidalCoherence.left
- CategoryTheory.MonoidalCoherence.tensor_right
- CategoryTheory.MonoidalCoherence.iso
- CategoryTheory.MonoidalCoherence.whiskerRight
- CategoryTheory.MonoidalCoherence.tensor_right'_iso
- CategoryTheory.MonoidalCoherence.tensor_right'
- Mathlib.Tactic.Monoidal.StructuralOfExpr_monoidalComp
- CategoryTheory.MonoidalCoherence.left'_iso
- CategoryTheory.MonoidalCoherence.right
- CategoryTheory.MonoidalCoherence.whiskerRight_iso
- CategoryTheory.MonoidalCoherence.assoc'_iso
- CategoryTheory.MonoidalCoherence.left_iso
- CategoryTheory.MonoidalCoherence.tensor_right_iso
- CategoryTheory.MonoidalCoherence.assoc_iso
- CategoryTheory.MonoidalCoherence.whiskerLeft_iso
- CategoryTheory.MonoidalCoherence.left'
- CategoryTheory.MonoidalCoherence.right_iso
- CategoryTheory.monoidalComp
- CategoryTheory.monoidalIso
- CategoryTheory.monoidalIsoComp
- CategoryTheory.MonoidalCoherence.whiskerLeft
- CategoryTheory.MonoidalCoherence.right'
- CategoryTheory.MonoidalCoherence.assoc
Ancestors0
No ancestors.