Category instance on Sigma type

Stream: Is there code for X?

[Adam Topaz]

I'm looking for a category instance on a Sigma type given a category instance on the base... something like this:

import category_theory.category

open category_theory

variables {C : Type*} [category C] (T : C → Type*)

example : category (Σ (X : C), T X) :=
{ hom := λ X Y, X.fst ⟶ Y.fst,
  id := λ _, 𝟙 _,
  comp := λ _ _ _ f g, f ≫ g }

Does mathlib have something like this? (apply_instance does not work).

[Reid Barton]

docs#category_theory.induced_category, nothing special for Sigma

[Adam Topaz]

Thanks! (I probably should have looked at the definition of the full subcategory, which uses this :smiling_face:️)