# The `to_app` attribute #

Adding `@[to_app]` to a lemma named `F` of shape `∀ .., η = θ`, where `η θ : f ⟶ g` are 2-morphisms in some bicategory, create a new lemma named `F_app`. This lemma is obtained by first specializing the bicategory in which the equality is taking place to `Cat`, then applying `NatTrans.congr_app` to obtain a proof of `∀ ... (X : Cat), η.app X = θ.app X`, and finally simplifying the conclusion using some basic lemmas in the bicategory `Cat`: `Cat.whiskerLeft_app`, `Cat.whiskerRight_app`, `Cat.id_app`, `Cat.comp_app` and `Cat.eqToHom_app`

So, for example, if the conclusion of `F` is `f ◁ η = θ` then the conclusion of `F_app` will be `η.app (f.obj X) = θ.app X`.

This is useful for automatically generating lemmas that can be applied to expressions of 1-morphisms in `Cat` which contain components of 2-morphisms.

There is also a term elaborator `to_app_of% t` for use within proofs.

source
def CategoryTheory.catAppSimp (e : Lean.Expr) :
Lean.MetaM Lean.Meta.Simp.Result

Simplify an expression in `Cat` using basic properties of `NatTrans.app`.

Equations

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

Instances For

source
def CategoryTheory.toCatExpr (e : Lean.Expr) :
Lean.MetaM Lean.Expr

Given a term of type `∀ ..., η = θ`, where `η θ : f ⟶ g` are 2-morphisms in some bicategory `B`, which is bound by the `∀` binder, get the corresponding equation in the bicategory `Cat`.

It is important here that the levels in the term are level metavariables, as otherwise these will not be reassignable to the corresponding levels of `Cat`.

Equations

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

Instances For

source
@[irreducible]
def CategoryTheory.toCatExpr.apprec (args : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) (B inst : Lean.Expr) (i : ℕ) (e : Lean.Expr) :
Lean.MetaM Lean.Expr

Recursive function which applies `mkLambdaFVars` stepwise (so that each step can have different binderinfos)

Equations

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

Instances For

source
def CategoryTheory.toAppExpr (e : Lean.Expr) :
Lean.MetaM Lean.Expr

Given morphisms `f g : C ⟶ D` in the bicategory `Cat`, and an equation `η = θ` between 2-morphisms (possibly after a `∀` binder), produce the equation `∀ (X : C), f.app X = g.app X`, and simplify it using basic lemmas about `NatTrans.app`.

Equations

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

Instances For

source
def CategoryTheory.to_app :
Lean.ParserDescr

Adding `@[to_app]` to a lemma named `F` of shape `∀ .., η = θ`, where `η θ : f ⟶ g` are 2-morphisms in some bicategory, create a new lemma named `F_app`. This lemma is obtained by first specializing the bicategory in which the equality is taking place to `Cat`, then applying `NatTrans.congr_app` to obtain a proof of `∀ ... (X : Cat), η.app X = θ.app X`, and finally simplifying the conclusion using some basic lemmas in the bicategory `Cat`: `Cat.whiskerLeft_app`, `Cat.whiskerRight_app`, `Cat.id_app`, `Cat.comp_app` and `Cat.eqToHom_app`

So, for example, if the conclusion of `F` is `f ◁ η = θ` then the conclusion of `F_app` will be `η.app (f.obj X) = θ.app X`.

This is useful for automatically generating lemmas that can be applied to expressions of 1-morphisms in `Cat` which contain components of 2-morphisms.

Note that if you want both the lemma and the new lemma to be `simp` lemmas, you should tag the lemma `@[to_app (attr := simp)]`. The variant `@[simp, to_app]` on a lemma `F` will tag `F` with `@[simp]`, but not `F_app` (this is sometimes useful).

Equations

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

Instances For

source
def CategoryTheory.«termTo_app_of%_» :
Lean.ParserDescr

Given an equation `t` of the form `η = θ` between 2-morphisms `f ⟶ g` with `f g : C ⟶ D` in the bicategory `Cat` (possibly after a `∀` binder), `to_app_of% t` produces the equation `∀ (X : C), η.app X = θ.app X` (where `X` is an object in the domain of `f` and `g`), and simplifies it suitably using basic lemmas about `NatTrans.app`.

Equations

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

Instances For