Basic

📁 Source: Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean

Statistics

Metric	Count
Definitions toOverCompCoyoneda, toOverCompOverEquivPresheafCostructuredArrow, toOverCompYoneda, MakesOverArrow, OverArrows, costructuredArrowIso, map₁, map₂, val, yonedaArrow, YonedaCollection, fst, map₁, map₂, mk, snd, yonedaEquivFst, costructuredArrowPresheafToOver, counit, counitAux, counitAuxAux, counitBackward, counitForward, restrictedYoneda, restrictedYonedaObj, restrictedYonedaObjMap₁, toOverYonedaCompRestrictedYoneda, unit, unitAux, unitAuxAux, unitAuxAuxAux, unitBackward, unitForward, yonedaCollectionFunctor, yonedaCollectionPresheaf, yonedaCollectionPresheafMap₁, yonedaCollectionPresheafToA, overEquivPresheafCostructuredArrow	38
Theorems overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda, overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda, overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda, app, map₁, map₂, of_arrow, of_yoneda_arrow, app_val, ext, ext_iff, map_val, map₁_map₂, map₁_val, map₂_val, val_mk, yonedaArrow_val, yonedaCollectionPresheafToA_val_fst, ext, map₁_comp, map₁_fst, map₁_id, map₁_map₂, map₁_snd, map₁_yonedaEquivFst, map₂_comp, map₂_fst, map₂_id, map₂_snd, map₂_yonedaEquivFst, mk_fst, mk_snd, yonedaEquivFst_eq, app_unitForward, costructuredArrowPresheafToOver_map, costructuredArrowPresheafToOver_obj, counitAuxAux_hom, counitAuxAux_inv, counitAux_hom, counitBackward_counitForward, counitForward_counitBackward, counitForward_naturality₁, counitForward_naturality₂, counitForward_val_fst, counitForward_val_snd, map_mkPrecomp_eqToHom, restrictedYonedaObjMap₁_app, restrictedYonedaObj_map, restrictedYonedaObj_obj, restrictedYoneda_map, restrictedYoneda_obj, unitAuxAuxAux_hom, unitAuxAuxAux_inv, unitAuxAux_hom_app, unitAuxAux_inv_app_fst, unitAuxAux_inv_app_snd_coe, unitAux_hom, unitBackward_unitForward, unitForward_naturality₁, unitForward_naturality₂, unitForward_unitBackward, yonedaCollectionFunctor_map, yonedaCollectionFunctor_obj, yonedaCollectionPresheafMap₁_app, yonedaCollectionPresheafToA_app, yonedaCollectionPresheaf_map, yonedaCollectionPresheaf_obj	68
Total	106

CategoryTheory

Definitions

Name	Category	Theorems
overEquivPresheafCostructuredArrow 📖	CompOp	4 math math: CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda, CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda, CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda

CategoryTheory.CostructuredArrow

Definitions

Name	Category	Theorems
toOverCompCoyoneda 📖	CompOp	2 math math: overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda
toOverCompOverEquivPresheafCostructuredArrow 📖	CompOp	4 math math: overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda, overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda, overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda, overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda
toOverCompYoneda 📖	CompOp	2 math math: overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda, overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.instCategoryOver CategoryTheory.CostructuredArrow CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Equivalence.functor CategoryTheory.overEquivPresheafCostructuredArrow Opposite.unop CategoryTheory.Functor.obj CategoryTheory.Functor.op toOver Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.coyoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.inv toOverCompCoyoneda CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom toOverCompOverEquivPresheafCostructuredArrow	—	CategoryTheory.Category.comp_id CategoryTheory.Functor.FullyFaithful.map_preimage
overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.instCategoryOver CategoryTheory.CostructuredArrow CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Equivalence.functor CategoryTheory.overEquivPresheafCostructuredArrow Opposite.unop CategoryTheory.Functor.obj CategoryTheory.Functor.op toOver Opposite.op CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv toOverCompYoneda CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom toOverCompOverEquivPresheafCostructuredArrow	—	CategoryTheory.Category.comp_id CategoryTheory.Functor.FullyFaithful.map_preimage
overEquivPresheafCostructuredArrow_inverse_map_toOverCompCoyoneda 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Equivalence.inverse CategoryTheory.overEquivPresheafCostructuredArrow Opposite.unop CategoryTheory.Functor.obj CategoryTheory.Functor.op Opposite.op CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp toOver CategoryTheory.coyoneda CategoryTheory.Functor.whiskeringLeft CategoryTheory.Iso.hom toOverCompCoyoneda CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Iso.isoCompInverse toOverCompOverEquivPresheafCostructuredArrow CategoryTheory.Functor.id CategoryTheory.Equivalence.unit	—	CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp CategoryTheory.Equivalence.inv_fun_map CategoryTheory.Iso.isoCompInverse_inv_app CategoryTheory.Category.assoc
overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Equivalence.inverse CategoryTheory.overEquivPresheafCostructuredArrow Opposite.unop CategoryTheory.Functor.obj CategoryTheory.Functor.op Opposite.op CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp toOver CategoryTheory.Iso.hom toOverCompYoneda CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Iso.isoCompInverse toOverCompOverEquivPresheafCostructuredArrow CategoryTheory.Functor.id CategoryTheory.Equivalence.unit	—	CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp CategoryTheory.Equivalence.inv_fun_map CategoryTheory.Iso.isoCompInverse_inv_app CategoryTheory.Category.assoc

