# Datatypes for bicategory like structures #

This file defines the basic datatypes for bicategory like structures. We will use these datatypes to write tactics that can be applied to both monoidal categories and bicategories:

- `Obj`: objects type
- `Atom₁`: atomic 1-morphisms type
- `Mor₁`: 1-morphisms type
- `Atom`: atomic non-structural 2-morphisms type
- `Mor₂`: 2-morphisms type
- `AtomIso`: atomic non-structural 2-isomorphisms type
- `Mor₂Iso`: 2-isomorphisms type
- `NormalizedHom`: normalized 1-morphisms type

A term of these datatypes wraps the corresponding `Expr` term, which can be extracted by e.g. `η.e` for `η : Mor₂`.

The operations of these datatypes are defined in a monad `m` with the corresponding typeclasses:

- `MonadMor₁`: operations on `Mor₁`
- `MonadMor₂Iso`: operations on `Mor₂Iso`
- `MonadMor₂`: operations on `Mor₂`

For example, a monad `m` with `[MonadMor₂ m]` provides the operation `MonadMor₂.comp₂M : Mor₂Iso → Mor₂Iso → m Mor₂Iso`, which constructs the expression for the composition `η ≫ θ` of 2-morphisms `η` and `θ` in the monad `m`.

source
structure Mathlib.Tactic.BicategoryLike.Obj :
Type

Expressions for objects.

- e? : Option Lean.Expr

  Extracts a lean expression from an `Obj` term. Return `none` in the monoidal category context.

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedObj :
Inhabited Obj
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedObj = { default := Mathlib.Tactic.BicategoryLike.instInhabitedObj.default }

source
def Mathlib.Tactic.BicategoryLike.instInhabitedObj.default :
Obj
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedObj.default = { e? := default }

Instances For

source
def Mathlib.Tactic.BicategoryLike.Obj.e (a : Obj) :
Lean.Expr

Extract a lean expression from an `Obj` term.

Equations

- a.e = a.e?.get!

Instances For

source
structure Mathlib.Tactic.BicategoryLike.Atom₁ :
Type

Expressions for atomic 1-morphisms.

- e : Lean.Expr

  Extract a lean expression from an `Atom₁` term.

- src : Obj

  The domain of the 1-morphism.

- tgt : Obj

  The codomain of the 1-morphism.

Instances For

source
def Mathlib.Tactic.BicategoryLike.instInhabitedAtom₁.default :
Atom₁
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedAtom₁.default = { e := default, src := default, tgt := default }

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedAtom₁ :
Inhabited Atom₁
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedAtom₁ = { default := Mathlib.Tactic.BicategoryLike.instInhabitedAtom₁.default }

source
class Mathlib.Tactic.BicategoryLike.MkAtom₁ (m : Type → Type) :
Type

A monad equipped with the ability to construct `Atom₁` terms.

- ofExpr (e : Lean.Expr) : m Atom₁

  Construct a `Atom₁` term from a lean expression.

Instances

source
inductive Mathlib.Tactic.BicategoryLike.Mor₁ :
Type

Expressions for 1-morphisms.

- id (e : Lean.Expr) (a : Obj) : Mor₁

  `id e a` is the expression for `𝟙 a`, where `e` is the underlying lean expression.

- comp (e : Lean.Expr) : Mor₁ → Mor₁ → Mor₁

  `comp e f g` is the expression for `f ≫ g`, where `e` is the underlying lean expression.

- of : Atom₁ → Mor₁

  The expression for an atomic 1-morphism.

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedMor₁ :
Inhabited Mor₁
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedMor₁ = { default := Mathlib.Tactic.BicategoryLike.instInhabitedMor₁.default }

source
def Mathlib.Tactic.BicategoryLike.instInhabitedMor₁.default :
Mor₁
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedMor₁.default = Mathlib.Tactic.BicategoryLike.Mor₁.id default default

Instances For

