Codiscrete categories #
We define Codiscrete A
as an alias for the type A
,
and use this type alias to provide a Category
instance
whose Hom type are Unit types.
Codiscrete.functor
promotes a function f : C → A
(for any category C
) to a functor
f : C ⥤ Codiscrete A
.
Similarly, Codiscrete.natTrans
and Codiscrete.natIso
promote I
-indexed families of morphisms,
or I
-indexed families of isomorphisms to natural transformations or natural isomorphism.
We define functorToCat : Type u ⥤ Cat.{0,u}
which sends a type to the codiscrete category and show
it is right adjoint to Cat.objects.
A wrapper for promoting any type to a category, with a unique morphisms between any two objects of the category.
- as : α
A wrapper for promoting any type to a category, with a unique morphisms between any two objects of the category.
Instances For
Codiscrete α
is equivalent to the original type α
.
Equations
- CategoryTheory.codiscreteEquiv = { toFun := CategoryTheory.Codiscrete.as, invFun := CategoryTheory.Codiscrete.mk, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- CategoryTheory.instDecidableEqCodiscrete = CategoryTheory.codiscreteEquiv.decidableEq
Equations
Any function C → A
lifts to a functor C ⥤ Codiscrete A
.
Equations
- CategoryTheory.Codiscrete.functor F = { obj := CategoryTheory.Codiscrete.mk ∘ F, map := fun {X Y : C} (x : X ⟶ Y) => PUnit.unit, map_id := ⋯, map_comp := ⋯ }
Instances For
The underlying function C → A
of a functor C ⥤ Codiscrete A
.
Equations
- CategoryTheory.Codiscrete.invFunctor F = CategoryTheory.Codiscrete.as ∘ F.obj
Instances For
Given two functors to a codiscrete category, there is a trivial natural transformation.
Equations
- CategoryTheory.Codiscrete.natTrans = { app := fun (x : C) => PUnit.unit, naturality := ⋯ }
Instances For
Given two functors into a codiscrete category, the trivial natural transformation is an natural isomorphism.
Equations
- CategoryTheory.Codiscrete.natIso = { hom := CategoryTheory.Codiscrete.natTrans, inv := CategoryTheory.Codiscrete.natTrans, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Every functor F
to a codiscrete category is naturally isomorphic {(actually, equal)} to
Codiscrete.as ∘ F.obj
.
Equations
- CategoryTheory.Codiscrete.natIsoFunctor = CategoryTheory.Iso.refl F
Instances For
A function induces a functor between codiscrete categories.
Equations
- CategoryTheory.Codiscrete.functorOfFun f = CategoryTheory.Codiscrete.functor (f ∘ CategoryTheory.Codiscrete.as)
Instances For
A codiscrete category is equivalent to its opposite category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Codiscrete.functorToCat
turns a type into a codiscrete category
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a category C
and type A
, there is an equivalence between functions objects.obj C ⟶ A
and functors C ⥤ Codiscrete A
.
Equations
- CategoryTheory.Codiscrete.equivFunctorToCodiscrete = { toFun := CategoryTheory.Codiscrete.functor, invFun := CategoryTheory.Codiscrete.invFunctor, left_inv := ⋯, right_inv := ⋯ }
Instances For
The functor that turns a type into a codiscrete category is right adjoint to the objects functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Components of the unit of the adjunction Cat.objects ⊣ Codiscrete.functorToCat
.
Instances For
Components of the counit of the adjunction Cat.objects ⊣ Codiscrete.functorToCat
Equations
- CategoryTheory.Codiscrete.counitApp A = CategoryTheory.Codiscrete.as
Instances For
Left triangle equality of the adjunction Cat.objects ⊣ Codiscrete.functorToCat
,
as a universe polymorphic statement.
Right triangle equality of the adjunction Cat.objects ⊣ Codiscrete.functorToCat
,
stated using a composition of functors.