CategoryTheory.OverPresheafAux

Definitions

Name	Category	Theorems
MakesOverArrow 📖	CompData	3 math math: unitAuxAux_inv_app_snd_coe, MakesOverArrow.of_yoneda_arrow, MakesOverArrow.of_arrow
OverArrows 📖	CompOp	6 math math: counitAuxAux_inv, counitBackward_counitForward, counitAux_hom, restrictedYonedaObj_obj, counitForward_counitBackward, counitAuxAux_hom
YonedaCollection 📖	CompOp	9 math math: YonedaCollection.map₂_comp, unitAuxAuxAux_hom, unitAuxAuxAux_inv, yonedaCollectionPresheaf_obj, YonedaCollection.map₂_id, unitBackward_unitForward, YonedaCollection.map₁_comp, unitForward_unitBackward, YonedaCollection.map₁_id
costructuredArrowPresheafToOver 📖	CompOp	3 math math: costructuredArrowPresheafToOver_map, unitAux_hom, costructuredArrowPresheafToOver_obj
counit 📖	CompOp	—
counitAux 📖	CompOp	1 math math: counitAux_hom
counitAuxAux 📖	CompOp	3 math math: counitAuxAux_inv, counitAux_hom, counitAuxAux_hom
counitBackward 📖	CompOp	3 math math: counitAuxAux_inv, counitBackward_counitForward, counitForward_counitBackward
counitForward 📖	CompOp	7 math math: counitForward_naturality₁, counitForward_val_snd, counitBackward_counitForward, counitForward_counitBackward, counitAuxAux_hom, counitForward_val_fst, counitForward_naturality₂
restrictedYoneda 📖	CompOp	3 math math: unitAux_hom, restrictedYoneda_map, restrictedYoneda_obj
restrictedYonedaObj 📖	CompOp	16 math math: unitAux_hom, restrictedYoneda_obj, unitAuxAuxAux_hom, unitAuxAuxAux_inv, unitForward_naturality₂, restrictedYonedaObj_map, counitAux_hom, unitBackward_unitForward, unitAuxAux_inv_app_fst, unitAuxAux_inv_app_snd_coe, restrictedYonedaObj_obj, restrictedYonedaObjMap₁_app, app_unitForward, unitForward_unitBackward, unitAuxAux_hom_app, unitForward_naturality₁
restrictedYonedaObjMap₁ 📖	CompOp	3 math math: restrictedYoneda_map, restrictedYonedaObjMap₁_app, unitForward_naturality₁
toOverYonedaCompRestrictedYoneda 📖	CompOp	—
unit 📖	CompOp	—
unitAux 📖	CompOp	1 math math: unitAux_hom
unitAuxAux 📖	CompOp	4 math math: unitAux_hom, unitAuxAux_inv_app_fst, unitAuxAux_inv_app_snd_coe, unitAuxAux_hom_app
unitAuxAuxAux 📖	CompOp	2 math math: unitAuxAuxAux_hom, unitAuxAuxAux_inv
unitBackward 📖	CompOp	3 math math: unitAuxAuxAux_inv, unitBackward_unitForward, unitForward_unitBackward
unitForward 📖	CompOp	7 math math: unitAuxAuxAux_hom, unitForward_naturality₂, unitBackward_unitForward, app_unitForward, unitForward_unitBackward, unitAuxAux_hom_app, unitForward_naturality₁
yonedaCollectionFunctor 📖	CompOp	2 math math: yonedaCollectionFunctor_obj, yonedaCollectionFunctor_map
yonedaCollectionPresheaf 📖	CompOp	21 math math: costructuredArrowPresheafToOver_map, unitAux_hom, OverArrows.yonedaCollectionPresheafToA_val_fst, yonedaCollectionPresheaf_map, counitForward_naturality₁, yonedaCollectionPresheafToA_app, counitForward_val_snd, yonedaCollectionFunctor_obj, counitAuxAux_inv, counitBackward_counitForward, yonedaCollectionPresheaf_obj, counitAux_hom, unitAuxAux_inv_app_fst, unitAuxAux_inv_app_snd_coe, unitAuxAux_hom_app, yonedaCollectionPresheafMap₁_app, counitForward_counitBackward, costructuredArrowPresheafToOver_obj, counitAuxAux_hom, counitForward_val_fst, counitForward_naturality₂
yonedaCollectionPresheafMap₁ 📖	CompOp	4 math math: costructuredArrowPresheafToOver_map, counitForward_naturality₁, yonedaCollectionFunctor_map, yonedaCollectionPresheafMap₁_app
yonedaCollectionPresheafToA 📖	CompOp	14 math math: costructuredArrowPresheafToOver_map, unitAux_hom, OverArrows.yonedaCollectionPresheafToA_val_fst, counitForward_naturality₁, yonedaCollectionPresheafToA_app, counitForward_val_snd, counitAuxAux_inv, counitBackward_counitForward, counitAux_hom, counitForward_counitBackward, costructuredArrowPresheafToOver_obj, counitAuxAux_hom, counitForward_val_fst, counitForward_naturality₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_unitForward 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types unitForward Opposite.unop YonedaCollection.yonedaEquivFst restrictedYonedaObj	—	OverArrows.app_val
costructuredArrowPresheafToOver_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Over CategoryTheory.instCategoryOver costructuredArrowPresheafToOver CategoryTheory.CostructuredArrow.homMk CategoryTheory.Functor.id yonedaCollectionPresheaf yonedaCollectionPresheafToA yonedaCollectionPresheafMap₁	—	—
costructuredArrowPresheafToOver_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Over CategoryTheory.instCategoryOver costructuredArrowPresheafToOver yonedaCollectionPresheaf CategoryTheory.Functor.id yonedaCollectionPresheafToA	—	—
counitAuxAux_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow Opposite.op OverArrows yonedaCollectionPresheaf yonedaCollectionPresheafToA CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom counitAuxAux counitForward	—	—
counitAuxAux_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow Opposite.op OverArrows yonedaCollectionPresheaf yonedaCollectionPresheafToA CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom counitAuxAux counitBackward	—	—
counitAux_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow restrictedYonedaObj yonedaCollectionPresheaf yonedaCollectionPresheafToA counitAux CategoryTheory.Functor.obj OverArrows CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.Comma.hom counitAuxAux	—	—
counitBackward_counitForward 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow Opposite.op OverArrows yonedaCollectionPresheaf yonedaCollectionPresheafToA CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom counitBackward counitForward	—	counitForward_val_snd CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply CategoryTheory.FunctorToTypes.map_id_apply
counitForward_counitBackward 📖	mathematical	—	OverArrows yonedaCollectionPresheaf yonedaCollectionPresheafToA CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow Opposite.op counitForward counitBackward	—	OverArrows.ext YonedaCollection.ext OverArrows.yonedaCollectionPresheafToA_val_fst counitForward_val_snd CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply
counitForward_naturality₁ 📖	mathematical	—	counitForward Opposite.unop CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.NatTrans.app CategoryTheory.instCategoryCostructuredArrow OverArrows.map₁ yonedaCollectionPresheaf yonedaCollectionPresheafToA CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom yonedaCollectionPresheafMap₁	—	OverArrows.ext YonedaCollection.ext OverArrows.yonedaCollectionPresheafToA_val_fst YonedaCollection.map₁_fst YonedaCollection.map₁_snd counitForward_val_snd CategoryTheory.FunctorToTypes.naturality CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply
counitForward_naturality₂ 📖	mathematical	—	counitForward Opposite.unop CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.map CategoryTheory.instCategoryCostructuredArrow OverArrows.map₂ yonedaCollectionPresheaf yonedaCollectionPresheafToA CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	OverArrows.ext YonedaCollection.ext OverArrows.yonedaCollectionPresheafToA_val_fst YonedaCollection.map₂_fst CategoryTheory.CommaMorphism.w CategoryTheory.Category.comp_id CategoryTheory.eqToHom_unop CategoryTheory.CostructuredArrow.eqToHom_left CategoryTheory.Category.id_comp YonedaCollection.map₂_snd counitForward_val_snd CategoryTheory.FunctorToTypes.map_comp_apply map_mkPrecomp_eqToHom CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply
counitForward_val_fst 📖	mathematical	—	YonedaCollection.fst Opposite.unop Opposite.op CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.fromPUnit OverArrows.val yonedaCollectionPresheaf yonedaCollectionPresheafToA CategoryTheory.Comma.hom counitForward	—	OverArrows.yonedaCollectionPresheafToA_val_fst
counitForward_val_snd 📖	mathematical	—	YonedaCollection.snd Opposite.unop Opposite.op CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.fromPUnit OverArrows.val yonedaCollectionPresheaf yonedaCollectionPresheafToA CategoryTheory.Comma.hom counitForward CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow YonedaCollection.fst CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	YonedaCollection.mk_snd
map_mkPrecomp_eqToHom 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow Opposite.op CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.CostructuredArrow.mkPrecomp CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	CategoryTheory.FunctorToTypes.map_id_apply
restrictedYonedaObjMap₁_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow restrictedYonedaObj restrictedYonedaObjMap₁ OverArrows.map₁ CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.Comma.hom	—	—
restrictedYonedaObj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow restrictedYonedaObj OverArrows.map₂ CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
restrictedYonedaObj_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow restrictedYonedaObj OverArrows CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.Comma.hom	—	—
restrictedYoneda_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Over CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.instCategoryOver CategoryTheory.CostructuredArrow CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow restrictedYoneda restrictedYonedaObjMap₁ CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.left	—	—
restrictedYoneda_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.instCategoryOver CategoryTheory.CostructuredArrow CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow restrictedYoneda restrictedYonedaObj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom	—	—
unitAuxAuxAux_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types YonedaCollection restrictedYonedaObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op unitAuxAuxAux unitForward	—	—
unitAuxAuxAux_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.types YonedaCollection restrictedYonedaObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op unitAuxAuxAux unitBackward	—	—
unitAuxAux_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types yonedaCollectionPresheaf restrictedYonedaObj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitAuxAux unitForward Opposite.unop	—	—
unitAuxAux_inv_app_fst 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Opposite.unop CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow restrictedYonedaObj DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.yonedaEquiv CategoryTheory.NatTrans.app yonedaCollectionPresheaf CategoryTheory.Iso.inv unitAuxAux	—	Equiv.apply_symm_apply
unitAuxAux_inv_app_snd_coe 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.CostructuredArrow DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.yonedaEquiv CategoryTheory.NatTrans.app MakesOverArrow CategoryTheory.Comma.hom CategoryTheory.instCategoryCostructuredArrow restrictedYonedaObj yonedaCollectionPresheaf CategoryTheory.Iso.inv unitAuxAux OverArrows.val	—	CategoryTheory.eqToHom_unop CategoryTheory.CostructuredArrow.eqToHom_left CategoryTheory.FunctorToTypes.map_id_apply
unitAux_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Over CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow restrictedYoneda costructuredArrowPresheafToOver unitAux CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit yonedaCollectionPresheaf restrictedYonedaObj CategoryTheory.Comma.left CategoryTheory.Comma.hom yonedaCollectionPresheafToA unitAuxAux CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right	—	—
unitBackward_unitForward 📖	mathematical	—	YonedaCollection restrictedYonedaObj CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op unitBackward unitForward	—	YonedaCollection.ext YonedaCollection.mk_fst Equiv.symm_apply_apply OverArrows.app_val OverArrows.ext CategoryTheory.eqToHom_unop CategoryTheory.CostructuredArrow.eqToHom_left OverArrows.map₂.congr_simp CategoryTheory.FunctorToTypes.map_id_apply
unitForward_naturality₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	unitForward YonedaCollection.map₁ restrictedYonedaObj restrictedYonedaObjMap₁ CategoryTheory.NatTrans.app Opposite.op	—	CategoryTheory.eqToHom_unop CategoryTheory.CostructuredArrow.eqToHom_left YonedaCollection.map₁_snd OverArrows.map₂.congr_simp OverArrows.map₁_map₂ CategoryTheory.FunctorToTypes.map_id_apply
unitForward_naturality₂ 📖	mathematical	—	unitForward YonedaCollection.map₂ restrictedYonedaObj CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.eqToHom_unop CategoryTheory.CostructuredArrow.eqToHom_left CategoryTheory.Category.id_comp YonedaCollection.map₂_snd OverArrows.map₂.congr_simp
unitForward_unitBackward 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op YonedaCollection restrictedYonedaObj unitForward unitBackward	—	CategoryTheory.eqToHom_unop CategoryTheory.CostructuredArrow.eqToHom_left OverArrows.map₂.congr_simp CategoryTheory.FunctorToTypes.map_id_apply
yonedaCollectionFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow yonedaCollectionFunctor yonedaCollectionPresheafMap₁	—	—
yonedaCollectionFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow yonedaCollectionFunctor yonedaCollectionPresheaf	—	—
yonedaCollectionPresheafMap₁_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types yonedaCollectionPresheaf yonedaCollectionPresheafMap₁ YonedaCollection.map₁ Opposite.unop	—	—
yonedaCollectionPresheafToA_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types yonedaCollectionPresheaf yonedaCollectionPresheafToA YonedaCollection.yonedaEquivFst Opposite.unop	—	—
yonedaCollectionPresheaf_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types yonedaCollectionPresheaf YonedaCollection.map₂ Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
yonedaCollectionPresheaf_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types yonedaCollectionPresheaf YonedaCollection Opposite.unop	—	—

