Zulip Chat Archive

Stream: Is there code for X?

Topic: Category instance on Sigma type


view this post on Zulip 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).

view this post on Zulip Reid Barton (Aug 24 2020 at 22:57):

docs#category_theory.induced_category, nothing special for Sigma

view this post on Zulip 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