Theorems · Inductive type · category theory

CategoryTheory.BasedFunctor

{𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    CategoryTheory.BasedCategory 𝒮 → CategoryTheory.BasedCategory 𝒮 → Type (max (max (max u₂ u₃) v₂) v₃)

A functor between based categories is a functor between the underlying categories that commutes with the projections.

Defined in

Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Cited by

34 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Category