Normalize

📁 Source: Mathlib/Tactic/CategoryTheory/Coherence/Normalize.lean

Statistics

Metric	Count
Definitions `expr`, `proof`, `instInhabitedResult`, `default`, `HorizontalComp`, `e`, `srcM`, `tgtM`, `MkEval`, `mkEvalComp`, `mkEvalHorizontalComp`, `mkEvalMonoidalComp`, `mkEvalOf`, `mkEvalWhiskerLeft`, `mkEvalWhiskerRight`, `toMkEvalComp`, `toMkEvalHorizontalComp`, `toMkEvalWhiskerLeft`, `toMkEvalWhiskerRight`, `MkEvalComp`, `mkEvalCompCons`, `mkEvalCompNilCons`, `mkEvalCompNilNil`, `MkEvalHorizontalComp`, `mkEvalHorizontalCompAux'OfWhisker`, `mkEvalHorizontalCompAux'Whisker`, `mkEvalHorizontalCompAuxCons`, `mkEvalHorizontalCompAuxOf`, `mkEvalHorizontalCompConsCons`, `mkEvalHorizontalCompConsNil`, `mkEvalHorizontalCompNilCons`, `mkEvalHorizontalCompNilNil`, `MkEvalWhiskerLeft`, `mkEvalWhiskerLeftComp`, `mkEvalWhiskerLeftId`, `mkEvalWhiskerLeftNil`, `mkEvalWhiskerLeftOfCons`, `MkEvalWhiskerRight`, `mkEvalWhiskerRightAuxCons`, `mkEvalWhiskerRightAuxOf`, `mkEvalWhiskerRightComp`, `mkEvalWhiskerRightConsOfOf`, `mkEvalWhiskerRightConsWhisker`, `mkEvalWhiskerRightId`, `mkEvalWhiskerRightNil`, `MonadHorizontalComp`, `hConsM`, `toMonadWhiskerRight`, `MonadNormalExpr`, `consM`, `nilM`, `toMonadWhiskerLeft`, `MonadWhiskerLeft`, `toMonadHorizontalComp`, `whiskerLeftM`, `MonadWhiskerRight`, `whiskerRightM`, `isStructural`, `NormalExpr`, `associatorInvM`, `associatorM`, `e`, `idM`, `leftUnitorInvM`, `leftUnitorM`, `ofAtomM`, `ofM`, `rightUnitorInvM`, `rightUnitorM`, `srcM`, `tgtM`, `toList`, `Structural`, `WhiskerLeft`, `e`, `srcM`, `tgtM`, `WhiskerRight`, `e`, `srcM`, `tgtM`, `eval`, `evalComp`, `evalCompNil`, `evalHorizontalComp`, `evalHorizontalCompAux`, `evalHorizontalCompAux'`, `evalWhiskerLeft`, `evalWhiskerRight`, `evalWhiskerRightAux`, `instInhabitedHorizontalComp`, `default`, `instInhabitedNormalExpr`, `default`, `instInhabitedWhiskerLeft`, `default`, `instInhabitedWhiskerRight`, `default`, `traceProof`	99
Theorems	0
Total	99

Mathlib.Tactic.BicategoryLike

Definitions

Name	Category	Theorems
`HorizontalComp` 📖	CompData	—
`MkEval` 📖	CompData	—
`MkEvalComp` 📖	CompData	—
`MkEvalHorizontalComp` 📖	CompData	—
`MkEvalWhiskerLeft` 📖	CompData	—
`MkEvalWhiskerRight` 📖	CompData	—
`MonadHorizontalComp` 📖	CompData	—
`MonadNormalExpr` 📖	CompData	—
`MonadWhiskerLeft` 📖	CompData	—
`MonadWhiskerRight` 📖	CompData	—
`NormalExpr` 📖	CompData	—
`Structural` 📖	CompOp	—
`WhiskerLeft` 📖	CompData	—
`WhiskerRight` 📖	CompData	—
`eval` 📖	CompOp	—
`evalComp` 📖	CompOp	—
`evalCompNil` 📖	CompOp	—
`evalHorizontalComp` 📖	CompOp	—
`evalHorizontalCompAux` 📖	CompOp	—
`evalHorizontalCompAux'` 📖	CompOp	—
`evalWhiskerLeft` 📖	CompOp	—
`evalWhiskerRight` 📖	CompOp	—
`evalWhiskerRightAux` 📖	CompOp	—
`instInhabitedHorizontalComp` 📖	CompOp	—
`instInhabitedNormalExpr` 📖	CompOp	—
`instInhabitedWhiskerLeft` 📖	CompOp	—
`instInhabitedWhiskerRight` 📖	CompOp	—
`traceProof` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.Eval