source
class Mathlib.Tactic.BicategoryLike.MkMor₁ (m : Type → Type) :
Type

A monad equipped with the ability to construct `Mor₁` terms.

- ofExpr (e : Lean.Expr) : m Mor₁

  Construct a `Mor₁` term from a lean expression.

Instances

source
def Mathlib.Tactic.BicategoryLike.Mor₁.e :
Mor₁ → Lean.Expr

The underlying lean expression of a 1-morphism.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₁.id e a).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₁.comp e a a_1).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₁.of a).e = a.e

Instances For

source
def Mathlib.Tactic.BicategoryLike.Mor₁.src :
Mor₁ → Obj

The domain of a 1-morphism.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₁.id e a).src = a
- (Mathlib.Tactic.BicategoryLike.Mor₁.comp e a a_1).src = a.src
- (Mathlib.Tactic.BicategoryLike.Mor₁.of a).src = a.src

Instances For

source
def Mathlib.Tactic.BicategoryLike.Mor₁.tgt :
Mor₁ → Obj

The codomain of a 1-morphism.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₁.id e a).tgt = a
- (Mathlib.Tactic.BicategoryLike.Mor₁.comp e a a_1).tgt = a_1.tgt
- (Mathlib.Tactic.BicategoryLike.Mor₁.of a).tgt = a.tgt

Instances For

source
def Mathlib.Tactic.BicategoryLike.Mor₁.toList :
Mor₁ → List Atom₁

Converts a 1-morphism into a list of its components.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₁.id e a).toList = []
- (Mathlib.Tactic.BicategoryLike.Mor₁.comp e a a_1).toList = a.toList ++ a_1.toList
- (Mathlib.Tactic.BicategoryLike.Mor₁.of a).toList = [a]

Instances For

source
class Mathlib.Tactic.BicategoryLike.MonadMor₁ (m : Type → Type) :
Type

A monad equipped with the ability to manipulate 1-morphisms.

- id₁M (a : Obj) : m Mor₁

  The expression for `𝟙 a`.

- comp₁M (f g : Mor₁) : m Mor₁

  The expression for `f ≫ g`.

Instances

source
structure Mathlib.Tactic.BicategoryLike.CoherenceHom :
Type

Expressions for coherence isomorphisms (i.e., structural 2-morphisms given by `BicategoricalCoherence.iso`).

- e : Lean.Expr

  The underlying lean expression of a coherence isomorphism.

- src : Mor₁

  The domain of a coherence isomorphism.

- tgt : Mor₁

  The codomain of a coherence isomorphism.

- inst : Lean.Expr

  The `BicategoricalCoherence` instance.

- unfold : Lean.Expr

  Extract the structural 2-isomorphism.

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedCoherenceHom :
Inhabited CoherenceHom
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedCoherenceHom = { default := Mathlib.Tactic.BicategoryLike.instInhabitedCoherenceHom.default }

source
def Mathlib.Tactic.BicategoryLike.instInhabitedCoherenceHom.default :
CoherenceHom
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedCoherenceHom.default = { e := default, src := default, tgt := default, inst := default, unfold := default }

Instances For

source
structure Mathlib.Tactic.BicategoryLike.AtomIso :
Type

Expressions for atomic non-structural 2-isomorphisms.

- e : Lean.Expr

  The underlying lean expression of an `AtomIso` term.

- src : Mor₁

  The domain of a 2-isomorphism.

- tgt : Mor₁

  The codomain of a 2-isomorphism.

Instances For

source
def Mathlib.Tactic.BicategoryLike.instInhabitedAtomIso.default :
AtomIso
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedAtomIso.default = { e := default, src := default, tgt := default }

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedAtomIso :
Inhabited AtomIso
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedAtomIso = { default := Mathlib.Tactic.BicategoryLike.instInhabitedAtomIso.default }

source
inductive Mathlib.Tactic.BicategoryLike.StructuralAtom :
Type