CategoryTheory.OverPresheafAux.MakesOverArrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app 📖	mathematical	CategoryTheory.OverPresheafAux.MakesOverArrow	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.yonedaEquiv	—	—
map₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.OverPresheafAux.MakesOverArrow	CategoryTheory.NatTrans.app Opposite.op	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise CategoryTheory.NatTrans.comp_app app
map₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda CategoryTheory.Functor.map CategoryTheory.OverPresheafAux.MakesOverArrow	Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.FunctorToTypes.naturality app CategoryTheory.yonedaEquiv_naturality
of_arrow 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda	CategoryTheory.OverPresheafAux.MakesOverArrow DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Opposite.op EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.yonedaEquiv	—	—
of_yoneda_arrow 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda CategoryTheory.Functor.map	CategoryTheory.OverPresheafAux.MakesOverArrow	—	CategoryTheory.yonedaEquiv_yoneda_map of_arrow

CategoryTheory.OverPresheafAux.OverArrows

Definitions

Name	Category	Theorems
costructuredArrowIso 📖	CompOp	—
map₁ 📖	CompOp	4 math math: CategoryTheory.OverPresheafAux.counitForward_naturality₁, map₁_map₂, CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁_app, map₁_val
map₂ 📖	CompOp	4 math math: map₂_val, map₁_map₂, CategoryTheory.OverPresheafAux.restrictedYonedaObj_map, CategoryTheory.OverPresheafAux.counitForward_naturality₂
val 📖	CompOp	11 math math: yonedaCollectionPresheafToA_val_fst, ext_iff, val_mk, map₂_val, CategoryTheory.OverPresheafAux.counitForward_val_snd, yonedaArrow_val, CategoryTheory.OverPresheafAux.unitAuxAux_inv_app_snd_coe, app_val, map₁_val, map_val, CategoryTheory.OverPresheafAux.counitForward_val_fst
yonedaArrow 📖	CompOp	1 math math: yonedaArrow_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_val 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op val DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.yonedaEquiv	—	CategoryTheory.OverPresheafAux.MakesOverArrow.app Subtype.prop
ext 📖	—	val	—	—	—
ext_iff 📖	mathematical	—	val	—	ext
map_val 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda Opposite.unop Opposite.op CategoryTheory.Functor.map val	—	Equiv.injective CategoryTheory.yonedaEquiv_comp CategoryTheory.yonedaEquiv_yoneda_map app_val
map₁_map₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda CategoryTheory.Functor.map	map₂ map₁	—	ext CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise CategoryTheory.NatTrans.naturality
map₁_val 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category	val map₁ CategoryTheory.NatTrans.app Opposite.op	—	—
map₂_val 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda CategoryTheory.Functor.map	val map₂ Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	—
val_mk 📖	mathematical	CategoryTheory.OverPresheafAux.MakesOverArrow	val CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op	—	—
yonedaArrow_val 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda CategoryTheory.Functor.map	val yonedaArrow	—	—
yonedaCollectionPresheafToA_val_fst 📖	mathematical	—	CategoryTheory.OverPresheafAux.YonedaCollection.fst Opposite.unop Opposite.op val CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA	—	EquivLike.toEmbeddingLike app_val

