Theorems · Definition · category theory

CategoryTheory.forget

(C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] →
          [CategoryTheory.ConcreteCategory C FC] → CategoryTheory.Functor C (Type w)

The forgetful functor from a concrete category to the category of types.

Defined in

Mathlib.CategoryTheory.ConcreteCategory.Forget

Cited by

418 results in Mathlib

Foundations

Depth 19 from the axioms, rests on 104 definitions · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryoutParamCategoryTheory.ConcreteCategory