Theorems · Theorem · category theory

CategoryTheory.WithInitial.ofCommaMorphism_app

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {c c' :
    CategoryTheory.Comma (CategoryTheory.Functor.const C) (CategoryTheory.Functor.id (CategoryTheory.Functor C D))}
  (φ : c ⟶ c') (x : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.ofCommaMorphism φ).app x =
    match x with
    | CategoryTheory.WithInitial.of x => φ.right.app x
    | CategoryTheory.WithInitial.star => φ.left

Defined in

Mathlib.CategoryTheory.WithTerminal.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category