Expressions for atomic structural 2-morphisms.

- associator (e : Lean.Expr) (f g h : Mor₁) : StructuralAtom

  The expression for the associator `α_ f g h`.

- leftUnitor (e : Lean.Expr) (f : Mor₁) : StructuralAtom

  The expression for the left unitor `λ_ f`.

- rightUnitor (e : Lean.Expr) (f : Mor₁) : StructuralAtom

  The expression for the right unitor `ρ_ f`.

- id (e : Lean.Expr) (f : Mor₁) : StructuralAtom
- coherenceHom (α : CoherenceHom) : StructuralAtom

Instances For

source
def Mathlib.Tactic.BicategoryLike.instInhabitedStructuralAtom.default :
StructuralAtom
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedStructuralAtom.default = Mathlib.Tactic.BicategoryLike.StructuralAtom.associator default default default default

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedStructuralAtom :
Inhabited StructuralAtom
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedStructuralAtom = { default := Mathlib.Tactic.BicategoryLike.instInhabitedStructuralAtom.default }

source
inductive Mathlib.Tactic.BicategoryLike.Mor₂Iso :
Type

Expressions for 2-isomorphisms.

- structuralAtom (α : StructuralAtom) : Mor₂Iso
- comp (e : Lean.Expr) (f g h : Mor₁) (η θ : Mor₂Iso) : Mor₂Iso
- whiskerLeft (e : Lean.Expr) (f g h : Mor₁) (η : Mor₂Iso) : Mor₂Iso
- whiskerRight (e : Lean.Expr) (f g : Mor₁) (η : Mor₂Iso) (h : Mor₁) : Mor₂Iso
- horizontalComp (e : Lean.Expr) (f₁ g₁ f₂ g₂ : Mor₁) (η θ : Mor₂Iso) : Mor₂Iso
- inv (e : Lean.Expr) (f g : Mor₁) (η : Mor₂Iso) : Mor₂Iso
- coherenceComp (e : Lean.Expr) (f g h i : Mor₁) (α : CoherenceHom) (η θ : Mor₂Iso) : Mor₂Iso
- of (η : AtomIso) : Mor₂Iso

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedMor₂Iso :
Inhabited Mor₂Iso
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedMor₂Iso = { default := Mathlib.Tactic.BicategoryLike.instInhabitedMor₂Iso.default }

source
def Mathlib.Tactic.BicategoryLike.instInhabitedMor₂Iso.default :
Mor₂Iso
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedMor₂Iso.default = Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom default

Instances For

source
class Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom (m : Type → Type) :
Type

A monad equipped with the ability to unfold `BicategoricalCoherence.iso`.

- unfoldM (α : CoherenceHom) : m Mor₂Iso

  Unfold a coherence isomorphism.

Instances

source
def Mathlib.Tactic.BicategoryLike.StructuralAtom.e :
StructuralAtom → Lean.Expr

The underlying lean expression of a 2-isomorphism.

Equations

- (Mathlib.Tactic.BicategoryLike.StructuralAtom.associator e f g h).e = e
- (Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor e f).e = e
- (Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor e f).e = e
- (Mathlib.Tactic.BicategoryLike.StructuralAtom.id e f).e = e
- (Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom α).e = α.e

Instances For

source
def Mathlib.Tactic.BicategoryLike.StructuralAtom.srcM {m : Type → Type} [Monad m] [MonadMor₁ m] :
StructuralAtom → m Mor₁

The domain of a 2-isomorphism.

Equations

- One or more equations did not get rendered due to their size.
- (Mathlib.Tactic.BicategoryLike.StructuralAtom.id e f).srcM = pure f
- (Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom α).srcM = pure α.src

Instances For

source
def Mathlib.Tactic.BicategoryLike.StructuralAtom.tgtM {m : Type → Type} [Monad m] [MonadMor₁ m] :
StructuralAtom → m Mor₁

