Disjoint union of categories #
We define the category structure on a sigma-type (disjoint union) of categories.
- mk: {I : Type w₁} → {C : I → Type u₁} → [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] → {i : I} → {X Y : C i} → (X ⟶ Y) → CategoryTheory.Sigma.SigmaHom { fst := i, snd := X } { fst := i, snd := Y }
The type of morphisms of a disjoint union of categories: for X : C i
and Y : C j
, a morphism
(i, X) ⟶ (j, Y)
if i = j
is just a morphism X ⟶ Y
, and if i ≠ j
there are no such morphisms.
Instances For
The identity morphism on an object.
Instances For
Composition of sigma homomorphisms.
Instances For
The inclusion functor into the disjoint union of categories.
Instances For
To build a natural transformation over the sigma category, it suffices to specify it restricted to each subcategory.
Instances For
(Implementation). An auxiliary definition to build the functor desc
.
Instances For
Given a collection of functors F i : C i ⥤ D
, we can produce a functor (Σ i, C i) ⥤ D
.
The produced functor desc F
satisfies: incl i ⋙ desc F ≅ F i
, i.e. restricted to just the
subcategory C i
, desc F
agrees with F i
, and it is unique (up to natural isomorphism) with
this property.
This witnesses that the sigma-type is the coproduct in Cat.
Instances For
This shows that when desc F
is restricted to just the subcategory C i
, desc F
agrees with
F i
.
Instances For
If q
when restricted to each subcategory C i
agrees with F i
, then q
is isomorphic to
desc F
.
Instances For
If q₁
and q₂
when restricted to each subcategory C i
agree, then q₁
and q₂
are isomorphic.
Instances For
A function J → I
induces a functor Σ j, C (g j) ⥤ Σ i, C i
.
Instances For
The functor Sigma.map C g
restricted to the subcategory C j
acts as the inclusion of g j
.
Instances For
The functor Sigma.map
applied to the identity function is just the identity functor.
Instances For
The functor Sigma.map
applied to a composition is a composition of functors.
Instances For
Assemble an I
-indexed family of functors into a functor between the sigma types.
Instances For
Assemble an I
-indexed family of natural transformations into a single natural transformation.