Theorems · Definition · category theory

CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso

(C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u_2} →
      (j : J) →
        (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.comp
            ((CategoryTheory.evaluation (CategoryTheory.Discrete J) C).obj { as := j }) ≅
          CategoryTheory.Pi.eval (fun a => C) j

piEquivalenceFunctorDiscrete is compatible with evaluation.

Defined in

Mathlib.CategoryTheory.Discrete.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category