The codomain of a 2-isomorphism.

Equations

- One or more equations did not get rendered due to their size.
- (Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor e f).tgtM = pure f
- (Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor e f).tgtM = pure f
- (Mathlib.Tactic.BicategoryLike.StructuralAtom.id e f).tgtM = pure f
- (Mathlib.Tactic.BicategoryLike.StructuralAtom.coherenceHom α).tgtM = pure α.tgt

Instances For

source
def Mathlib.Tactic.BicategoryLike.Mor₂Iso.e :
Mor₂Iso → Lean.Expr

The underlying lean expression of a 2-isomorphism.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom α).e = α.e
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp e f g h η θ).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft e f g h η).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight e f g η h).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp e f₁ g₁ f₂ g₂ η θ).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv e f g η).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp e f g h i α η θ).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.of η).e = η.e

Instances For

source
def Mathlib.Tactic.BicategoryLike.Mor₂Iso.srcM {m : Type → Type} [Monad m] [MonadMor₁ m] :
Mor₂Iso → m Mor₁

The domain of a 2-isomorphism.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom α).srcM = α.srcM
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp e f g h η θ).srcM = pure f
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft e f g h η).srcM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M f g
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight e f g η h).srcM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M f h
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp e f₁ g₁ f₂ g₂ η θ).srcM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M f₁ f₂
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv e f g η).srcM = pure g
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp e f g h i α η θ).srcM = pure f
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.of η).srcM = pure η.src

Instances For

source
def Mathlib.Tactic.BicategoryLike.Mor₂Iso.tgtM {m : Type → Type} [Monad m] [MonadMor₁ m] :
Mor₂Iso → m Mor₁

The codomain of a 2-isomorphism.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom α).tgtM = α.tgtM
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp e f g h η θ).tgtM = pure h
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft e f g h η).tgtM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M f h
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight e f g η h).tgtM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M g h
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp e f₁ g₁ f₂ g₂ η θ).tgtM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M g₁ g₂
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv e f g η).tgtM = pure f
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp e f g h i α η θ).tgtM = pure i
- (Mathlib.Tactic.BicategoryLike.Mor₂Iso.of η).tgtM = pure η.tgt

Instances For

source
class Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (m : Type → Type) :
Type

A monad equipped with the ability to construct `Mor₂Iso` terms.

- associatorM (f g h : Mor₁) : m StructuralAtom

  The expression for the associator `α_ f g h`.

- leftUnitorM (f : Mor₁) : m StructuralAtom

  The expression for the left unitor `λ_ f`.

- rightUnitorM (f : Mor₁) : m StructuralAtom

  The expression for the right unitor `ρ_ f`.

- id₂M (f : Mor₁) : m StructuralAtom

  The expression for the identity `Iso.refl f`.

- coherenceHomM (f g : Mor₁) (inst : Lean.Expr) : m CoherenceHom

  The expression for the coherence isomorphism `⊗𝟙 : f ⟶ g`.

- comp₂M (η θ : Mor₂Iso) : m Mor₂Iso

  The expression for the composition `η ≪≫ θ`.

- whiskerLeftM (f : Mor₁) (η : Mor₂Iso) : m Mor₂Iso

  The expression for the left whiskering `whiskerLeftIso f η`.

- whiskerRightM (η : Mor₂Iso) (h : Mor₁) : m Mor₂Iso

  The expression for the right whiskering `whiskerRightIso η h`.

- horizontalCompM (η θ : Mor₂Iso) : m Mor₂Iso

  The expression for the horizontal composition `η ◫ θ`.

- symmM (η : Mor₂Iso) : m Mor₂Iso

  The expression for the inverse `Iso.symm η`.

- coherenceCompM (α : CoherenceHom) (η θ : Mor₂Iso) : m Mor₂Iso

  The expression for the coherence composition `η ≪⊗≫ θ := η ≪≫ α ≪≫ θ`.

