Theorems · Inductive type · category theory

CategoryTheory.Functor

(C : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} C] → (D : Type u₂) → [CategoryTheory.Category.{v₂, u₂} D] → Type (max v₁ v₂ u₁ u₂)

Functor C D represents a functor between categories C and D. To apply a functor F to an object use F.obj X, and to a morphism use F.map f. The axiom map_id expresses preservation of identities, and map_comp expresses functoriality.

Defined in

Mathlib.CategoryTheory.Functor.Basic

Cited by

16,252 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category