Theorems · Inductive type · category theory

CategoryTheory.InducedCategory.Hom

{C : Type u₁} →
  {D : Type u₂} →
    [CategoryTheory.Category.{v, u₂} D] →
      {F : C → D} → CategoryTheory.InducedCategory D F → CategoryTheory.InducedCategory D F → Type v

The type of morphisms in InducedCategory D F between X and Y is a 1-field structure which identifies to F X ⟶ F Y.

Defined in

Mathlib.CategoryTheory.InducedCategory

Cited by

12 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CategoryTheory.Category