Theorems · Definition · category theory

CategoryTheory.Limits.BinaryFan.fst

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (s : CategoryTheory.Limits.BinaryFan X Y) →
        ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj
            { as := CategoryTheory.Limits.WalkingPair.left } ⟶
          (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }

The first projection of a binary fan.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Cited by

53 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category