Theorems · Definition · category theory

CategoryTheory.Comma.equivProd

{A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) →
          (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) → CategoryTheory.Comma L R ≌ A × B

Taking the comma category of two functors into Discrete PUnit results in something is equivalent to their product.

Defined in

Mathlib.CategoryTheory.Comma.Basic

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category