Theorems · Theorem · category theory

CategoryTheory.Functor.isTerminalConst_from_app

∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {X : D} (hX : CategoryTheory.Limits.IsTerminal X)
  (F : CategoryTheory.Functor C D) (Y : C),
  ((CategoryTheory.Functor.isTerminalConst C hX).from F).app Y = hX.from (F.obj Y)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category