Theorems · Definition · category theory

CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse

{T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D T) →
          (Y : T) →
            (X : D) →
              CategoryTheory.Functor (CategoryTheory.StructuredArrow Y ((CategoryTheory.Under.forget X).comp F))
                (CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F))

The inverse functor of ofStructuredArrowProjEquivalence.functor.

Defined in

Mathlib.CategoryTheory.Comma.Over.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category