Theorems · Inductive type · category theory

CategoryTheory.BasedNatTrans

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

A BasedNatTrans between two BasedFunctors is a natural transformation α between the underlying functors, such that for all a : 𝒳, α.app a lifts 𝟙 S whenever 𝒳.p.obj a = S.

Defined in

Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Cited by

11 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category