Mate

📁 Source: Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean

Statistics

Metric	Count
Definitions homEquiv₁, homEquiv₂, conjugateEquiv, conjugateIsoEquiv, vcomp, comp, hcomp, vcomp, vcomp, mateEquiv, vcomp, comp, hcomp, vcomp, vcomp	15
Theorems homEquiv₁_apply, homEquiv₁_symm_apply, homEquiv₂_apply, homEquiv₂_symm_apply, conjugateEquiv_adjunction_id, conjugateEquiv_adjunction_id_symm, conjugateEquiv_apply, conjugateEquiv_apply', conjugateEquiv_associator_hom, conjugateEquiv_comm, conjugateEquiv_comp, conjugateEquiv_comp_id_right_apply, conjugateEquiv_id, conjugateEquiv_id_comp_right_apply, conjugateEquiv_iso, conjugateEquiv_mateEquiv_vcomp, conjugateEquiv_of_iso, conjugateEquiv_symm_apply, conjugateEquiv_symm_apply', conjugateEquiv_symm_comm, conjugateEquiv_symm_comp, conjugateEquiv_symm_id, conjugateEquiv_symm_iso, conjugateEquiv_symm_of_iso, conjugateEquiv_whiskerLeft, conjugateEquiv_whiskerRight, conjugateIsoEquiv_apply_hom, conjugateIsoEquiv_apply_inv, conjugateIsoEquiv_symm_apply_hom, conjugateIsoEquiv_symm_apply_inv, iterated_mateEquiv_conjugateEquiv, iterated_mateEquiv_conjugateEquiv_symm, comp_hvcomp, comp_vhcomp, mateEquiv_apply, mateEquiv_apply', mateEquiv_comp_id_right, mateEquiv_conjugateEquiv_vcomp, mateEquiv_eq_iff, mateEquiv_hcomp, mateEquiv_id_comp_right, mateEquiv_leftUnitor_hom_rightUnitor_inv, mateEquiv_square, mateEquiv_symm_apply, mateEquiv_symm_apply', mateEquiv_vcomp, comp_hvcomp, comp_vhcomp	48
Total	63

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
conjugateEquiv 📖	CompOp	30 math math: iterated_mateEquiv_conjugateEquiv, conjugateEquiv_whiskerRight, conjugateEquiv_adjunction_id_symm, conjugateEquiv_symm_id, conjugateEquiv_apply, Adj.Hom₂.conjugateEquiv_symm_τr, conjugateEquiv_id_comp_right_apply, conjugateEquiv_comp_id_right_apply, conjugateIsoEquiv_apply_inv, conjugateEquiv_symm_comm, conjugateEquiv_symm_comp, conjugateIsoEquiv_apply_hom, conjugateIsoEquiv_symm_apply_hom, iterated_mateEquiv_conjugateEquiv_symm, conjugateEquiv_apply', mateEquiv_conjugateEquiv_vcomp, conjugateEquiv_adjunction_id, conjugateEquiv_associator_hom, Adj.Hom₂.conjugateEquiv_τl, conjugateEquiv_id, conjugateEquiv_symm_iso, conjugateEquiv_mateEquiv_vcomp, toNatTrans_conjugateEquiv, conjugateEquiv_symm_apply', conjugateEquiv_iso, conjugateEquiv_comm, conjugateEquiv_whiskerLeft, conjugateEquiv_symm_apply, conjugateIsoEquiv_symm_apply_inv, conjugateEquiv_comp
conjugateIsoEquiv 📖	CompOp	4 math math: conjugateIsoEquiv_apply_inv, conjugateIsoEquiv_apply_hom, conjugateIsoEquiv_symm_apply_hom, conjugateIsoEquiv_symm_apply_inv
mateEquiv 📖	CompOp	18 math math: iterated_mateEquiv_conjugateEquiv, mateEquiv_comp_id_right, mateEquiv_vcomp, conjugateEquiv_apply, mateEquiv_id_comp_right, mateEquiv_symm_apply', mateEquiv_symm_apply, mateEquiv_hcomp, mateEquiv_eq_iff, toNatTrans_mateEquiv, iterated_mateEquiv_conjugateEquiv_symm, mateEquiv_square, mateEquiv_conjugateEquiv_vcomp, mateEquiv_leftUnitor_hom_rightUnitor_inv, conjugateEquiv_mateEquiv_vcomp, mateEquiv_apply, conjugateEquiv_symm_apply, mateEquiv_apply'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjugateEquiv_adjunction_id 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.id EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv Adjunction.id CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.inv rightUnitor whiskerLeft Adjunction.counit	—	conjugateEquiv_apply mateEquiv_apply' Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_leftUnitor
conjugateEquiv_adjunction_id_symm 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.id EquivLike.toFunLike Equiv.instEquivLike Equiv.symm conjugateEquiv Adjunction.id CategoryTheory.CategoryStruct.comp Adjunction.unit whiskerLeft CategoryTheory.Iso.hom rightUnitor	—	conjugateEquiv_symm_apply mateEquiv_symm_apply' Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_whiskerLeft
conjugateEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv rightUnitor mateEquiv CategoryTheory.Iso.hom leftUnitor	—	—
conjugateEquiv_apply' 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv rightUnitor whiskerLeft Adjunction.unit whiskerRight associator Adjunction.counit CategoryTheory.Iso.hom leftUnitor	—	conjugateEquiv_apply mateEquiv_apply' Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerLeft_id Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_associator
conjugateEquiv_associator_hom 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv Adjunction.comp CategoryTheory.Iso.hom associator	—	CategoryTheory.cancel_epi CategoryTheory.IsIso.epi_of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.cancel_mono CategoryTheory.IsIso.mono_of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id unitors_inv_equal whiskerRight_id whiskerLeft_comp whiskerLeft_rightUnitor comp_whiskerLeft CategoryTheory.Iso.inv_hom_id_assoc whiskerLeft_inv_hom_assoc whiskerRight_comp id_whiskerLeft unitors_equal comp_whiskerRight leftUnitor_whiskerRight Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_rightUnitor
conjugateEquiv_comm 📖	mathematical	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.id	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv	—	conjugateEquiv_comp conjugateEquiv_id
conjugateEquiv_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.evalWhiskerLeft_id Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_associator mateEquiv_vcomp mateEquiv_apply' Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.Bicategory.naturality_whiskerRight
conjugateEquiv_comp_id_right_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv Adjunction.comp Adjunction.id CategoryTheory.Iso.hom rightUnitor CategoryTheory.Iso.inv leftUnitor	—	CategoryTheory.Category.assoc mateEquiv_comp_id_right id_whiskerLeft CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id EquivLike.toEmbeddingLike Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_id
conjugateEquiv_id 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv CategoryTheory.CategoryStruct.id	—	conjugateEquiv_apply mateEquiv_apply' Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerLeft_id Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_associator Adjunction.right_triangle
conjugateEquiv_id_comp_right_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv Adjunction.comp Adjunction.id CategoryTheory.Iso.hom leftUnitor CategoryTheory.Iso.inv rightUnitor	—	CategoryTheory.Category.assoc mateEquiv_id_comp_right id_whiskerLeft CategoryTheory.Iso.inv_hom_id_assoc Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_leftUnitor
conjugateEquiv_iso 📖	mathematical	—	CategoryTheory.IsIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory DFunLike.coe Equiv CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv	—	conjugateEquiv_comm CategoryTheory.IsIso.inv_hom_id CategoryTheory.IsIso.hom_inv_id
conjugateEquiv_mateEquiv_vcomp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike mateEquiv leftAdjointConjugateSquare.vcomp rightAdjointConjugateSquare.vcomp conjugateEquiv	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.evalWhiskerLeft_id Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_associator mateEquiv_vcomp mateEquiv_apply' Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.Bicategory.evalWhiskerRight_id
conjugateEquiv_of_iso 📖	mathematical	—	CategoryTheory.IsIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory	—	conjugateEquiv_symm_iso Equiv.symm_apply_apply
conjugateEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory EquivLike.toFunLike Equiv.instEquivLike Equiv.symm conjugateEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv leftUnitor mateEquiv CategoryTheory.Iso.hom rightUnitor	—	—
conjugateEquiv_symm_apply' 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory EquivLike.toFunLike Equiv.instEquivLike Equiv.symm conjugateEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv leftUnitor whiskerRight Adjunction.unit CategoryTheory.Iso.hom associator whiskerLeft Adjunction.counit rightUnitor	—	conjugateEquiv_symm_apply mateEquiv_symm_apply' Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalWhiskerLeft_id Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_whiskerLeft
conjugateEquiv_symm_comm 📖	mathematical	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.id	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm conjugateEquiv	—	conjugateEquiv_symm_comp conjugateEquiv_symm_id
conjugateEquiv_symm_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm conjugateEquiv	—	Equiv.eq_symm_apply conjugateEquiv_comp Equiv.apply_symm_apply
conjugateEquiv_symm_id 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory EquivLike.toFunLike Equiv.instEquivLike Equiv.symm conjugateEquiv CategoryTheory.CategoryStruct.id	—	Equiv.symm_apply_eq conjugateEquiv_id
conjugateEquiv_symm_iso 📖	mathematical	—	CategoryTheory.IsIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory DFunLike.coe Equiv CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm conjugateEquiv	—	conjugateEquiv_symm_comm CategoryTheory.IsIso.inv_hom_id CategoryTheory.IsIso.hom_inv_id
conjugateEquiv_symm_of_iso 📖	mathematical	—	CategoryTheory.IsIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory	—	conjugateEquiv_iso Equiv.apply_symm_apply
conjugateEquiv_whiskerLeft 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv Adjunction.comp whiskerLeft whiskerRight	—	mateEquiv_hcomp comp_whiskerRight leftUnitor_whiskerRight CategoryTheory.Category.assoc whiskerLeft_comp whiskerLeft_rightUnitor_inv CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id triangle_assoc inv_hom_whiskerRight_assoc CategoryTheory.Iso.inv_hom_id_assoc mateEquiv_leftUnitor_hom_rightUnitor_inv whiskerLeft_rightUnitor triangle_assoc_comp_left_inv_assoc CategoryTheory.Iso.hom_inv_id_assoc
conjugateEquiv_whiskerRight 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike conjugateEquiv Adjunction.comp whiskerRight whiskerLeft	—	mateEquiv_hcomp comp_whiskerRight leftUnitor_whiskerRight CategoryTheory.Category.assoc whiskerLeft_comp whiskerLeft_rightUnitor_inv CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id triangle_assoc inv_hom_whiskerRight_assoc CategoryTheory.Iso.inv_hom_id_assoc mateEquiv_leftUnitor_hom_rightUnitor_inv leftUnitor_inv_whiskerRight CategoryTheory.Iso.inv_hom_id triangle_assoc_comp_right_assoc
conjugateIsoEquiv_apply_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory DFunLike.coe Equiv CategoryTheory.Iso EquivLike.toFunLike Equiv.instEquivLike conjugateIsoEquiv CategoryTheory.Category.toCategoryStruct conjugateEquiv	—	—
conjugateIsoEquiv_apply_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory DFunLike.coe Equiv CategoryTheory.Iso EquivLike.toFunLike Equiv.instEquivLike conjugateIsoEquiv CategoryTheory.Category.toCategoryStruct conjugateEquiv	—	—
conjugateIsoEquiv_symm_apply_hom 📖	mathematical	—	CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory DFunLike.coe Equiv CategoryTheory.Iso EquivLike.toFunLike Equiv.instEquivLike Equiv.symm conjugateIsoEquiv CategoryTheory.Category.toCategoryStruct conjugateEquiv	—	—
conjugateIsoEquiv_symm_apply_inv 📖	mathematical	—	CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct homCategory DFunLike.coe Equiv CategoryTheory.Iso EquivLike.toFunLike Equiv.instEquivLike Equiv.symm conjugateIsoEquiv CategoryTheory.Category.toCategoryStruct conjugateEquiv	—	—
iterated_mateEquiv_conjugateEquiv 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike mateEquiv conjugateEquiv Adjunction.comp	—	mateEquiv_apply' Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.evalWhiskerLeft_id Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_whiskerRight
iterated_mateEquiv_conjugateEquiv_symm 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike Equiv.symm mateEquiv conjugateEquiv Adjunction.comp	—	Equiv.eq_symm_apply iterated_mateEquiv_conjugateEquiv Equiv.apply_symm_apply
mateEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike mateEquiv Adjunction.homEquiv₁ Adjunction.homEquiv₂ CategoryTheory.Iso.hom associator	—	CategoryTheory.Category.id_comp
mateEquiv_apply' 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike mateEquiv CategoryTheory.bicategoricalComp CategoryTheory.CategoryStruct.id CategoryTheory.BicategoricalCoherence.whiskerLeft CategoryTheory.BicategoricalCoherence.right' CategoryTheory.BicategoricalCoherence.refl CategoryTheory.BicategoricalCoherence.assoc' CategoryTheory.BicategoricalCoherence.whiskerRight whiskerLeft Adjunction.unit CategoryTheory.BicategoricalCoherence.assoc whiskerRight CategoryTheory.BicategoricalCoherence.left Adjunction.counit	—	mateEquiv_apply Adjunction.homEquiv₂_apply Adjunction.homEquiv₁_apply Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_leftUnitor
mateEquiv_comp_id_right 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id EquivLike.toFunLike Equiv.instEquivLike mateEquiv Adjunction.comp Adjunction.id CategoryTheory.Iso.inv rightUnitor CategoryTheory.Iso.hom associator whiskerLeft leftUnitor	—	mateEquiv_apply Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_associator
mateEquiv_conjugateEquiv_vcomp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike mateEquiv leftAdjointSquareConjugate.vcomp rightAdjointSquareConjugate.vcomp conjugateEquiv	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_leftUnitor mateEquiv_vcomp mateEquiv_apply' Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp Mathlib.Tactic.Bicategory.evalWhiskerLeft_id Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.Bicategory.naturality_whiskerRight
mateEquiv_eq_iff 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike mateEquiv Equiv.symm Adjunction.homEquiv₁ Adjunction.homEquiv₂ CategoryTheory.Iso.hom associator	—	Equiv.injective mateEquiv_apply Equiv.symm_apply_apply
mateEquiv_hcomp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike mateEquiv Adjunction.comp leftAdjointSquare.hcomp rightAdjointSquare.hcomp	—	mateEquiv_apply' Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_whiskerRight whisker_exchange Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.Bicategory.evalWhiskerLeft_id
mateEquiv_id_comp_right 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id EquivLike.toFunLike Equiv.instEquivLike mateEquiv Adjunction.comp Adjunction.id whiskerLeft CategoryTheory.Iso.inv leftUnitor rightUnitor CategoryTheory.Iso.hom associator	—	mateEquiv_apply Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_id Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_whiskerRight
mateEquiv_leftUnitor_hom_rightUnitor_inv 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id EquivLike.toFunLike Equiv.instEquivLike mateEquiv CategoryTheory.Iso.hom leftUnitor CategoryTheory.Iso.inv rightUnitor	—	CategoryTheory.cancel_mono CategoryTheory.IsIso.mono_of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id conjugateEquiv_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id_assoc
mateEquiv_square 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike mateEquiv Adjunction.comp leftAdjointSquare.comp rightAdjointSquare.comp	—	mateEquiv_vcomp mateEquiv_hcomp
mateEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike Equiv.symm mateEquiv Adjunction.homEquiv₂ Adjunction.homEquiv₁ CategoryTheory.Iso.inv associator	—	CategoryTheory.Category.id_comp
mateEquiv_symm_apply' 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike Equiv.symm mateEquiv CategoryTheory.bicategoricalComp CategoryTheory.CategoryStruct.id CategoryTheory.BicategoricalCoherence.whiskerRight CategoryTheory.BicategoricalCoherence.left' CategoryTheory.BicategoricalCoherence.refl CategoryTheory.BicategoricalCoherence.assoc CategoryTheory.BicategoricalCoherence.whiskerLeft CategoryTheory.BicategoricalCoherence.assoc' whiskerRight Adjunction.unit whiskerLeft CategoryTheory.BicategoricalCoherence.right Adjunction.counit	—	mateEquiv_symm_apply Adjunction.homEquiv₂_symm_apply Adjunction.homEquiv₁_symm_apply Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_leftUnitor Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_rightUnitor
mateEquiv_vcomp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver toCategoryStruct CategoryTheory.Category.toCategoryStruct homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike mateEquiv leftAdjointSquare.vcomp rightAdjointSquare.vcomp	—	mateEquiv_apply' Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.Bicategory.evalWhiskerRight_id Mathlib.Tactic.Bicategory.evalWhiskerLeft_id Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_id Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_rightUnitor Mathlib.Tactic.Bicategory.naturality_leftUnitor whisker_exchange Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp Adjunction.left_triangle

