Functor

📁 Source: Mathlib/CategoryTheory/Comma/StructuredArrow/Functor.lean

Statistics

Metric	Count
Definitions commaToGrothendieckPrecompFunctor, functor, grothendieckPrecompFunctorEquivalence, grothendieckPrecompFunctorToComma, grothendieckProj, mapCompιCompGrothendieckProj, preFunctor, ιCompGrothendieckPrecompFunctorToCommaCompFst, ιCompGrothendieckProj, functor	10
Theorems commaToGrothendieckPrecompFunctor_map_base, commaToGrothendieckPrecompFunctor_map_fiber, commaToGrothendieckPrecompFunctor_obj_base, commaToGrothendieckPrecompFunctor_obj_fiber, functor_map, functor_obj, grothendieckPrecompFunctorEquivalence_counitIso, grothendieckPrecompFunctorEquivalence_functor, grothendieckPrecompFunctorEquivalence_inverse, grothendieckPrecompFunctorEquivalence_unitIso, grothendieckPrecompFunctorToComma_map_left, grothendieckPrecompFunctorToComma_map_right, grothendieckPrecompFunctorToComma_obj_hom, grothendieckPrecompFunctorToComma_obj_left, grothendieckPrecompFunctorToComma_obj_right, grothendieckProj_map, grothendieckProj_obj, mapCompιCompGrothendieckProj_hom_app, mapCompιCompGrothendieckProj_inv_app, preFunctor_app, ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app, ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app, ιCompGrothendieckProj_hom_app, ιCompGrothendieckProj_inv_app, functor_map, functor_obj	26
Total	36

CategoryTheory.CostructuredArrow

Definitions

