Theorems · Theorem · category theory

CategoryTheory.StrictlyUnitaryLaxFunctor.mk.sizeOf_spec

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : SizeOf B] [inst_3 : SizeOf C] (toLaxFunctor : CategoryTheory.LaxFunctor B C)
  (map_id :
    autoParam
      (∀ (X : B),
        toLaxFunctor.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (toLaxFunctor.obj X))
      CategoryTheory.StrictlyUnitaryLaxFunctor.map_id._autoParam)
  (mapId_eq_eqToHom :
    autoParam (∀ (X : B), toLaxFunctor.mapId X = CategoryTheory.eqToHom ⋯)
      CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom._autoParam),
  sizeOf { toLaxFunctor := toLaxFunctor, map_id := map_id, mapId_eq_eqToHom := mapId_eq_eqToHom } =
    1 + sizeOf toLaxFunctor

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.BicategorySizeOfSizeOf