Instances

source
def Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.associatorM' {m : Type → Type} [Monad m] [MonadMor₂Iso m] (f g h : Mor₁) :
m Mor₂Iso

The expression for the associator `α_ f g h`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.leftUnitorM' {m : Type → Type} [Monad m] [MonadMor₂Iso m] (f : Mor₁) :
m Mor₂Iso

The expression for the left unitor `λ_ f`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.rightUnitorM' {m : Type → Type} [Monad m] [MonadMor₂Iso m] (f : Mor₁) :
m Mor₂Iso

The expression for the right unitor `ρ_ f`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.id₂M' {m : Type → Type} [Monad m] [MonadMor₂Iso m] (f : Mor₁) :
m Mor₂Iso

The expression for the identity `Iso.refl f`.

Equations

- Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.id₂M' f = do let __do_lift ← Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.id₂M f pure (Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom __do_lift)

Instances For

source
def Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.coherenceHomM' {m : Type → Type} [Monad m] [MonadMor₂Iso m] (f g : Mor₁) (inst : Lean.Expr) :
m Mor₂Iso

The expression for the coherence isomorphism `⊗𝟙 : f ⟶ g`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
structure Mathlib.Tactic.BicategoryLike.Atom :
Type

Expressions for atomic non-structural 2-morphisms.

- e : Lean.Expr

  Extract a lean expression from an `Atom` expression.

- src : Mor₁

  The domain of a 2-morphism.

- tgt : Mor₁

  The codomain of a 2-morphism.

Instances For

source
def Mathlib.Tactic.BicategoryLike.instInhabitedAtom.default :
Atom
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedAtom.default = { e := default, src := default, tgt := default }

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedAtom :
Inhabited Atom
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedAtom = { default := Mathlib.Tactic.BicategoryLike.instInhabitedAtom.default }

source
structure Mathlib.Tactic.BicategoryLike.IsoLift :
Type

`Mor₂` expressions defined below will have the `isoLift? : Option IsoLift` field. For `η : Mor₂` such that `η.isoLift? = some isoLift`, we have the following data:

- `isoLift.e`: an expression for a 2-isomorphism `η'`, given as a `Mor₂Iso` term,
- `isoLift.eq`: a lean expression for the proof that `η'.hom = η`.

- e : Mor₂Iso

  The expression for the 2-isomorphism.

- eq : Lean.Expr

  The expression for the proof that the forward direction of the 2-isomorphism is equal to the original 2-morphism.

Instances For

source
inductive Mathlib.Tactic.BicategoryLike.Mor₂ :
Type

Expressions for 2-morphisms.

- isoHom (e : Lean.Expr) (isoLift : IsoLift) (iso : Mor₂Iso) : Mor₂

  The expression for `Iso.hom`.

- isoInv (e : Lean.Expr) (isoLift : IsoLift) (iso : Mor₂Iso) : Mor₂

  The expression for `Iso.inv`.

- id (e : Lean.Expr) (isoLift : IsoLift) (f : Mor₁) : Mor₂

  The expression for the identity `𝟙 f`.

- comp (e : Lean.Expr) (isoLift? : Option IsoLift) (f g h : Mor₁) (η θ : Mor₂) : Mor₂

  The expression for the composition `η ≫ θ`.

- whiskerLeft (e : Lean.Expr) (isoLift? : Option IsoLift) (f g h : Mor₁) (η : Mor₂) : Mor₂

  The expression for the left whiskering `f ◁ η` with `η : g ⟶ h`.

- whiskerRight (e : Lean.Expr) (isoLift? : Option IsoLift) (f g : Mor₁) (η : Mor₂) (h : Mor₁) : Mor₂

  The expression for the right whiskering `η ▷ h` with `η : f ⟶ g`.

