Basic

📁 Source: Mathlib/CategoryTheory/Join/Basic.lean

Statistics

Metric	Count
Definitions comp, edge, edgeTransform, homInduction, id, inclLeft, inclLeftFullyFaithful, inclRight, inclRightFullyFaithful, instCategory, instUniqueHomLeftRight, isoMkFunctor, mapIsoWhiskerLeft, mapIsoWhiskerRight, mapPair, mapPairComp, mapPairEquiv, mapPairId, mapPairLeft, mapPairRight, mapWhiskerLeft, mapWhiskerRight, mkFunctor, mkFunctorLeft, mkFunctorRight, mkNatIso, mkNatTrans, «term_⋆_»	28
Theorems edgeTransform_app, eq_mkNatTrans, false_of_right_to_left, homInduction_edge, homInduction_left, homInduction_right, id_left, id_right, inclLeftFaithful, inclLeftFull, inclLeft_obj, inclRightFaithful, inclRightFull, inclRight_obj, isEquivalenceMapPair, isoMkFunctor_hom_app, isoMkFunctor_inv_app, mapIsoWhiskerLeft_hom, mapIsoWhiskerLeft_hom_app, mapIsoWhiskerLeft_inv, mapIsoWhiskerLeft_inv_app, mapIsoWhiskerRight_hom, mapIsoWhiskerRight_hom_app, mapIsoWhiskerRight_inv, mapIsoWhiskerRight_inv_app, mapPairComp_hom_app_left, mapPairComp_hom_app_right, mapPairComp_inv_app_left, mapPairComp_inv_app_right, mapPairEquiv_counitIso, mapPairEquiv_functor, mapPairEquiv_inverse, mapPairEquiv_unitIso, mapPairId_hom_app, mapPairId_inv_app, mapPairLeft_hom_app, mapPairLeft_inv_app, mapPairRight_hom_app, mapPairRight_inv_app, mapPair_map_inclLeft, mapPair_map_inclRight, mapPair_obj_left, mapPair_obj_right, mapWhiskerLeft_app, mapWhiskerLeft_comp, mapWhiskerLeft_id, mapWhiskerRight_app, mapWhiskerRight_comp, mapWhiskerRight_id, mapWhisker_exchange, mkFunctorLeft_hom_app, mkFunctorLeft_inv_app, mkFunctorRight_hom_app, mkFunctorRight_inv_app, mkFunctor_edgeTransform, mkFunctor_map_edge, mkFunctor_map_inclLeft, mkFunctor_map_inclRight, mkFunctor_obj_left, mkFunctor_obj_right, mkNatIso_hom, mkNatIso_inv, mkNatTransComp, mkNatTrans_app_left, mkNatTrans_app_right, natTrans_ext, whiskerLeft_inclLeft_mkNatTrans, whiskerLeft_inclRight_mkNatTrans	68
Total	96

CategoryTheory.Join

Definitions

