Mathlib.CategoryTheory.Category.Cat

CategoryTheory.Cat definition

Full source

/-- Category of categories. -/
@[nolint checkUnivs]
def Cat :=
  Bundled CategoryCategory.{v, u}

Category of categories

Informal description

The category `Cat` consists of all categories as objects, with functors between these categories as morphisms. The objects are represented using the `Bundled` structure to pair a type with its category instance.

CategoryTheory.Cat.instInhabited instance

: Inhabited Cat

Full source

instance : Inhabited Cat :=
  ⟨⟨Type u, CategoryTheory.types⟩⟩

The Category of Categories is Inhabited

Informal description

The category of categories `Cat` is inhabited.

CategoryTheory.Cat.instCoeSortType instance

: CoeSort Cat (Type u)

Full source

instance : CoeSort Cat (Type u) :=
  ⟨Bundled.α⟩

Categories as Types via Canonical Coercion

Informal description

For any category $C$ in the category of categories $\mathrm{Cat}$, there is a canonical way to view $C$ as a type.

CategoryTheory.Cat.str instance

(C : Cat.{v, u}) : Category.{v, u} C

Full source

instance str (C : CatCat.{v, u}) : Category.{v, u} C :=
  Bundled.str C

Categories in Cat are Categories

Informal description

For any category $C$ in the category of categories $\mathrm{Cat}$, $C$ has the structure of a category.

CategoryTheory.Cat.of definition

(C : Type u) [Category.{v} C] : Cat.{v, u}

Full source

/-- Construct a bundled `Cat` from the underlying type and the typeclass. -/
def of (C : Type u) [Category.{v} C] : CatCat.{v, u} :=
  Bundled.of C

Inclusion of a category into the category of all categories

Informal description

Given a type `C` equipped with a category structure, the function `Cat.of` constructs an object in the category `Cat` of all categories, represented as a bundled pair of the type `C` and its category instance.

CategoryTheory.Cat.bicategory instance

: Bicategory.{max v u, max v u} Cat.{v, u}

Full source

/-- Bicategory structure on `Cat` -/
instance bicategory : Bicategory.{max v u, max v u} CatCat.{v, u} where
  Hom C D := C ⥤ D
  id C := 𝟭 C
  comp F G := F ⋙ G
  homCategory := fun _ _ => Functor.category
  whiskerLeft {_} {_} {_} F _ _ η := whiskerLeft F η
  whiskerRight {_} {_} {_} _ _ η H := whiskerRight η H
  associator {_} {_} {_} _ := Functor.associator
  leftUnitor {_} _ := Functor.leftUnitor
  rightUnitor {_} _ := Functor.rightUnitor
  pentagon := fun {_} {_} {_} {_} {_}=> Functor.pentagon
  triangle {_} {_} {_} := Functor.triangle

Bicategory Structure on the Category of Categories

Informal description

The category of categories $\mathrm{Cat}$ has a natural bicategory structure, where objects are categories, 1-morphisms are functors, and 2-morphisms are natural transformations between functors.

CategoryTheory.Cat.bicategory.strict instance

: Bicategory.Strict Cat.{v, u}

Full source

/-- `Cat` is a strict bicategory. -/
instance bicategory.strict : Bicategory.Strict CatCat.{v, u} where
  id_comp {C} {D} F := by cases F; rfl
  comp_id {C} {D} F := by cases F; rfl
  assoc := by intros; rfl

Strict Bicategory Structure on the Category of Categories

Informal description

The bicategory structure on the category of categories $\mathrm{Cat}$ is strict, meaning that the associators and unitors are all identity morphisms.

CategoryTheory.Cat.category instance

: LargeCategory.{max v u} Cat.{v, u}

Full source

/-- Category structure on `Cat` -/
instance category : LargeCategory.{max v u} CatCat.{v, u} :=
  StrictBicategory.category CatCat.{v, u}

The Category Structure on the Category of Categories

Informal description

The category $\mathrm{Cat}$ of all categories forms a large category, where objects are categories and morphisms are functors between them. Composition of morphisms is given by composition of functors, and identity morphisms are given by identity functors.

CategoryTheory.Cat.id_obj theorem

{C : Cat} (X : C) : (𝟙 C : C ⥤ C).obj X = X

Full source

@[simp]
theorem id_obj {C : Cat} (X : C) : (𝟙 C : C ⥤ C).obj X = X :=
  rfl

