## Stream: Is there code for X?

### Topic: Category instance on Sigma type

#### Adam Topaz (Aug 24 2020 at 22:43):

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 (Aug 24 2020 at 22:57):

docs#category_theory.induced_category, nothing special for Sigma

#### Adam Topaz (Aug 24 2020 at 23:06):

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

Last updated: May 17 2021 at 16:26 UTC