Definitions

Name	Category	Theorems
`instInhabitedResult` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.Eval.Result

Definitions

Name	Category	Theorems
`expr` 📖	CompOp	—
`proof` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.Eval.instInhabitedResult

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.HorizontalComp

Definitions

Name	Category	Theorems
`e` 📖	CompOp	—
`srcM` 📖	CompOp	—
`tgtM` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MkEval

Definitions

Name	Category	Theorems
`mkEvalComp` 📖	CompOp	—
`mkEvalHorizontalComp` 📖	CompOp	—
`mkEvalMonoidalComp` 📖	CompOp	—
`mkEvalOf` 📖	CompOp	—
`mkEvalWhiskerLeft` 📖	CompOp	—
`mkEvalWhiskerRight` 📖	CompOp	—
`toMkEvalComp` 📖	CompOp	—
`toMkEvalHorizontalComp` 📖	CompOp	—
`toMkEvalWhiskerLeft` 📖	CompOp	—
`toMkEvalWhiskerRight` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MkEvalComp

Definitions

Name	Category	Theorems
`mkEvalCompCons` 📖	CompOp	—
`mkEvalCompNilCons` 📖	CompOp	—
`mkEvalCompNilNil` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp

Definitions

Name	Category	Theorems
`mkEvalHorizontalCompAux'OfWhisker` 📖	CompOp	—
`mkEvalHorizontalCompAux'Whisker` 📖	CompOp	—
`mkEvalHorizontalCompAuxCons` 📖	CompOp	—
`mkEvalHorizontalCompAuxOf` 📖	CompOp	—
`mkEvalHorizontalCompConsCons` 📖	CompOp	—
`mkEvalHorizontalCompConsNil` 📖	CompOp	—
`mkEvalHorizontalCompNilCons` 📖	CompOp	—
`mkEvalHorizontalCompNilNil` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft

Definitions

Name	Category	Theorems
`mkEvalWhiskerLeftComp` 📖	CompOp	—
`mkEvalWhiskerLeftId` 📖	CompOp	—
`mkEvalWhiskerLeftNil` 📖	CompOp	—
`mkEvalWhiskerLeftOfCons` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight

Definitions

Name	Category	Theorems
`mkEvalWhiskerRightAuxCons` 📖	CompOp	—
`mkEvalWhiskerRightAuxOf` 📖	CompOp	—
`mkEvalWhiskerRightComp` 📖	CompOp	—
`mkEvalWhiskerRightConsOfOf` 📖	CompOp	—
`mkEvalWhiskerRightConsWhisker` 📖	CompOp	—
`mkEvalWhiskerRightId` 📖	CompOp	—
`mkEvalWhiskerRightNil` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MonadHorizontalComp

Definitions

Name	Category	Theorems
`hConsM` 📖	CompOp	—
`toMonadWhiskerRight` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MonadNormalExpr

Definitions

Name	Category	Theorems
`consM` 📖	CompOp	—
`nilM` 📖	CompOp	—
`toMonadWhiskerLeft` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft

Definitions

Name	Category	Theorems
`toMonadHorizontalComp` 📖	CompOp	—
`whiskerLeftM` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.MonadWhiskerRight

Definitions

Name	Category	Theorems
`whiskerRightM` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.Mor₂Iso

Definitions

Name	Category	Theorems
`isStructural` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.NormalExpr

Definitions

Name	Category	Theorems
`associatorInvM` 📖	CompOp	—
`associatorM` 📖	CompOp	—
`e` 📖	CompOp	—
`idM` 📖	CompOp	—
`leftUnitorInvM` 📖	CompOp	—
`leftUnitorM` 📖	CompOp	—
`ofAtomM` 📖	CompOp	—
`ofM` 📖	CompOp	—
`rightUnitorInvM` 📖	CompOp	—
`rightUnitorM` 📖	CompOp	—
`srcM` 📖	CompOp	—
`tgtM` 📖	CompOp	—
`toList` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.WhiskerLeft

Definitions

Name	Category	Theorems
`e` 📖	CompOp	—
`srcM` 📖	CompOp	—
`tgtM` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.WhiskerRight

Definitions

Name	Category	Theorems
`e` 📖	CompOp	—
`srcM` 📖	CompOp	—
`tgtM` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index