Name	Category	Theorems
commaToGrothendieckPrecompFunctor 📖	CompOp	7 math math: commaToGrothendieckPrecompFunctor_map_fiber, commaToGrothendieckPrecompFunctor_obj_fiber, commaToGrothendieckPrecompFunctor_map_base, grothendieckPrecompFunctorEquivalence_unitIso, grothendieckPrecompFunctorEquivalence_inverse, grothendieckPrecompFunctorEquivalence_counitIso, commaToGrothendieckPrecompFunctor_obj_base
functor 📖	CompOp	32 math math: CategoryTheory.Functor.instHasColimitGrothendieckFunctorCompGrothendieckProj, grothendieckPrecompFunctorToComma_map_left, functor_obj, grothendieckPrecompFunctorEquivalence_functor, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc, commaToGrothendieckPrecompFunctor_map_fiber, commaToGrothendieckPrecompFunctor_obj_fiber, ιCompGrothendieckProj_inv_app, CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom, grothendieckPrecompFunctorToComma_obj_right, commaToGrothendieckPrecompFunctor_map_base, ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app, grothendieckPrecompFunctorToComma_obj_left, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom_assoc, mapCompιCompGrothendieckProj_inv_app, functor_map, grothendieckPrecompFunctorEquivalence_unitIso, grothendieckProj_map, grothendieckPrecompFunctorEquivalence_inverse, preFunctor_app, grothendieckPrecompFunctorEquivalence_counitIso, grothendieckProj_obj, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, mapCompιCompGrothendieckProj_hom_app, ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app, grothendieckPrecompFunctorToComma_map_right, ιCompGrothendieckProj_hom_app, commaToGrothendieckPrecompFunctor_obj_base, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app, grothendieckPrecompFunctorToComma_obj_hom
grothendieckPrecompFunctorEquivalence 📖	CompOp	4 math math: grothendieckPrecompFunctorEquivalence_functor, grothendieckPrecompFunctorEquivalence_unitIso, grothendieckPrecompFunctorEquivalence_inverse, grothendieckPrecompFunctorEquivalence_counitIso
grothendieckPrecompFunctorToComma 📖	CompOp	14 math math: grothendieckPrecompFunctorToComma_map_left, grothendieckPrecompFunctorEquivalence_functor, ιCompGrothendieckProj_inv_app, grothendieckPrecompFunctorToComma_obj_right, ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app, grothendieckPrecompFunctorToComma_obj_left, mapCompιCompGrothendieckProj_inv_app, grothendieckPrecompFunctorEquivalence_unitIso, grothendieckPrecompFunctorEquivalence_counitIso, mapCompιCompGrothendieckProj_hom_app, ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app, grothendieckPrecompFunctorToComma_map_right, ιCompGrothendieckProj_hom_app, grothendieckPrecompFunctorToComma_obj_hom
grothendieckProj 📖	CompOp	14 math math: CategoryTheory.Functor.instHasColimitGrothendieckFunctorCompGrothendieckProj, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc, ιCompGrothendieckProj_inv_app, CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom_assoc, mapCompιCompGrothendieckProj_inv_app, grothendieckProj_map, grothendieckProj_obj, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, mapCompιCompGrothendieckProj_hom_app, ιCompGrothendieckProj_hom_app, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app
mapCompιCompGrothendieckProj 📖	CompOp	2 math math: mapCompιCompGrothendieckProj_inv_app, mapCompιCompGrothendieckProj_hom_app
preFunctor 📖	CompOp	1 math math: preFunctor_app
ιCompGrothendieckPrecompFunctorToCommaCompFst 📖	CompOp	2 math math: ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app, ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app
ιCompGrothendieckProj 📖	CompOp	4 math math: ιCompGrothendieckProj_inv_app, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, ιCompGrothendieckProj_hom_app, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commaToGrothendieckPrecompFunctor_map_base 📖	mathematical	—	CategoryTheory.Grothendieck.Hom.base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Comma.right CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory commaToGrothendieckPrecompFunctor CategoryTheory.CommaMorphism.right	—	—
commaToGrothendieckPrecompFunctor_map_fiber 📖	mathematical	—	CategoryTheory.Grothendieck.Hom.fiber CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Comma.right CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory commaToGrothendieckPrecompFunctor homMk CategoryTheory.Grothendieck.base CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.CommaMorphism.right CategoryTheory.Grothendieck.fiber CategoryTheory.CommaMorphism.left	—	—
commaToGrothendieckPrecompFunctor_obj_base 📖	mathematical	—	CategoryTheory.Grothendieck.base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory commaToGrothendieckPrecompFunctor CategoryTheory.Comma.right	—	—
commaToGrothendieckPrecompFunctor_obj_fiber 📖	mathematical	—	CategoryTheory.Grothendieck.fiber CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory commaToGrothendieckPrecompFunctor CategoryTheory.Comma.right CategoryTheory.Comma.left CategoryTheory.Comma.hom	—	—
functor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Functor.toCatHom CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow map	—	—
functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Cat.of CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	—	—
grothendieckPrecompFunctorEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Comma CategoryTheory.Grothendieck.instCategory CategoryTheory.commaCategory grothendieckPrecompFunctorEquivalence CategoryTheory.NatIso.ofComponents commaToGrothendieckPrecompFunctor grothendieckPrecompFunctorToComma CategoryTheory.Functor.id CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
grothendieckPrecompFunctorEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Comma CategoryTheory.Grothendieck.instCategory CategoryTheory.commaCategory grothendieckPrecompFunctorEquivalence grothendieckPrecompFunctorToComma	—	—
grothendieckPrecompFunctorEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Comma CategoryTheory.Grothendieck.instCategory CategoryTheory.commaCategory grothendieckPrecompFunctorEquivalence commaToGrothendieckPrecompFunctor	—	—
grothendieckPrecompFunctorEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Comma CategoryTheory.Grothendieck.instCategory CategoryTheory.commaCategory grothendieckPrecompFunctorEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id grothendieckPrecompFunctorToComma commaToGrothendieckPrecompFunctor CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
grothendieckPrecompFunctorToComma_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Grothendieck.base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Grothendieck.fiber CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Grothendieck.Hom.base CategoryTheory.Grothendieck.Hom.fiber	—	—
grothendieckPrecompFunctorToComma_map_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Grothendieck.base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Grothendieck.fiber CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Grothendieck.Hom.base	—	—
grothendieckPrecompFunctorToComma_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Functor.obj CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Grothendieck.instCategory CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Grothendieck.base CategoryTheory.Grothendieck.fiber	—	—
grothendieckPrecompFunctorToComma_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor.obj CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Grothendieck.instCategory CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Grothendieck.base CategoryTheory.Grothendieck.fiber	—	—
grothendieckPrecompFunctorToComma_obj_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor.obj CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Grothendieck.instCategory CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Grothendieck.base	—	—
grothendieckProj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Grothendieck functor CategoryTheory.Grothendieck.instCategory grothendieckProj CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Grothendieck.base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Cat.str CategoryTheory.Cat.of CategoryTheory.instCategoryCostructuredArrow map CategoryTheory.Grothendieck.Hom.base CategoryTheory.Grothendieck.fiber CategoryTheory.Grothendieck.Hom.fiber	—	—
grothendieckProj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Grothendieck functor CategoryTheory.Grothendieck.instCategory grothendieckProj CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Grothendieck.base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.id CategoryTheory.Grothendieck.fiber	—	—
mapCompιCompGrothendieckProj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft map CategoryTheory.Functor.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.id functor CategoryTheory.Cat.str CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Comma.fst proj CategoryTheory.Iso.hom grothendieckProj mapCompιCompGrothendieckProj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
mapCompιCompGrothendieckProj_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringLeft map proj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Cat.str CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Comma.fst CategoryTheory.Iso.inv grothendieckProj mapCompιCompGrothendieckProj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
preFunctor_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Functor.comp preFunctor CategoryTheory.Functor.toCatHom CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow pre	—	—
ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.comp functor CategoryTheory.Cat.str CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Comma.fst proj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category ιCompGrothendieckPrecompFunctorToCommaCompFst CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.comp functor CategoryTheory.Cat.str proj CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Comma.fst CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category ιCompGrothendieckPrecompFunctorToCommaCompFst CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
ιCompGrothendieckProj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.comp CategoryTheory.Functor.id functor CategoryTheory.Cat.str CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Comma.fst proj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category grothendieckProj ιCompGrothendieckProj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
ιCompGrothendieckProj_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.comp CategoryTheory.Functor.id functor CategoryTheory.Cat.str proj CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι CategoryTheory.Comma CategoryTheory.commaCategory grothendieckPrecompFunctorToComma CategoryTheory.Comma.fst CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category grothendieckProj ιCompGrothendieckProj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—

CategoryTheory.StructuredArrow

Definitions

Name	Category	Theorems
functor 📖	CompOp	2 math math: functor_map, functor_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Functor.toCatHom CategoryTheory.StructuredArrow Opposite.unop CategoryTheory.instCategoryStructuredArrow map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.category functor CategoryTheory.Cat.of CategoryTheory.StructuredArrow Opposite.unop CategoryTheory.instCategoryStructuredArrow	—	—

---

← Back to Index