# mathlibdocumentation

category_theory.punit

# The category discrete punit#

We define star : C ⥤ discrete punit sending everything to punit.star, show that any two functors to discrete punit are naturally isomorphic, and construct the equivalence (discrete punit ⥤ C) ≌ C.

def category_theory.functor.star (C : Type u)  :

The constant functor sending everything to punit.star.

Equations
def category_theory.functor.punit_ext {C : Type u} (F G : C ) :
F G

Any two functors to discrete punit are isomorphic.

Equations
theorem category_theory.functor.punit_ext' {C : Type u} (F G : C ) :
F = G

Any two functors to discrete punit are equal. You probably want to use punit_ext instead of this.

def category_theory.functor.from_punit {C : Type u} (X : C) :

The functor from discrete punit sending everything to the given object.

@[simp]
@[simp]
theorem category_theory.functor.equiv_unit_iso {C : Type u}  :
@[simp]
theorem category_theory.functor.equiv_functor_map {C : Type u} (F G : C) (θ : F G) :
@[simp]
theorem category_theory.functor.equiv_counit_iso {C : Type u}  :
category_theory.functor.equiv.counit_iso = category_theory.functor.equiv._proof_4
def category_theory.functor.equiv {C : Type u}  :

Functors from discrete punit are equivalent to the category itself.

Equations
@[simp]