Identity Functor Acts as Identity on Objects in $\mathrm{Cat}$

Informal description

For any category $C$ in the category of categories $\mathrm{Cat}$ and any object $X$ in $C$, the application of the identity functor $\mathrm{id}_C$ to $X$ yields $X$ itself, i.e., $(\mathrm{id}_C)(X) = X$.

CategoryTheory.Cat.id_map theorem

{C : Cat} {X Y : C} (f : X ⟶ Y) : (𝟙 C : C ⥤ C).map f = f

Full source

@[simp]
theorem id_map {C : Cat} {X Y : C} (f : X ⟶ Y) : (𝟙 C : C ⥤ C).map f = f :=
  rfl

Identity Functor Preserves Morphisms in Category of Categories

Informal description

For any category $C$ in the category of categories $\mathrm{Cat}$ and any morphism $f \colon X \to Y$ in $C$, the identity functor $\mathrm{id}_C \colon C \to C$ maps $f$ to itself, i.e., $(\mathrm{id}_C).\mathrm{map}(f) = f$.

CategoryTheory.Cat.comp_obj theorem

{C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) (X : C) : (F ≫ G).obj X = G.obj (F.obj X)

Full source

@[simp]
theorem comp_obj {C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) (X : C) : (F ≫ G).obj X = G.obj (F.obj X) :=
  rfl

Object Mapping of Functor Composition in the Category of Categories

Informal description

For any categories $C$, $D$, and $E$ in the category of categories $\mathrm{Cat}$, and for any functors $F \colon C \to D$ and $G \colon D \to E$, the object mapping of the composition $F \circ G$ applied to an object $X$ in $C$ is equal to the object mapping of $G$ applied to the object mapping of $F$ applied to $X$, i.e., $(F \circ G)(X) = G(F(X))$.

CategoryTheory.Cat.comp_map theorem

{C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) {X Y : C} (f : X ⟶ Y) : (F ≫ G).map f = G.map (F.map f)

Full source

@[simp]
theorem comp_map {C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) {X Y : C} (f : X ⟶ Y) :
    (F ≫ G).map f = G.map (F.map f) :=
  rfl

Functor Composition Preserves Morphism Mapping

Informal description

For any categories $C$, $D$, and $E$ in the category of categories $\mathrm{Cat}$, and for any functors $F \colon C \to D$ and $G \colon D \to E$, the mapping of a morphism $f \colon X \to Y$ in $C$ under the composition $F \circ G$ is equal to the mapping of $f$ under $G$ after mapping under $F$. That is, $(F \circ G)(f) = G(F(f))$.

CategoryTheory.Cat.id_app theorem

{C D : Cat} (F : C ⟶ D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X)

Full source