CategoryTheory.Bicategory.Adjunction

Definitions

Name	Category	Theorems
homEquiv₁ 📖	CompOp	5 math math: homEquiv₁_apply, CategoryTheory.Bicategory.mateEquiv_symm_apply, CategoryTheory.Bicategory.mateEquiv_eq_iff, CategoryTheory.Bicategory.mateEquiv_apply, homEquiv₁_symm_apply
homEquiv₂ 📖	CompOp	5 math math: homEquiv₂_symm_apply, homEquiv₂_apply, CategoryTheory.Bicategory.mateEquiv_symm_apply, CategoryTheory.Bicategory.mateEquiv_eq_iff, CategoryTheory.Bicategory.mateEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homEquiv₁_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike homEquiv₁ CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.Bicategory.associator CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.whiskerRight counit CategoryTheory.Iso.hom CategoryTheory.Bicategory.leftUnitor	—	—
homEquiv₁_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv₁ CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv CategoryTheory.Bicategory.leftUnitor CategoryTheory.Bicategory.whiskerRight unit CategoryTheory.Iso.hom CategoryTheory.Bicategory.associator CategoryTheory.Bicategory.whiskerLeft	—	—
homEquiv₂_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike homEquiv₂ CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv CategoryTheory.Bicategory.rightUnitor CategoryTheory.Bicategory.whiskerLeft unit CategoryTheory.Bicategory.associator CategoryTheory.Bicategory.whiskerRight	—	—
homEquiv₂_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.CategoryStruct.comp EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv₂ CategoryTheory.Bicategory.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Bicategory.associator CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.whiskerLeft counit CategoryTheory.Bicategory.rightUnitor	—	—

