Theorems · Definition · category theory

CategoryTheory.EnrichedFunctor.mk.noConfusion

{V : Type v} →
  {inst : CategoryTheory.Category.{w, v} V} →
    {inst_1 : CategoryTheory.MonoidalCategory V} →
      {C : Type u₁} →
        {inst_2 : CategoryTheory.EnrichedCategory V C} →
          {D : Type u₂} →
            {inst_3 : CategoryTheory.EnrichedCategory V D} →
              {P : Sort u} →
                {obj : C → D} →
                  {map : (X Y : C) → (X ⟶[V] Y) ⟶ obj X ⟶[V] obj Y} →
                    {map_id :
                        autoParam
                          (∀ (X : C),
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map X X) =
                              CategoryTheory.eId V (obj X))
                          CategoryTheory.EnrichedFunctor.map_id._autoParam} →
                      {map_comp :
                          autoParam
                            (∀ (X Y Z : C),
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map X Z) =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.tensorHom (map X Y) (map Y Z))
                                  (CategoryTheory.eComp V (obj X) (obj Y) (obj Z)))
                            CategoryTheory.EnrichedFunctor.map_comp._autoParam} →
                        {obj' : C → D} →
                          {map' : (X Y : C) → (X ⟶[V] Y) ⟶ obj' X ⟶[V] obj' Y} →
                            {map_id' :
                                autoParam
                                  (∀ (X : C),
                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map' X X) =
                                      CategoryTheory.eId V (obj' X))
                                  CategoryTheory.EnrichedFunctor.map_id._autoParam} →
                              {map_comp' :
                                  autoParam
                                    (∀ (X Y Z : C),
                                      CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map' X Z) =
                                        CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategoryStruct.tensorHom (map' X Y) (map' Y Z))
                                          (CategoryTheory.eComp V (obj' X) (obj' Y) (obj' Z)))
                                    CategoryTheory.EnrichedFunctor.map_comp._autoParam} →
                                { obj := obj, map := map, map_id := map_id, map_comp := map_comp } =
                                    { obj := obj', map := map', map_id := map_id', map_comp := map_comp' } →
                                  (obj ≍ obj' → map ≍ map' → P) → P

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms