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.

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

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

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.

@[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)

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.

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).

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.