CategoryTheory.Bicategory.leftAdjointConjugateSquare

Definitions

Name	Category	Theorems
vcomp 📖	CompOp	1 math math: CategoryTheory.Bicategory.conjugateEquiv_mateEquiv_vcomp

CategoryTheory.Bicategory.leftAdjointSquare

Definitions

Name	Category	Theorems
comp 📖	CompOp	3 math math: comp_hvcomp, CategoryTheory.Bicategory.mateEquiv_square, comp_vhcomp
hcomp 📖	CompOp	3 math math: comp_hvcomp, CategoryTheory.Bicategory.mateEquiv_hcomp, comp_vhcomp
vcomp 📖	CompOp	3 math math: comp_hvcomp, CategoryTheory.Bicategory.mateEquiv_vcomp, comp_vhcomp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hvcomp 📖	mathematical	—	comp hcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct vcomp	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_id CategoryTheory.Bicategory.whisker_exchange
comp_vhcomp 📖	mathematical	—	comp vcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct hcomp	—	—

CategoryTheory.Bicategory.leftAdjointSquareConjugate

Definitions

Name	Category	Theorems
vcomp 📖	CompOp	1 math math: CategoryTheory.Bicategory.mateEquiv_conjugateEquiv_vcomp

CategoryTheory.Bicategory.rightAdjointConjugateSquare