Name	Category	Theorems
comp 📖	CompOp	12 math math: pseudofunctorLeft_mapId_inv_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, pseudofunctorRight_mapComp_inv_toNatTrans_app, pseudofunctorLeft_mapId_hom_toNatTrans_app, pseudofunctorLeft_mapComp_hom_toNatTrans_app, pseudofunctorLeft_mapComp_inv_toNatTrans_app, pseudofunctorRight_mapId_hom_toNatTrans_app, pseudofunctorRight_mapId_inv_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp, pseudofunctorRight_mapComp_hom_toNatTrans_app, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp
edge 📖	CompOp	11 math math: pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, homInduction_edge, opEquiv_functor_map_op_edge, mapPairLeft_inv_app, mkFunctor_map_edge, opEquiv_inverse_map_edge_op, mapPairLeft_hom_app, mapPairRight_hom_app, mapPairRight_inv_app, edgeTransform_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map
edgeTransform 📖	CompOp	4 math math: isoMkFunctor_hom_app, mkFunctor_edgeTransform, isoMkFunctor_inv_app, edgeTransform_app
homInduction 📖	CompOp	5 math math: pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, homInduction_edge, homInduction_left, homInduction_right, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map
id 📖	CompOp	12 math math: pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, pseudofunctorLeft_mapId_inv_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, pseudofunctorRight_mapComp_inv_toNatTrans_app, pseudofunctorLeft_mapId_hom_toNatTrans_app, pseudofunctorLeft_mapComp_hom_toNatTrans_app, pseudofunctorLeft_mapComp_inv_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id, pseudofunctorRight_mapId_hom_toNatTrans_app, pseudofunctorRight_mapId_inv_toNatTrans_app, pseudofunctorRight_mapComp_hom_toNatTrans_app, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app
inclLeft 📖	CompOp	42 math math: pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, inlCompFromSum_hom_app, inclRightCompOpEquivInverse_inv_app_op, isoMkFunctor_hom_app, inrCompFromSum_hom_app, mkFunctor_edgeTransform, opEquiv_inverse_map_inclRight_op, mkFunctor_map_inclLeft, mapWhiskerRight_app, mapPair_map_inclLeft, isoMkFunctor_inv_app, mapIsoWhiskerRight_hom_app, opEquiv_functor_map_op_inclRight, mkFunctorLeft_hom_app, inclLeft_obj, mapPairLeft_inv_app, opEquiv_inverse_map_inclLeft_op, homInduction_left, InclLeftCompRightOpOpEquivFunctor_hom_app, inclRightCompOpEquivInverse_hom_app_op, inclLeftCompOpEquivInverse_inv_app_op, inclLeftCompOpEquivInverse_hom_app_op, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, InclLeftCompRightOpOpEquivFunctor_inv_app, instInitialInclLeftOfIsConnected, InclRightCompRightOpOpEquivFunctor_inv_app, inrCompFromSum_inv_app, mkFunctorLeft_inv_app, mapPairLeft_hom_app, mapPairRight_hom_app, opEquiv_functor_map_op_inclLeft, id_left, eq_mkNatTrans, fromSum_map_inl, inclLeftFull, InclRightCompRightOpOpEquivFunctor_hom_app, mapPairRight_inv_app, inlCompFromSum_inv_app, inclLeftFaithful, edgeTransform_app, mapIsoWhiskerRight_inv_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map
inclLeftFullyFaithful 📖	CompOp	—
inclRight 📖	CompOp	42 math math: pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, inlCompFromSum_hom_app, mapWhiskerLeft_app, inclRightCompOpEquivInverse_inv_app_op, id_right, isoMkFunctor_hom_app, inrCompFromSum_hom_app, mkFunctor_edgeTransform, mapPair_map_inclRight, instFinalInclRightOfIsConnected, opEquiv_inverse_map_inclRight_op, inclRightFaithful, mkFunctor_map_inclRight, isoMkFunctor_inv_app, fromSum_map_inr, opEquiv_functor_map_op_inclRight, mapPairLeft_inv_app, opEquiv_inverse_map_inclLeft_op, InclLeftCompRightOpOpEquivFunctor_hom_app, inclRightCompOpEquivInverse_hom_app_op, homInduction_right, inclRight_obj, inclLeftCompOpEquivInverse_inv_app_op, inclRightFull, inclLeftCompOpEquivInverse_hom_app_op, InclLeftCompRightOpOpEquivFunctor_inv_app, InclRightCompRightOpOpEquivFunctor_inv_app, mkFunctorRight_inv_app, inrCompFromSum_inv_app, mapPairLeft_hom_app, mapIsoWhiskerLeft_inv_app, mapPairRight_hom_app, opEquiv_functor_map_op_inclLeft, mapIsoWhiskerLeft_hom_app, eq_mkNatTrans, InclRightCompRightOpOpEquivFunctor_hom_app, mapPairRight_inv_app, mkFunctorRight_hom_app, inlCompFromSum_inv_app, edgeTransform_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map
inclRightFullyFaithful 📖	CompOp	—
instCategory 📖	CompOp	116 math math: pseudofunctorLeft_mapId_inv_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map, inlCompFromSum_hom_app, mapPairId_hom_app, mapWhiskerLeft_app, pseudofunctorRight_mapComp_inv_toNatTrans_app, mapPairEquiv_inverse, mapPairEquiv_unitIso, mapPairEquiv_counitIso, inclRightCompOpEquivInverse_inv_app_op, id_right, mapWhiskerRight_leftUnitor_hom, isoMkFunctor_hom_app, mapWhiskerLeft_whiskerRight, isEquivalenceMapPair, mkFunctor_obj_left, opEquiv_functor_obj_op_right, mapWhiskerLeft_whiskerLeft, inrCompFromSum_hom_app, mkFunctor_edgeTransform, mapPair_obj_right, mapIsoWhiskerLeft_hom, mapPair_map_inclRight, pseudofunctorLeft_mapId_hom_toNatTrans_app, instFinalInclRightOfIsConnected, opEquiv_inverse_map_inclRight_op, mkFunctor_map_inclLeft, mapWhiskerRight_comp, pseudofunctorLeft_mapComp_hom_toNatTrans_app, inclRightFaithful, mapWhiskerRight_whiskerRight, mkFunctor_map_inclRight, mapPairComp_hom_app_right, mapWhiskerRight_app, mapWhiskerLeft_whiskerRight_assoc, mapPair_map_inclLeft, isoMkFunctor_inv_app, mapIsoWhiskerRight_inv, pseudofunctorLeft_mapComp_inv_toNatTrans_app, fromSum_map_inr, opEquiv_functor_map_op_edge, mapIsoWhiskerRight_hom_app, opEquiv_functor_map_op_inclRight, opEquiv_inverse_obj_right_op, mkFunctorLeft_hom_app, mapWhiskerLeft_associator_hom, inclLeft_obj, mapPairComp_inv_app_right, mapPairLeft_inv_app, pseudofunctorRight_mapId_hom_toNatTrans_app, opEquiv_inverse_map_inclLeft_op, homInduction_left, InclLeftCompRightOpOpEquivFunctor_hom_app, mapWhiskerRight_associator_hom, inclRightCompOpEquivInverse_hom_app_op, pseudofunctorRight_mapId_inv_toNatTrans_app, homInduction_right, inclRight_obj, opEquiv_functor_obj_op_left, opEquiv_inverse_obj_left_op, instFaithfulSumFromSum, mapWhisker_exchange, inclLeftCompOpEquivInverse_inv_app_op, mapPairId_inv_app, mapWhiskerRight_whiskerLeft, inclRightFull, pseudofunctorRight_mapComp_hom_toNatTrans_app, mapWhiskerRight_whiskerLeft_assoc, mkFunctor_map_edge, mapPairComp_hom_app_left, inclLeftCompOpEquivInverse_hom_app_op, mapWhiskerLeft_associator_hom_assoc, mapWhiskerLeft_rightUnitor_hom, mapWhiskerRight_id, mapWhiskerRight_rightUnitor_hom, opEquiv_inverse_map_edge_op, mapPairComp_inv_app_left, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, InclLeftCompRightOpOpEquivFunctor_inv_app, mapIsoWhiskerRight_hom, instInitialInclLeftOfIsConnected, mapPair_obj_left, InclRightCompRightOpOpEquivFunctor_inv_app, mkFunctorRight_inv_app, mapWhiskerLeft_whiskerLeft_assoc, mapWhiskerLeft_id, mapWhiskerRight_whiskerRight_assoc, mapWhiskerLeft_leftUnitor_hom, fromSum_obj, inrCompFromSum_inv_app, mkFunctorLeft_inv_app, mapPairLeft_hom_app, mapIsoWhiskerLeft_inv_app, mkFunctor_obj_right, mapPairRight_hom_app, opEquiv_functor_map_op_inclLeft, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, id_left, mapIsoWhiskerLeft_hom_app, eq_mkNatTrans, mapPairEquiv_functor, instEssSurjSumFromSum, fromSum_map_inl, mapIsoWhiskerLeft_inv, inclLeftFull, mapWhiskerLeft_comp, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj, InclRightCompRightOpOpEquivFunctor_hom_app, mapPairRight_inv_app, mkFunctorRight_hom_app, inlCompFromSum_inv_app, inclLeftFaithful, edgeTransform_app, mapIsoWhiskerRight_inv_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map
instUniqueHomLeftRight 📖	CompOp	—
isoMkFunctor 📖	CompOp	2 math math: isoMkFunctor_hom_app, isoMkFunctor_inv_app
mapIsoWhiskerLeft 📖	CompOp	6 math math: mapPairEquiv_unitIso, mapPairEquiv_counitIso, mapIsoWhiskerLeft_hom, mapIsoWhiskerLeft_inv_app, mapIsoWhiskerLeft_hom_app, mapIsoWhiskerLeft_inv
mapIsoWhiskerRight 📖	CompOp	6 math math: mapPairEquiv_unitIso, mapPairEquiv_counitIso, mapIsoWhiskerRight_inv, mapIsoWhiskerRight_hom_app, mapIsoWhiskerRight_hom, mapIsoWhiskerRight_inv_app
mapPair 📖	CompOp	59 math math: pseudofunctorLeft_mapId_inv_toNatTrans_app, pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, mapPairId_hom_app, mapWhiskerLeft_app, pseudofunctorRight_mapComp_inv_toNatTrans_app, mapPairEquiv_inverse, mapPairEquiv_unitIso, mapPairEquiv_counitIso, mapWhiskerRight_leftUnitor_hom, mapWhiskerLeft_whiskerRight, isEquivalenceMapPair, mapWhiskerLeft_whiskerLeft, mapPair_obj_right, mapIsoWhiskerLeft_hom, mapPair_map_inclRight, pseudofunctorLeft_mapId_hom_toNatTrans_app, mapWhiskerRight_comp, pseudofunctorLeft_mapComp_hom_toNatTrans_app, mapWhiskerRight_whiskerRight, mapPairComp_hom_app_right, mapWhiskerRight_app, mapWhiskerLeft_whiskerRight_assoc, mapPair_map_inclLeft, mapIsoWhiskerRight_inv, pseudofunctorLeft_mapComp_inv_toNatTrans_app, mapIsoWhiskerRight_hom_app, mapWhiskerLeft_associator_hom, mapPairComp_inv_app_right, mapPairLeft_inv_app, pseudofunctorRight_mapId_hom_toNatTrans_app, mapWhiskerRight_associator_hom, pseudofunctorRight_mapId_inv_toNatTrans_app, mapWhisker_exchange, mapPairId_inv_app, mapWhiskerRight_whiskerLeft, pseudofunctorRight_mapComp_hom_toNatTrans_app, mapWhiskerRight_whiskerLeft_assoc, mapPairComp_hom_app_left, mapWhiskerLeft_associator_hom_assoc, mapWhiskerLeft_rightUnitor_hom, mapWhiskerRight_id, mapWhiskerRight_rightUnitor_hom, mapPairComp_inv_app_left, pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app, mapIsoWhiskerRight_hom, mapPair_obj_left, mapWhiskerLeft_whiskerLeft_assoc, mapWhiskerLeft_id, mapWhiskerRight_whiskerRight_assoc, mapWhiskerLeft_leftUnitor_hom, mapPairLeft_hom_app, mapIsoWhiskerLeft_inv_app, mapPairRight_hom_app, mapIsoWhiskerLeft_hom_app, mapPairEquiv_functor, mapIsoWhiskerLeft_inv, mapWhiskerLeft_comp, mapPairRight_inv_app, mapIsoWhiskerRight_inv_app
mapPairComp 📖	CompOp	10 math math: pseudofunctorRight_mapComp_inv_toNatTrans_app, mapPairEquiv_unitIso, mapPairEquiv_counitIso, pseudofunctorLeft_mapComp_hom_toNatTrans_app, mapPairComp_hom_app_right, pseudofunctorLeft_mapComp_inv_toNatTrans_app, mapPairComp_inv_app_right, pseudofunctorRight_mapComp_hom_toNatTrans_app, mapPairComp_hom_app_left, mapPairComp_inv_app_left
mapPairEquiv 📖	CompOp	4 math math: mapPairEquiv_inverse, mapPairEquiv_unitIso, mapPairEquiv_counitIso, mapPairEquiv_functor
mapPairId 📖	CompOp	8 math math: mapPairId_hom_app, mapPairEquiv_unitIso, mapPairEquiv_counitIso, mapWhiskerRight_leftUnitor_hom, mapPairId_inv_app, mapWhiskerLeft_rightUnitor_hom, mapWhiskerRight_rightUnitor_hom, mapWhiskerLeft_leftUnitor_hom
mapPairLeft 📖	CompOp	2 math math: mapPairLeft_inv_app, mapPairLeft_hom_app
mapPairRight 📖	CompOp	2 math math: mapPairRight_hom_app, mapPairRight_inv_app
mapWhiskerLeft 📖	CompOp	14 math math: mapWhiskerLeft_app, mapWhiskerLeft_whiskerRight, mapWhiskerLeft_whiskerLeft, mapIsoWhiskerLeft_hom, mapWhiskerLeft_whiskerRight_assoc, mapWhiskerLeft_associator_hom, mapWhisker_exchange, mapWhiskerLeft_associator_hom_assoc, mapWhiskerLeft_rightUnitor_hom, mapWhiskerLeft_whiskerLeft_assoc, mapWhiskerLeft_id, mapWhiskerLeft_leftUnitor_hom, mapIsoWhiskerLeft_inv, mapWhiskerLeft_comp
mapWhiskerRight 📖	CompOp	13 math math: mapWhiskerRight_leftUnitor_hom, mapWhiskerRight_comp, mapWhiskerRight_whiskerRight, mapWhiskerRight_app, mapIsoWhiskerRight_inv, mapWhiskerRight_associator_hom, mapWhisker_exchange, mapWhiskerRight_whiskerLeft, mapWhiskerRight_whiskerLeft_assoc, mapWhiskerRight_id, mapWhiskerRight_rightUnitor_hom, mapIsoWhiskerRight_hom, mapWhiskerRight_whiskerRight_assoc
mkFunctor 📖	CompOp	16 math math: isoMkFunctor_hom_app, mkFunctor_obj_left, mkFunctor_edgeTransform, mkFunctor_map_inclLeft, mkFunctor_map_inclRight, isoMkFunctor_inv_app, mkFunctorLeft_hom_app, mapPairLeft_inv_app, mkFunctor_map_edge, mkFunctorRight_inv_app, mkFunctorLeft_inv_app, mapPairLeft_hom_app, mkFunctor_obj_right, mapPairRight_hom_app, mapPairRight_inv_app, mkFunctorRight_hom_app
mkFunctorLeft 📖	CompOp	2 math math: mkFunctorLeft_hom_app, mkFunctorLeft_inv_app
mkFunctorRight 📖	CompOp	2 math math: mkFunctorRight_inv_app, mkFunctorRight_hom_app
mkNatIso 📖	CompOp	2 math math: mkNatIso_inv, mkNatIso_hom
mkNatTrans 📖	CompOp	8 math math: mkNatIso_inv, mkNatTrans_app_right, whiskerLeft_inclRight_mkNatTrans, mkNatTrans_app_left, whiskerLeft_inclLeft_mkNatTrans, eq_mkNatTrans, mkNatTransComp, mkNatIso_hom
«term_⋆_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
edgeTransform_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' CategoryTheory.Join instCategory CategoryTheory.Functor.comp CategoryTheory.Prod.fst inclLeft CategoryTheory.Prod.snd inclRight edgeTransform edge	—	—
eq_mkNatTrans 📖	mathematical	—	mkNatTrans CategoryTheory.Functor.whiskerLeft CategoryTheory.Join instCategory inclLeft inclRight	—	natTrans_ext
false_of_right_to_left 📖	—	—	—	—	—
homInduction_edge 📖	mathematical	—	homInduction left right edge	—	—
homInduction_left 📖	mathematical	—	homInduction CategoryTheory.Functor.obj CategoryTheory.Join instCategory inclLeft CategoryTheory.Functor.map	—	—
homInduction_right 📖	mathematical	—	homInduction CategoryTheory.Functor.obj CategoryTheory.Join instCategory inclRight CategoryTheory.Functor.map	—	—
id_left 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Join CategoryTheory.Category.toCategoryStruct instCategory left CategoryTheory.Functor.map inclLeft	—	—
id_right 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Join CategoryTheory.Category.toCategoryStruct instCategory right CategoryTheory.Functor.map inclRight	—	—
inclLeftFaithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Join instCategory inclLeft	—	CategoryTheory.Functor.FullyFaithful.faithful
inclLeftFull 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Join instCategory inclLeft	—	CategoryTheory.Functor.FullyFaithful.full
inclLeft_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Join instCategory inclLeft left	—	—
inclRightFaithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Join instCategory inclRight	—	CategoryTheory.Functor.FullyFaithful.faithful
inclRightFull 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Join instCategory inclRight	—	CategoryTheory.Functor.FullyFaithful.full
inclRight_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Join instCategory inclRight right	—	—
isEquivalenceMapPair 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Join instCategory mapPair	—	CategoryTheory.Equivalence.isEquivalence_functor
isoMkFunctor_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mkFunctor CategoryTheory.Functor.comp inclLeft inclRight CategoryTheory.Functor.whiskerRight CategoryTheory.prod' CategoryTheory.Prod.fst CategoryTheory.Prod.snd edgeTransform CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category isoMkFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id left right	—	—
isoMkFunctor_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mkFunctor CategoryTheory.Functor.comp inclLeft inclRight CategoryTheory.Functor.whiskerRight CategoryTheory.prod' CategoryTheory.Prod.fst CategoryTheory.Prod.snd edgeTransform CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category isoMkFunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id left right	—	—
mapIsoWhiskerLeft_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Functor.category mapPair mapIsoWhiskerLeft mapWhiskerLeft	—	—
mapIsoWhiskerLeft_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mapPair CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapIsoWhiskerLeft Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id left CategoryTheory.Functor.map inclRight	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mapIsoWhiskerLeft_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Functor.category mapPair mapIsoWhiskerLeft mapWhiskerLeft	—	CategoryTheory.NatTrans.ext' CategoryTheory.Functor.isoWhiskerRight_refl CategoryTheory.Iso.refl_trans CategoryTheory.Category.assoc mkNatIso.congr_simp mkNatTrans.congr_simp CategoryTheory.Category.comp_id mapWhiskerLeft_app CategoryTheory.Category.id_comp
mapIsoWhiskerLeft_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mapPair CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapIsoWhiskerLeft Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id left CategoryTheory.Functor.map inclRight	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mapIsoWhiskerRight_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Functor.category mapPair mapIsoWhiskerRight mapWhiskerRight	—	—
mapIsoWhiskerRight_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mapPair CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapIsoWhiskerRight Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map inclLeft CategoryTheory.CategoryStruct.id right	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id
mapIsoWhiskerRight_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Functor.category mapPair mapIsoWhiskerRight mapWhiskerRight	—	CategoryTheory.NatTrans.ext' CategoryTheory.Functor.isoWhiskerRight_refl CategoryTheory.Iso.refl_trans CategoryTheory.Category.assoc mkNatIso.congr_simp mkNatTrans.congr_simp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp mapWhiskerRight_app
mapIsoWhiskerRight_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mapPair CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapIsoWhiskerRight Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map inclLeft CategoryTheory.CategoryStruct.id right	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Functor.map_id
mapPairComp_hom_app_left 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mapPair CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapPairComp left CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
mapPairComp_hom_app_right 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mapPair CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapPairComp right CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
mapPairComp_inv_app_left 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory CategoryTheory.Functor.comp mapPair CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapPairComp left CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
mapPairComp_inv_app_right 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory CategoryTheory.Functor.comp mapPair CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapPairComp right CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
mapPairEquiv_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Join instCategory mapPairEquiv CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp mapPair CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Iso.symm mapPairComp mapIsoWhiskerRight mapIsoWhiskerLeft mapPairId	—	—
mapPairEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Join instCategory mapPairEquiv mapPair	—	—
mapPairEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Join instCategory mapPairEquiv mapPair	—	—
mapPairEquiv_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Join instCategory mapPairEquiv CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id mapPair CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.inverse CategoryTheory.Iso.symm mapPairId mapIsoWhiskerRight mapIsoWhiskerLeft mapPairComp	—	—
mapPairId_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mapPair CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapPairId Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id left right	—	CategoryTheory.Category.comp_id
mapPairId_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory CategoryTheory.Functor.id mapPair CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapPairId Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id left right	—	CategoryTheory.Category.comp_id
mapPairLeft_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory CategoryTheory.Functor.comp inclLeft mkFunctor inclRight CategoryTheory.prod' CategoryTheory.Prod.fst CategoryTheory.Prod.snd edge CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapPair mapPairLeft CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct left	—	—
mapPairLeft_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory CategoryTheory.Functor.comp inclLeft mkFunctor inclRight CategoryTheory.prod' CategoryTheory.Prod.fst CategoryTheory.Prod.snd edge CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapPair mapPairLeft CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct left	—	—
mapPairRight_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory CategoryTheory.Functor.comp inclRight mkFunctor inclLeft CategoryTheory.prod' CategoryTheory.Prod.fst CategoryTheory.Prod.snd edge CategoryTheory.Functor.obj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapPair mapPairRight CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct right	—	—
mapPairRight_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory CategoryTheory.Functor.comp inclRight mkFunctor inclLeft CategoryTheory.prod' CategoryTheory.Prod.fst CategoryTheory.Prod.snd edge CategoryTheory.Functor.obj CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapPair mapPairRight CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct right	—	—
mapPair_map_inclLeft 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Join instCategory mapPair CategoryTheory.Functor.obj inclLeft	—	—
mapPair_map_inclRight 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Join instCategory mapPair CategoryTheory.Functor.obj inclRight	—	—
mapPair_obj_left 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Join instCategory mapPair left	—	—
mapPair_obj_right 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Join instCategory mapPair right	—	—
mapWhiskerLeft_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mapPair mapWhiskerLeft Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.id left CategoryTheory.Functor.map inclRight	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mapWhiskerLeft_comp 📖	mathematical	—	mapWhiskerLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Join instCategory mapPair	—	CategoryTheory.NatTrans.ext' mapWhiskerLeft_app CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id
mapWhiskerLeft_id 📖	mathematical	—	mapWhiskerLeft CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Join instCategory mapPair	—	CategoryTheory.NatTrans.ext' mapWhiskerLeft_app CategoryTheory.Functor.map_id
mapWhiskerRight_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Join instCategory mapPair mapWhiskerRight Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map inclLeft CategoryTheory.CategoryStruct.id right	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id
mapWhiskerRight_comp 📖	mathematical	—	mapWhiskerRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Join instCategory mapPair	—	CategoryTheory.NatTrans.ext' mapWhiskerRight_app CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id
mapWhiskerRight_id 📖	mathematical	—	mapWhiskerRight CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Join instCategory mapPair	—	CategoryTheory.NatTrans.ext' mapWhiskerRight_app CategoryTheory.Functor.map_id
mapWhisker_exchange 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Join instCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category mapPair mapWhiskerLeft mapWhiskerRight	—	CategoryTheory.NatTrans.ext' mapWhiskerLeft_app mapWhiskerRight_app CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
mkFunctorLeft_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Join instCategory inclLeft mkFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mkFunctorLeft CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
mkFunctorLeft_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Join instCategory inclLeft mkFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mkFunctorLeft CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
mkFunctorRight_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Join instCategory inclRight mkFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mkFunctorRight CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
mkFunctorRight_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Join instCategory inclRight mkFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mkFunctorRight CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
mkFunctor_edgeTransform 📖	mathematical	—	CategoryTheory.Functor.whiskerRight CategoryTheory.prod' CategoryTheory.Join instCategory CategoryTheory.Functor.comp CategoryTheory.Prod.fst inclLeft CategoryTheory.Prod.snd inclRight edgeTransform mkFunctor	—	CategoryTheory.NatTrans.ext'
mkFunctor_map_edge 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Join instCategory mkFunctor left right edge CategoryTheory.NatTrans.app CategoryTheory.prod' CategoryTheory.Functor.comp CategoryTheory.Prod.fst CategoryTheory.Prod.snd	—	—
mkFunctor_map_inclLeft 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Join instCategory mkFunctor CategoryTheory.Functor.obj inclLeft	—	—
mkFunctor_map_inclRight 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Join instCategory mkFunctor CategoryTheory.Functor.obj inclRight	—	—
mkFunctor_obj_left 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Join instCategory mkFunctor left	—	—
mkFunctor_obj_right 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Join instCategory mkFunctor right	—	—
mkNatIso_hom 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Join instCategory CategoryTheory.Prod.fst inclLeft CategoryTheory.Prod.snd inclRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerRight edgeTransform CategoryTheory.Iso.hom CategoryTheory.Functor.isoWhiskerLeft	mkNatIso mkNatTrans	—	—
mkNatIso_inv 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Join instCategory CategoryTheory.Prod.fst inclLeft CategoryTheory.Prod.snd inclRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerRight edgeTransform CategoryTheory.Iso.hom CategoryTheory.Functor.isoWhiskerLeft	CategoryTheory.Iso.inv mkNatIso mkNatTrans	—	—
mkNatTransComp 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Join instCategory CategoryTheory.Prod.fst inclLeft CategoryTheory.Prod.snd inclRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerRight edgeTransform CategoryTheory.Functor.whiskerLeft	mkNatTrans	—	natTrans_ext
mkNatTrans_app_left 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Join instCategory CategoryTheory.Prod.fst inclLeft CategoryTheory.Prod.snd inclRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerRight edgeTransform CategoryTheory.Functor.whiskerLeft	CategoryTheory.NatTrans.app mkNatTrans left	—	—
mkNatTrans_app_right 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Join instCategory CategoryTheory.Prod.fst inclLeft CategoryTheory.Prod.snd inclRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerRight edgeTransform CategoryTheory.Functor.whiskerLeft	CategoryTheory.NatTrans.app mkNatTrans right	—	—
natTrans_ext 📖	—	CategoryTheory.Functor.whiskerLeft CategoryTheory.Join instCategory inclLeft inclRight	—	—	CategoryTheory.NatTrans.ext'
whiskerLeft_inclLeft_mkNatTrans 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Join instCategory CategoryTheory.Prod.fst inclLeft CategoryTheory.Prod.snd inclRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerRight edgeTransform CategoryTheory.Functor.whiskerLeft	mkNatTrans	—	—
whiskerLeft_inclRight_mkNatTrans 📖	mathematical	Quiver.Hom CategoryTheory.Functor CategoryTheory.prod' CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Join instCategory CategoryTheory.Prod.fst inclLeft CategoryTheory.Prod.snd inclRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerRight edgeTransform CategoryTheory.Functor.whiskerLeft	mkNatTrans	—	—

---

← Back to Index