- horizontalComp (e : Lean.Expr) (isoLift? : Option IsoLift) (f₁ g₁ f₂ g₂ : Mor₁) (η θ : Mor₂) : Mor₂

  The expression for the horizontal composition `η ◫ θ` with `η : f₁ ⟶ g₁` and `θ : f₂ ⟶ g₂`.

- coherenceComp (e : Lean.Expr) (isoLift? : Option IsoLift) (f g h i : Mor₁) (α : CoherenceHom) (η θ : Mor₂) : Mor₂

  The expression for the coherence composition `η ⊗≫ θ := η ≫ α ≫ θ` with `η : f ⟶ g` and `θ : h ⟶ i`.

- of (η : Atom) : Mor₂

  The expression for an atomic non-structural 2-morphism.

Instances For

source
def Mathlib.Tactic.BicategoryLike.instInhabitedMor₂.default :
Mor₂
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedMor₂.default = Mathlib.Tactic.BicategoryLike.Mor₂.of default

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedMor₂ :
Inhabited Mor₂
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedMor₂ = { default := Mathlib.Tactic.BicategoryLike.instInhabitedMor₂.default }

source
class Mathlib.Tactic.BicategoryLike.MkMor₂ (m : Type → Type) :
Type

A monad equipped with the ability to construct `Mor₂` terms.

- ofExpr (e : Lean.Expr) : m Mor₂

  Construct a `Mor₂` term from a lean expression.

Instances

source
def Mathlib.Tactic.BicategoryLike.Mor₂.e :
Mor₂ → Lean.Expr

The underlying lean expression of a 2-morphism.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₂.isoHom e isoLift iso).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂.isoInv e isoLift iso).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂.id e isoLift f).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂.comp e isoLift? f g h η θ).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e isoLift? f g h η).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight e isoLift? f g η h).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e isoLift? f₁ g₁ f₂ g₂ η θ).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp e isoLift? f g h i α η θ).e = e
- (Mathlib.Tactic.BicategoryLike.Mor₂.of η).e = η.e

Instances For

source
def Mathlib.Tactic.BicategoryLike.Mor₂.isoLift? :
Mor₂ → Option IsoLift

`η.isoLift?` is a pair of a 2-isomorphism `η'` and a proof that `η'.hom = η`. If no such `η'` is found, returns `none`. This function does not seek `IsIso` instance.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₂.isoHom e isoLift iso).isoLift? = some isoLift
- (Mathlib.Tactic.BicategoryLike.Mor₂.isoInv e isoLift iso).isoLift? = some isoLift
- (Mathlib.Tactic.BicategoryLike.Mor₂.id e isoLift f).isoLift? = some isoLift
- (Mathlib.Tactic.BicategoryLike.Mor₂.comp e isoLift? f g h η θ).isoLift? = isoLift?
- (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e isoLift? f g h η).isoLift? = isoLift?
- (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight e isoLift? f g η h).isoLift? = isoLift?
- (Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e isoLift? f₁ g₁ f₂ g₂ η θ).isoLift? = isoLift?
- (Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp e isoLift? f g h i α η θ).isoLift? = isoLift?
- (Mathlib.Tactic.BicategoryLike.Mor₂.of η).isoLift? = none

Instances For

source
def Mathlib.Tactic.BicategoryLike.Mor₂.srcM {m : Type → Type} [Monad m] [MonadMor₁ m] :
Mor₂ → m Mor₁

The domain of a 2-morphism.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₂.isoHom e isoLift iso).srcM = iso.srcM
- (Mathlib.Tactic.BicategoryLike.Mor₂.isoInv e isoLift iso).srcM = iso.tgtM
- (Mathlib.Tactic.BicategoryLike.Mor₂.id e isoLift f).srcM = pure f
- (Mathlib.Tactic.BicategoryLike.Mor₂.comp e isoLift? f g h η θ).srcM = pure f
- (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e isoLift? f g h η).srcM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M f g
- (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight e isoLift? f g η h).srcM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M f h
- (Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e isoLift? f₁ g₁ f₂ g₂ η θ).srcM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M f₁ f₂
- (Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp e isoLift? f g h i α η θ).srcM = pure f
- (Mathlib.Tactic.BicategoryLike.Mor₂.of η).srcM = pure η.src