Definitions

Name	Category	Theorems
vcomp 📖	CompOp	1 math math: CategoryTheory.Bicategory.conjugateEquiv_mateEquiv_vcomp

CategoryTheory.Bicategory.rightAdjointSquare

Definitions

Name	Category	Theorems
comp 📖	CompOp	3 math math: comp_vhcomp, comp_hvcomp, CategoryTheory.Bicategory.mateEquiv_square
hcomp 📖	CompOp	3 math math: comp_vhcomp, comp_hvcomp, CategoryTheory.Bicategory.mateEquiv_hcomp
vcomp 📖	CompOp	3 math math: comp_vhcomp, CategoryTheory.Bicategory.mateEquiv_vcomp, comp_hvcomp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hvcomp 📖	mathematical	—	comp hcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct vcomp	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Bicategory.eval_comp Mathlib.Tactic.Bicategory.eval_whiskerRight Mathlib.Tactic.Bicategory.eval_whiskerLeft Mathlib.Tactic.Bicategory.eval_of Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of Mathlib.Tactic.Bicategory.evalWhiskerRight_nil Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of Mathlib.Tactic.Bicategory.evalComp_cons Mathlib.Tactic.Bicategory.evalComp_nil_nil Mathlib.Tactic.Bicategory.evalComp_nil_cons Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker Mathlib.Tactic.Bicategory.eval_bicategoricalComp Mathlib.Tactic.Bicategory.evalWhiskerRight_comp Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Bicategory.mk_eq_of_naturality Mathlib.Tactic.Bicategory.naturality_comp Mathlib.Tactic.Bicategory.naturality_inv Mathlib.Tactic.Bicategory.naturality_associator Mathlib.Tactic.Bicategory.naturality_whiskerRight Mathlib.Tactic.Bicategory.naturality_whiskerLeft Mathlib.Tactic.Bicategory.naturality_id CategoryTheory.Bicategory.whisker_exchange
comp_vhcomp 📖	mathematical	—	comp vcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Bicategory.toCategoryStruct hcomp	—	—

CategoryTheory.Bicategory.rightAdjointSquareConjugate

Definitions

Name	Category	Theorems
vcomp 📖	CompOp	1 math math: CategoryTheory.Bicategory.mateEquiv_conjugateEquiv_vcomp

---

← Back to Index