Mathlib Map

Theorems · Definition · category theory

TypeCat.Fun.toFun

{X : Type u_1} → {Y : Type u_2} → TypeCat.Fun X Y → X → Y

The underlying function.

Defined in
Mathlib.CategoryTheory.Types.Basic
Cited by
47 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

TypeCat.Fun.ext · cited by 74Fun.extCategoryTheory.Subfunctor.homOfLe_ι · cited by 8Subfunctor.homOfLe_ιSSet.const_comp · cited by 4SSet.const_compCompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso · cited by 2LocallyConstant.sigmaComp…CategoryTheory.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.eventualRange_mapsTo · cited by 2Functor.eventualRange_map…CategoryTheory.Presheaf.χ_unique · cited by 1Presheaf.χ_uniqueCategoryTheory.Functor.CoconeTypes.isColimit_iff · cited by 1CoconeTypes.isColimit_iffCategoryTheory.ShortComplex.SnakeInput.δ_apply' · cited by 1SnakeInput.δ_apply'HasCardinalLT.isCardinalPresentable · cited by 1HasCardinalLT.isCardinalP…TypeCat.Fun.comp · cited by 1Fun.compCategoryTheory.Functor.IsDense.of_fullyFaithful_restrictedULiftYoneda · cited by 1IsDense.of_fullyFaithful_…CategoryTheory.Limits.PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux.iso_hom · cited by 1PreservesFiniteLimitsOfIs…TypeCat.Fun · cited by 1307TypeCat.FunFun.toFunCITED BYCITES

Cites1

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

Cited by48

Results whose statement or proof uses this declaration.