CategoryTheory.OverPresheafAux.YonedaCollection

Definitions

Name	Category	Theorems
fst 📖	CompOp	10 math math: CategoryTheory.OverPresheafAux.OverArrows.yonedaCollectionPresheafToA_val_fst, map₂_snd, yonedaEquivFst_eq, CategoryTheory.OverPresheafAux.counitForward_val_snd, mk_snd, map₁_snd, map₁_fst, map₂_fst, CategoryTheory.OverPresheafAux.counitForward_val_fst, mk_fst
map₁ 📖	CompOp	8 math math: map₁_yonedaEquivFst, map₁_map₂, map₁_comp, map₁_id, CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁_app, map₁_snd, CategoryTheory.OverPresheafAux.unitForward_naturality₁, map₁_fst
map₂ 📖	CompOp	8 math math: map₂_comp, map₂_yonedaEquivFst, CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf_map, map₂_snd, CategoryTheory.OverPresheafAux.unitForward_naturality₂, map₂_id, map₁_map₂, map₂_fst
mk 📖	CompOp	—
snd 📖	CompOp	4 math math: map₂_snd, CategoryTheory.OverPresheafAux.counitForward_val_snd, mk_snd, map₁_snd
yonedaEquivFst 📖	CompOp	5 math math: map₂_yonedaEquivFst, yonedaEquivFst_eq, CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA_app, map₁_yonedaEquivFst, CategoryTheory.OverPresheafAux.app_unitForward

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	fst CategoryTheory.Functor.map Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow Opposite.op CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct snd	—	—	CategoryTheory.FunctorToTypes.map_id_apply Equiv.injective
map₁_comp 📖	mathematical	—	map₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.OverPresheafAux.YonedaCollection	—	ext CategoryTheory.NatTrans.ext' CategoryTheory.types_ext map₁_fst map₁_snd CategoryTheory.FunctorToTypes.naturality CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply
map₁_fst 📖	mathematical	—	fst map₁	—	mk_fst
map₁_id 📖	mathematical	—	map₁ CategoryTheory.CategoryStruct.id CategoryTheory.Functor Opposite CategoryTheory.CostructuredArrow CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.OverPresheafAux.YonedaCollection	—	ext CategoryTheory.NatTrans.ext' CategoryTheory.types_ext map₁_fst
map₁_map₂ 📖	mathematical	—	map₂ map₁	—	ext CategoryTheory.NatTrans.ext' CategoryTheory.types_ext map₂_fst map₁_fst map₁_snd map₂_snd CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.FunctorToTypes.naturality CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply CategoryTheory.OverPresheafAux.map_mkPrecomp_eqToHom
map₁_snd 📖	mathematical	—	snd map₁ CategoryTheory.Functor.map Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow Opposite.op fst CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app	—	—
map₁_yonedaEquivFst 📖	mathematical	—	yonedaEquivFst map₁	—	map₁_fst
map₂_comp 📖	mathematical	—	map₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.OverPresheafAux.YonedaCollection	—	ext CategoryTheory.NatTrans.ext' CategoryTheory.types_ext map₂_fst CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc map₂_snd CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.OverPresheafAux.map_mkPrecomp_eqToHom CategoryTheory.FunctorToTypes.eqToHom_map_comp_apply CategoryTheory.CostructuredArrow.mkPrecomp_comp CategoryTheory.eqToHom_op CategoryTheory.eqToHom_trans
map₂_fst 📖	mathematical	—	fst map₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda CategoryTheory.Functor.map	—	mk_fst
map₂_id 📖	mathematical	—	map₂ CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.OverPresheafAux.YonedaCollection	—	ext CategoryTheory.NatTrans.ext' CategoryTheory.types_ext map₂_fst CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp map₂_snd CategoryTheory.CostructuredArrow.mkPrecomp_id CategoryTheory.eqToHom_op CategoryTheory.eqToHom_trans
map₂_snd 📖	mathematical	—	snd map₂ CategoryTheory.Functor.map Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow Opposite.op fst CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.CostructuredArrow.mkPrecomp CategoryTheory.eqToHom	—	CategoryTheory.FunctorToTypes.map_comp_apply
map₂_yonedaEquivFst 📖	mathematical	—	yonedaEquivFst map₂ CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	map₂_fst CategoryTheory.yonedaEquiv_naturality
mk_fst 📖	mathematical	—	fst	—	Equiv.apply_symm_apply
mk_snd 📖	mathematical	—	snd CategoryTheory.Functor.map Opposite CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow Opposite.op fst CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct	—	—
yonedaEquivFst_eq 📖	mathematical	—	yonedaEquivFst DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.yoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.yonedaEquiv fst	—	—

---

← Back to Index