Theorems · Definition · category theory

CategoryTheory.over

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X S : C) → autoParam (CategoryTheory.OverClass X S) CategoryTheory.over._auto_1 → (X ⟶ S)

The structure morphism X ↘ S : X ⟶ S given OverClass X S. The instance argument is an optParam instead so that it appears in the discrimination tree.

Defined in

Mathlib.CategoryTheory.Comma.Over.OverClass

Cited by

76 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

CategoryTheory.Category