# Pointed endofunctors on categories

Content created by Egbert Rijke.

Created on 2024-02-08.

module category-theory.pointed-endofunctors-categories where

Imports
open import category-theory.categories
open import category-theory.functors-categories
open import category-theory.natural-transformations-functors-categories
open import category-theory.pointed-endofunctors-precategories

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels


## Idea

An endofunctor F : C → C on a category C is said to be pointed if it comes equipped with a natural transformation id ⇒ F from the identity functor to F.

More explicitly, a pointing of an endofunctor F : C → C consists of a family of morphisms η X : X → F X such that for each morphism f : X → Y in C the diagram

       η X
X -----> F X
|         |
f |         | F f
∨         ∨
Y -----> F Y
η Y


## Definitions

### The structure of a pointing on an endofunctor on a category

module _
{l1 l2 : Level} (C : Category l1 l2) (T : functor-Category C C)
where

pointing-endofunctor-Category : UU (l1 ⊔ l2)
pointing-endofunctor-Category =
pointing-endofunctor-Precategory (precategory-Category C) T


### Pointed endofunctors on a category

module _
{l1 l2 : Level} (C : Category l1 l2)
where

pointed-endofunctor-Category : UU (l1 ⊔ l2)
pointed-endofunctor-Category =
pointed-endofunctor-Precategory (precategory-Category C)

module _
(F : pointed-endofunctor-Category)
where

functor-pointed-endofunctor-Category :
functor-Category C C
functor-pointed-endofunctor-Category =
functor-pointed-endofunctor-Precategory (precategory-Category C) F

obj-pointed-endofunctor-Category : obj-Category C → obj-Category C
obj-pointed-endofunctor-Category =
obj-pointed-endofunctor-Precategory (precategory-Category C) F

hom-pointed-endofunctor-Category :
{X Y : obj-Category C} →
hom-Category C X Y →
hom-Category C
( obj-pointed-endofunctor-Category X)
( obj-pointed-endofunctor-Category Y)
hom-pointed-endofunctor-Category =
hom-pointed-endofunctor-Precategory (precategory-Category C) F

preserves-id-pointed-endofunctor-Category :
(X : obj-Category C) →
hom-pointed-endofunctor-Category (id-hom-Category C {X}) ＝
id-hom-Category C
preserves-id-pointed-endofunctor-Category =
preserves-id-pointed-endofunctor-Precategory (precategory-Category C) F

preserves-comp-pointed-endofunctor-Category :
{X Y Z : obj-Category C}
(g : hom-Category C Y Z) (f : hom-Category C X Y) →
hom-pointed-endofunctor-Category
( comp-hom-Category C g f) ＝
comp-hom-Category C
( hom-pointed-endofunctor-Category g)
( hom-pointed-endofunctor-Category f)
preserves-comp-pointed-endofunctor-Category =
preserves-comp-pointed-endofunctor-Precategory (precategory-Category C) F

pointing-pointed-endofunctor-Category :
natural-transformation-Category C C
( id-functor-Category C)
( functor-pointed-endofunctor-Category)
pointing-pointed-endofunctor-Category =
pointing-pointed-endofunctor-Precategory (precategory-Category C) F

hom-family-pointing-pointed-endofunctor-Category :
hom-family-functor-Category C C
( id-functor-Category C)
( functor-pointed-endofunctor-Category)
hom-family-pointing-pointed-endofunctor-Category =
hom-family-pointing-pointed-endofunctor-Precategory
( precategory-Category C)
( F)

naturality-pointing-pointed-endofunctor-Category :
is-natural-transformation-Category C C
( id-functor-Category C)
( functor-pointed-endofunctor-Category)
( hom-family-pointing-pointed-endofunctor-Category)
naturality-pointing-pointed-endofunctor-Category =
naturality-pointing-pointed-endofunctor-Precategory
( precategory-Category C) F