@[simp]
theorem id_app {C D : Cat} (F : C ⟶ D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl

Component of Identity Natural Transformation Equals Identity Morphism

Informal description

For any functor $F \colon C \to D$ between categories $C$ and $D$ in $\mathrm{Cat}$, and for any object $X$ in $C$, the component of the identity natural transformation $\mathrm{id}_F$ at $X$ equals the identity morphism $\mathrm{id}_{F(X)}$ in $D$. That is, $(\mathrm{id}_F)_X = \mathrm{id}_{F(X)}$.

CategoryTheory.Cat.comp_app theorem

{C D : Cat} {F G H : C ⟶ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : (α ≫ β).app X = α.app X ≫ β.app X

Full source

@[simp]
theorem comp_app {C D : Cat} {F G H : C ⟶ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
    (α ≫ β).app X = α.app X ≫ β.app X := rfl

Component-wise Composition of Natural Transformations in $\mathrm{Cat}$

Informal description

For any categories $C$ and $D$ in $\mathrm{Cat}$, and any natural transformations $\alpha \colon F \to G$ and $\beta \colon G \to H$ between functors $F, G, H \colon C \to D$, the component of the composition $\alpha \ggg \beta$ at any object $X \in C$ satisfies $(\alpha \ggg \beta)_X = \alpha_X \circ \beta_X$.

CategoryTheory.Cat.whiskerLeft_app theorem

{C D E : Cat} (F : C ⟶ D) {G H : D ⟶ E} (η : G ⟶ H) (X : C) : (F ◁ η).app X = η.app (F.obj X)

Full source

@[simp]
lemma whiskerLeft_app {C D E : Cat} (F : C ⟶ D) {G H : D ⟶ E} (η : G ⟶ H) (X : C) :
    (F ◁ η).app X = η.app (F.obj X) :=
  rfl

Left Whiskering of Natural Transformation Applied to Object

Informal description

For categories $C$, $D$, and $E$, a functor $F \colon C \to D$, functors $G, H \colon D \to E$, and a natural transformation $\eta \colon G \to H$, the application of the left whiskering $F \triangleleft \eta$ at an object $X \in C$ satisfies $(F \triangleleft \eta)_X = \eta_{F(X)}$.

CategoryTheory.Cat.whiskerRight_app theorem

{C D E : Cat} {F G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G) (X : C) : (η ▷ H).app X = H.map (η.app X)

Full source

@[simp]
lemma whiskerRight_app {C D E : Cat} {F G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G) (X : C) :
    (η ▷ H).app X = H.map (η.app X) :=
  rfl

Component Formula for Right Whiskering of Natural Transformations

Informal description

For categories $C$, $D$, and $E$, functors $F, G : C \to D$, a functor $H : D \to E$, a natural transformation $\eta : F \to G$, and an object $X$ in $C$, the application of the right whiskering $\eta \triangleright H$ at $X$ is equal to the image under $H$ of the component $\eta_X : F(X) \to G(X)$, i.e., $(\eta \triangleright H)_X = H(\eta_X)$.

CategoryTheory.Cat.eqToHom_app theorem

{C D : Cat} (F G : C ⟶ D) (h : F = G) (X : C) : (eqToHom h).app X = eqToHom (Functor.congr_obj h X)

Full source

@[simp]
theorem eqToHom_app {C D : Cat} (F G : C ⟶ D) (h : F = G) (X : C) :
    (eqToHom h).app X = eqToHom (Functor.congr_obj h X) :=
  CategoryTheory.eqToHom_app h X

Component Equality of Natural Transformation from Functor Equality in $\mathrm{Cat}$

Informal description

For any two functors $F$ and $G$ between categories $\mathcal{C}$ and $\mathcal{D}$ in the category of categories $\mathrm{Cat}$, if $h : F = G$ is an equality between the functors, then for every object $X$ in $\mathcal{C}$, the component of the natural transformation $\text{eqToHom}\, h$ at $X$ is equal to the morphism $\text{eqToHom}\, (F(X) = G(X))$ induced by the equality of objects $F(X) = G(X)$.

CategoryTheory.Cat.leftUnitor_hom_app theorem

{B C : Cat} (F : B ⟶ C) (X : B) : (λ_ F).hom.app X = eqToHom (by simp)

Full source

lemma leftUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : B) : (λ_ F).hom.app X = eqToHom (by simp) :=
  rfl

Component Formula for the Left Unitor Natural Isomorphism in $\mathrm{Cat}$

Informal description

For any functor $F \colon B \to C$ between categories $B$ and $C$ in the category of categories $\mathrm{Cat}$, and for any object $X$ in $B$, the component at $X$ of the natural isomorphism $\lambda_F \colon \mathrm{id}_C \circ F \Rightarrow F$ (the left unitor) is equal to the morphism $\mathrm{eqToHom}$ constructed from the trivial equality $\mathrm{id}_C(F(X)) = F(X)$.

CategoryTheory.Cat.leftUnitor_inv_app theorem

{B C : Cat} (F : B ⟶ C) (X : B) : (λ_ F).inv.app X = eqToHom (by simp)

Full source

lemma leftUnitor_inv_app {B C : Cat} (F : B ⟶ C) (X : B) : (λ_ F).inv.app X = eqToHom (by simp) :=
  rfl

Component of Inverse Left Unitor in Category of Categories

Informal description

For any functor $F \colon B \to C$ between categories $B$ and $C$ in the category of categories $\mathrm{Cat}$, and for any object $X$ in $B$, the component at $X$ of the inverse of the left unitor natural isomorphism $\lambda_F^{-1}$ is equal to the morphism $\mathrm{eqToHom}$ (constructed from a trivial equality proof).

CategoryTheory.Cat.rightUnitor_hom_app theorem

{B C : Cat} (F : B ⟶ C) (X : B) : (ρ_ F).hom.app X = eqToHom (by simp)

Full source

lemma rightUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : B) : (ρ_ F).hom.app X = eqToHom (by simp) :=
  rfl

Component of Right Unitor Natural Transformation in Category of Categories

Informal description

For any functor $F \colon B \to C$ between categories $B$ and $C$ in $\mathrm{Cat}$, and for any object $X$ in $B$, the component of the right unitor natural transformation $\rho_F$ at $X$ is equal to the morphism induced by the equality proof (which simplifies to the identity morphism via the given simplification).

CategoryTheory.Cat.rightUnitor_inv_app theorem

{B C : Cat} (F : B ⟶ C) (X : B) : (ρ_ F).inv.app X = eqToHom (by simp)

Full source

lemma rightUnitor_inv_app {B C : Cat} (F : B ⟶ C) (X : B) : (ρ_ F).inv.app X = eqToHom (by simp) :=
  rfl

Component of Inverse Right Unitor in Category of Categories

Informal description

For any functor $F \colon B \to C$ between categories $B$ and $C$ in $\mathrm{Cat}$, and for any object $X$ in $B$, the component of the inverse right unitor natural transformation at $X$ is equal to the morphism induced by the trivial equality (via `eqToHom`), which simplifies to the identity morphism on $F(X)$.

CategoryTheory.Cat.associator_hom_app theorem

{B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : B) : (α_ F G H).hom.app X = eqToHom (by simp)

Full source

lemma associator_hom_app {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : B) :
    (α_ F G H).hom.app X = eqToHom (by simp) :=
  rfl

Component Formula for Associator Natural Isomorphism in Category of Categories

Informal description

For categories $B, C, D, E$ in $\mathrm{Cat}$, functors $F\colon B \to C$, $G\colon C \to D$, $H\colon D \to E$, and an object $X$ in $B$, the component of the associator natural isomorphism $(α_{F,G,H})_{\text{hom}}$ at $X$ is equal to the morphism induced by the equality proof (which simplifies to the identity via `simp`).

CategoryTheory.Cat.associator_inv_app theorem

{B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : B) : (α_ F G H).inv.app X = eqToHom (by simp)

Full source

lemma associator_inv_app {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : B) :
    (α_ F G H).inv.app X = eqToHom (by simp) :=
  rfl

Inverse Associator Component in $\mathrm{Cat}$ Equals Simplification-Induced Morphism

Informal description

For any categories $B$, $C$, $D$, and $E$ in the category of categories $\mathrm{Cat}$, and for any functors $F \colon B \to C$, $G \colon C \to D$, and $H \colon D \to E$, the component at an object $X$ of $B$ of the inverse associator $(α_{F,G,H})^{-1}$ is equal to the morphism induced by the equality obtained via simplification.

CategoryTheory.Cat.id_eq_id theorem

(X : Cat) : 𝟙 X = 𝟭 X

Full source

/-- The identity in the category of categories equals the identity functor. -/
theorem id_eq_id (X : Cat) : 𝟙 X = 𝟭 X := rfl

Identity Morphism Equals Identity Functor in $\mathrm{Cat}$

Informal description

For any category $X$ in the category of categories $\mathrm{Cat}$, the identity morphism $𝟙 X$ is equal to the identity functor $𝟭 X$.

CategoryTheory.Cat.comp_eq_comp theorem

{X Y Z : Cat} (F : X ⟶ Y) (G : Y ⟶ Z) : F ≫ G = F ⋙ G

Full source

/-- Composition in the category of categories equals functor composition. -/
theorem comp_eq_comp {X Y Z : Cat} (F : X ⟶ Y) (G : Y ⟶ Z) : F ≫ G = F ⋙ G := rfl

Composition in $\mathrm{Cat}$ Equals Functor Composition

Informal description

For any categories $X$, $Y$, and $Z$ in the category of categories $\mathrm{Cat}$, and for any functors $F \colon X \to Y$ and $G \colon Y \to Z$, the composition of morphisms $F \circ G$ in $\mathrm{Cat}$ is equal to the functor composition $F \circ G$ of the underlying functors.

CategoryTheory.Cat.of_α theorem

(C) [Category C] : (of C).α = C

Full source

@[simp] theorem of_α (C) [Category C] : (of C).α = C := rfl

Underlying Type Preservation in Category of Categories Construction

Informal description

For any category $C$, the underlying type of the object in the category of categories $\mathrm{Cat}$ constructed from $C$ via $\mathrm{Cat.of}$ is equal to $C$ itself, i.e., $(\mathrm{Cat.of}\, C).\alpha = C$.

CategoryTheory.Cat.coe_of theorem

(C : Cat.{v, u}) : Cat.of C = C

Full source

@[simp] theorem coe_of (C : CatCat.{v, u}) : Cat.of C = C := rfl

Identity of Category Construction in $\mathrm{Cat}$

Informal description

For any category $C$ in the category of categories $\mathrm{Cat}$, the construction $\mathrm{Cat.of}\, C$ is equal to $C$ itself.

CategoryTheory.Functor.toCatHom definition

{C D : Type u} [Category.{v} C] [Category.{v} D] (F : C ⥤ D) : Cat.of C ⟶ Cat.of D

Full source

/-- Functors between categories of the same size define arrows in `Cat`. -/
def toCatHom {C D : Type u} [Category.{v} C] [Category.{v} D] (F : C ⥤ D) :
    Cat.ofCat.of C ⟶ Cat.of D := F

Functor as morphism in the category of categories

Informal description

Given categories $C$ and $D$ and a functor $F : C \to D$, the function `toCatHom` maps $F$ to the corresponding morphism in the category of categories $\mathrm{Cat}$, where objects are categories and morphisms are functors.

CategoryTheory.Functor.ofCatHom definition

{C D : Type} [Category C] [Category D] (F : Cat.of C ⟶ Cat.of D) : C ⥤ D

Full source

/-- Arrows in `Cat` define functors. -/
def ofCatHom {C D : Type} [Category C] [Category D] (F : Cat.ofCat.of C ⟶ Cat.of D) : C ⥤ D := F

Functor corresponding to a morphism in the category of categories

Informal description

Given two categories $C$ and $D$ and a morphism $F$ in $\mathrm{Cat}$ from $\mathrm{Cat.of}\, C$ to $\mathrm{Cat.of}\, D$, the function $\mathrm{Functor.ofCatHom}$ constructs the corresponding functor from $C$ to $D$.

CategoryTheory.Functor.to_ofCatHom theorem

{C D : Type} [Category C] [Category D] (F : Cat.of C ⟶ Cat.of D) : (ofCatHom F).toCatHom = F

Full source

@[simp] theorem to_ofCatHom {C D : Type} [Category C] [Category D] (F : Cat.ofCat.of C ⟶ Cat.of D) :
    (ofCatHom F).toCatHom = F := rfl

Identity of Functor-Morphism Correspondence in the Category of Categories

Informal description

For any categories $C$ and $D$ and any morphism $F$ in $\mathrm{Cat}$ from $\mathrm{Cat.of}\, C$ to $\mathrm{Cat.of}\, D$, the composition of the functor corresponding to $F$ with the morphism construction in $\mathrm{Cat}$ yields $F$ itself. In other words, $(F.\mathrm{ofCatHom}).\mathrm{toCatHom} = F$.

CategoryTheory.Functor.of_toCatHom theorem

{C D : Type} [Category C] [Category D] (F : C ⥤ D) : ofCatHom (F.toCatHom) = F

Full source

@[simp] theorem of_toCatHom {C D : Type} [Category C] [Category D] (F : C ⥤ D) :
    ofCatHom (F.toCatHom) = F := rfl

Functor-Morphism Correspondence in the Category of Categories: $\mathrm{ofCatHom} \circ \mathrm{toCatHom} = \mathrm{id}$

Informal description

Given categories $C$ and $D$ and a functor $F : C \to D$, the composition of the morphism-to-functor construction `ofCatHom` with the functor-to-morphism construction `toCatHom` yields the original functor $F$, i.e., $\mathrm{ofCatHom}(\mathrm{toCatHom}(F)) = F$.

CategoryTheory.Cat.objects definition

: Cat.{v, u} ⥤ Type u

Full source

/-- Functor that gets the set of objects of a category. It is not
called `forget`, because it is not a faithful functor. -/
def objects : CatCat.{v, u}Cat.{v, u} ⥤ Type u where
  obj C := C
  map F := F.obj

-- Porting note: this instance was needed for CategoryTheory.Category.Cat.Limit

Objects functor for the category of categories

Informal description

The functor that maps a category $C$ in the category of categories $\mathrm{Cat}$ to its underlying type of objects, and a functor $F$ between categories to its object-level mapping function $F.\mathrm{obj}$.

CategoryTheory.Cat.instCategoryObjObjects instance

(X : Cat.{v, u}) : Category (objects.obj X)

Full source

instance (X : CatCat.{v, u}) : Category (objects.obj X) := (inferInstance : Category X)

Objects of a Category in Cat Form a Category

Informal description

For any category $X$ in the category of categories $\mathrm{Cat}$, the collection of objects of $X$ forms a category.

CategoryTheory.Cat.equivOfIso definition

{C D : Cat} (γ : C ≅ D) : C ≌ D

Full source

/-- Any isomorphism in `Cat` induces an equivalence of the underlying categories. -/
def equivOfIso {C D : Cat} (γ : C ≅ D) : C ≌ D where
  functor := γ.hom
  inverse := γ.inv
  unitIso := eqToIso <| Eq.symm γ.hom_inv_id
  counitIso := eqToIso γ.inv_hom_id

Equivalence from isomorphism in the category of categories

Informal description

Given an isomorphism $\gamma \colon C \cong D$ in the category $\mathrm{Cat}$ of categories, the function `equivOfIso` constructs an equivalence of categories $C \simeq D$. The equivalence consists of: - The functor $\gamma_{\text{hom}} \colon C \to D$ from the isomorphism $\gamma$, - Its inverse functor $\gamma_{\text{inv}} \colon D \to C$, - The unit isomorphism $\text{id}_C \cong \gamma_{\text{hom}} \circ \gamma_{\text{inv}}$ induced by the inverse identity $\gamma_{\text{hom}} \circ \gamma_{\text{inv}} = \text{id}_C$, - The counit isomorphism $\gamma_{\text{inv}} \circ \gamma_{\text{hom}} \cong \text{id}_D$ induced by the identity $\gamma_{\text{inv}} \circ \gamma_{\text{hom}} = \text{id}_D$.

CategoryTheory.typeToCat definition

: Type u ⥤ Cat

Full source

/-- Embedding `Type` into `Cat` as discrete categories.

This ought to be modelled as a 2-functor!
-/
@[simps]
def typeToCat : Type u ⥤ Cat where
  obj X := Cat.of (Discrete X)
  map := fun f => Discrete.functor (Discrete.mkDiscrete.mk ∘ f)
  map_id X := by
    apply Functor.ext
    · intro X Y f
      cases f
      simp only [id_eq, eqToHom_refl, Cat.id_map, Category.comp_id, Category.id_comp]
      apply ULift.ext
      aesop_cat
    · simp
  map_comp f g := by apply Functor.ext; aesop_cat

Embedding of types into categories as discrete categories

Informal description

The functor $\mathrm{typeToCat}$ embeds the category of types into the category of categories by sending a type $X$ to its discrete category $\mathrm{Discrete}\,X$, and a function $f \colon X \to Y$ to the functor $\mathrm{Discrete.functor}\,(\mathrm{Discrete.mk} \circ f) \colon \mathrm{Discrete}\,X \to \mathrm{Discrete}\,Y$.

CategoryTheory.instFaithfulCatTypeToCat instance

: Functor.Faithful typeToCat.{u}

Full source

instance : Functor.Faithful typeToCattypeToCat.{u} where
  map_injective {_X} {_Y} _f _g h :=
    funext fun x => congr_arg Discrete.as (Functor.congr_obj h ⟨x⟩)

Faithfulness of the Type-to-Category Embedding Functor

Informal description

The functor $\mathrm{typeToCat}$ from the category of types to the category of categories is faithful, meaning that for any two types $X$ and $Y$, the map on morphisms (functions) induced by $\mathrm{typeToCat}$ is injective. In other words, if two functions $f, g \colon X \to Y$ are sent to the same functor under $\mathrm{typeToCat}$, then $f = g$.

CategoryTheory.instFullCatTypeToCat instance

: Functor.Full typeToCat.{u}

Full source

instance : Functor.Full typeToCattypeToCat.{u} where
  map_surjective F := ⟨Discrete.as ∘ F.obj ∘ Discrete.mk, by
    apply Functor.ext
    · intro x y f
      dsimp
      apply ULift.ext
      aesop_cat
    · rintro ⟨x⟩
      apply Discrete.ext
      rfl⟩

Fullness of the Type-to-Category Embedding Functor

Informal description

The functor $\mathrm{typeToCat}$ from the category of types to the category of categories is full. That is, for any two types $X$ and $Y$, every functor between their corresponding discrete categories $\mathrm{Discrete}\,X$ and $\mathrm{Discrete}\,Y$ is induced by some function between $X$ and $Y$.

Implementation notes