Theorems · Definition · category theory

CategoryTheory.Over.postCongr

{T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : T} →
          {F G : CategoryTheory.Functor T D} →
            (e : F ≅ G) →
              (CategoryTheory.Over.post F).comp (CategoryTheory.Over.map (e.hom.app X)) ≅ CategoryTheory.Over.post G

If F and G are naturally isomorphic, then Over.post F and Over.post G are also naturally isomorphic up to Over.map

Defined in

Mathlib.CategoryTheory.Comma.Over.Basic

Cited by

2 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category