Instances For

source
def Mathlib.Tactic.BicategoryLike.Mor₂.tgtM {m : Type → Type} [Monad m] [MonadMor₁ m] :
Mor₂ → m Mor₁

The codomain of a 2-morphism.

Equations

- (Mathlib.Tactic.BicategoryLike.Mor₂.isoHom e isoLift iso).tgtM = iso.tgtM
- (Mathlib.Tactic.BicategoryLike.Mor₂.isoInv e isoLift iso).tgtM = iso.srcM
- (Mathlib.Tactic.BicategoryLike.Mor₂.id e isoLift f).tgtM = pure f
- (Mathlib.Tactic.BicategoryLike.Mor₂.comp e isoLift? f g h η θ).tgtM = pure h
- (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft e isoLift? f g h η).tgtM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M f h
- (Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight e isoLift? f g η h).tgtM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M g h
- (Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e isoLift? f₁ g₁ f₂ g₂ η θ).tgtM = Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M g₁ g₂
- (Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp e isoLift? f g h i α η θ).tgtM = pure i
- (Mathlib.Tactic.BicategoryLike.Mor₂.of η).tgtM = pure η.tgt

Instances For

source
class Mathlib.Tactic.BicategoryLike.MonadMor₂ (m : Type → Type) :
Type

A monad equipped with the ability to manipulate 2-morphisms.

- homM (η : Mor₂Iso) : m Mor₂

  The expression for `Iso.hom η`.

- atomHomM (η : AtomIso) : m Atom

  The expression for `Iso.hom η`.

- invM (η : Mor₂Iso) : m Mor₂

  The expression for `Iso.inv η`.

- atomInvM (η : AtomIso) : m Atom

  The expression for `Iso.inv η`.

- id₂M (f : Mor₁) : m Mor₂

  The expression for the identity `𝟙 f`.

- comp₂M (η θ : Mor₂) : m Mor₂

  The expression for the composition `η ≫ θ`.

- whiskerLeftM (f : Mor₁) (η : Mor₂) : m Mor₂

  The expression for the left whiskering `f ◁ η`.

- whiskerRightM (η : Mor₂) (h : Mor₁) : m Mor₂

  The expression for the right whiskering `η ▷ h`.

- horizontalCompM (η θ : Mor₂) : m Mor₂

  The expression for the horizontal composition `η ◫ θ`.

- coherenceCompM (α : CoherenceHom) (η θ : Mor₂) : m Mor₂

  The expression for the coherence composition `η ⊗≫ θ := η ≫ α ≫ θ`.

Instances

source
inductive Mathlib.Tactic.BicategoryLike.NormalizedHom :
Type

Type of normalized 1-morphisms `((... ≫ h) ≫ g) ≫ f`.

- nil (e : Mor₁) (a : Obj) : NormalizedHom

  The identity 1-morphism `𝟙 a`.

- cons (e : Mor₁) : NormalizedHom → Atom₁ → NormalizedHom

  The `cons` composes an atomic 1-morphism at the end of a normalized 1-morphism.

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedNormalizedHom :
Inhabited NormalizedHom
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedNormalizedHom = { default := Mathlib.Tactic.BicategoryLike.instInhabitedNormalizedHom.default }

source
def Mathlib.Tactic.BicategoryLike.instInhabitedNormalizedHom.default :
NormalizedHom
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedNormalizedHom.default = Mathlib.Tactic.BicategoryLike.NormalizedHom.nil default default

Instances For

source
def Mathlib.Tactic.BicategoryLike.NormalizedHom.e :
NormalizedHom → Mor₁

