Theorems · Definition · category theory

CategoryTheory.Functor.sectionsEquivHom

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor C (Type u₂)) →
      (X : Type u₂) → [Unique X] → ↑F.sections ≃ ((CategoryTheory.Functor.const C).obj X ⟶ F)

A type-level equivalence between sections of a functor and morphisms from a terminal functor to it. We use the constant functor on a given singleton type here as a specific choice of terminal functor.

Defined in

Mathlib.CategoryTheory.Yoneda

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryUnique