Mathlib Map

Theorems · Theorem · category theory

TypeCat.Fun.ext

∀ {X : Type u_1} {Y : Type u_2} {x y : TypeCat.Fun X Y}, x.toFun = y.toFun → x = y
Defined in
Mathlib.CategoryTheory.Types.Basic
Cited by
74 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Limits.Types.jointly_surjective_of_isColimit · cited by 27Types.jointly_surjective_…CategoryTheory.Subfunctor.homOfLe_ι · cited by 8Subfunctor.homOfLe_ιSSet.const_comp · cited by 4SSet.const_compSSet.Truncated.IsStrictSegal.hom_ext · cited by 3IsStrictSegal.hom_extCategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst · cited by 3Types.pullbackIsoPullback…CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd · cited by 3Types.pullbackIsoPullback…smoothSheafCommRing.forgetStalk_inv_comp_eval · cited by 3smoothSheafCommRing.forge…CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso · cited by 2LocallyConstant.sigmaComp…CategoryTheory.Functor.RepresentableBy.isRepresentedBy · cited by 2RepresentableBy.isReprese…CategoryTheory.Equalizer.Presieve.Arrows.w · cited by 2Arrows.wCategoryTheory.Square.IsPullback.iff_of_equiv · cited by 2IsPullback.iff_of_equivCategoryTheory.Presheaf.comp_χ_eq · cited by 2Presheaf.comp_χ_eqCategoryTheory.Equalizer.Presieve.w · cited by 2Presieve.wCategoryTheory.Functor.CoconeTypes.isColimit_iff · cited by 1CoconeTypes.isColimit_iffHasCardinalLT.isCardinalPresentable · cited by 1HasCardinalLT.isCardinalP…TypeCat.Fun · cited by 1307TypeCat.FunTypeCat.Fun.toFun · cited by 47Fun.toFunFun.extCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by74

Results whose statement or proof uses this declaration.