The underlying expression of a normalized 1-morphism.

Equations

- (Mathlib.Tactic.BicategoryLike.NormalizedHom.nil e a).e = e
- (Mathlib.Tactic.BicategoryLike.NormalizedHom.cons e a a_1).e = e

Instances For

source
def Mathlib.Tactic.BicategoryLike.NormalizedHom.src :
NormalizedHom → Obj

The domain of a normalized 1-morphism.

Equations

- (Mathlib.Tactic.BicategoryLike.NormalizedHom.nil e a).src = a
- (Mathlib.Tactic.BicategoryLike.NormalizedHom.cons e a a_1).src = a.src

Instances For

source
def Mathlib.Tactic.BicategoryLike.NormalizedHom.tgt :
NormalizedHom → Obj

The codomain of a normalized 1-morphism.

Equations

- (Mathlib.Tactic.BicategoryLike.NormalizedHom.nil e a).tgt = a
- (Mathlib.Tactic.BicategoryLike.NormalizedHom.cons e a a_1).tgt = a_1.tgt

Instances For

source
def Mathlib.Tactic.BicategoryLike.normalizedHom.nilM {m : Type → Type} [Monad m] [MonadMor₁ m] (a : Obj) :
m NormalizedHom

Construct the `NormalizedHom.nil` term in `m`.

Equations

- Mathlib.Tactic.BicategoryLike.normalizedHom.nilM a = do let __do_lift ← Mathlib.Tactic.BicategoryLike.MonadMor₁.id₁M a pure (Mathlib.Tactic.BicategoryLike.NormalizedHom.nil __do_lift a)

Instances For

source
def Mathlib.Tactic.BicategoryLike.NormalizedHom.consM {m : Type → Type} [Monad m] [MonadMor₁ m] (p : NormalizedHom) (f : Atom₁) :
m NormalizedHom

Construct a `NormalizedHom.cons` term in `m`.

Equations

- p.consM f = do let __do_lift ← Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M p.e (Mathlib.Tactic.BicategoryLike.Mor₁.of f) pure (Mathlib.Tactic.BicategoryLike.NormalizedHom.cons __do_lift p f)

Instances For

source
class Mathlib.Tactic.BicategoryLike.Context (ρ : Type) :
Type

`Context ρ` provides the context for manipulating 2-morphisms in a monoidal category or bicategory. In particular, we will store `MonoidalCategory` or `Bicategory` instance in a context, and use this through a reader monad when we construct the lean expressions for 2-morphisms.

- mkContext? : Lean.Expr → Lean.MetaM (Option ρ)

  Construct a context from a lean expression for a 2-morphism.

Instances

source
def Mathlib.Tactic.BicategoryLike.mkContext {ρ : Type} [Context ρ] (e : Lean.Expr) :
Lean.MetaM ρ

Construct a context from a lean expression for a 2-morphism.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
structure Mathlib.Tactic.BicategoryLike.State :
Type

The state for the `CoherenceM ρ` monad.

- cache : Lean.PersistentExprMap Mor₁

  The cache for evaluating lean expressions of 1-morphisms into `Mor₁` terms.

Instances For

source
@[reducible, inline]
abbrev Mathlib.Tactic.BicategoryLike.CoherenceM (ρ α : Type) :
Type

The monad for manipulating 2-morphisms in a monoidal category or bicategory.

Equations

- Mathlib.Tactic.BicategoryLike.CoherenceM ρ = ReaderT ρ (StateT Mathlib.Tactic.BicategoryLike.State Lean.MetaM)

Instances For

source
def Mathlib.Tactic.BicategoryLike.CoherenceM.run {α ρ : Type} (x : CoherenceM ρ α) (ctx : ρ) (s : State := { }) :
Lean.MetaM α

Run the `CoherenceM ρ` monad.

Equations

- x.run ctx s = Prod.fst <$> ReaderT.run x ctx s

Instances For