open import Cat.Instances.Shape.Terminal
open import Cat.Functor.Naturality
open import Cat.Functor.Compose
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

module Cat.Functor.Constant where


# Constant functorsπ

A constant functor is a functor that sends every object of to a single object and every morphism of to the identity morphism.

module _
{o β o' β'}
{C : Precategory o β} {D : Precategory o' β'}
where
private
module C = Cat.Reasoning C
module D = Cat.Reasoning D
open Functor
open _=>_


Equivalently, constant functors are factorizations through the terminal category. We opt to take this notion as primitive for ergonomic reasons: it is useful to only be able to write constant functors in a single way.

  Const : D.Ob β Functor C D
Const X = !Const X Fβ !F


Natural transformations between constant functors are given by a single morphism, and natural isomorphisms by a single iso.

  constβΏ
: {X Y : D.Ob}
β D.Hom X Y
β Const X => Const Y
constβΏ f = !constβΏ f β !F

const-isoβΏ
: {X Y : D.Ob}
β X D.β Y
β Const X ββΏ Const Y
const-isoβΏ f =
isoβisoβΏ (Ξ» _ β f) (Ξ» f β D.id-comm-sym)

  -- Coherence lemmas for cones and cocones as natural transformations.
to-coconeβΏ
: β {F : Functor C D} {K : Functor β€Cat D}
β F => K Fβ !F
β F => Const (K .Fβ tt)
to-coconeβΏ {K = K} Ο .Ξ· = Ο .Ξ·
to-coconeβΏ {K = K} Ο .is-natural x y f =
Ο .is-natural x y f β apβ D._β_ (K .F-id) refl

to-coneβΏ
: β {F : Functor C D} {K : Functor β€Cat D}
β K Fβ !F => F
β Const (K .Fβ tt) => F
to-coneβΏ {K = K} Ο .Ξ· = Ο .Ξ·
to-coneβΏ {K = K} Ο .is-natural x y f =
apβ D._β_ refl (sym (K .F-id)) β Ο .is-natural x y f


## Essentially constant functorsπ

A functor is essentially constant if it is (merely) isomorphic to a constant functor.

  is-essentially-constant : Functor C D β Type _
is-essentially-constant F = β[ X β D.Ob ] (F ββΏ Const X)

module _
{ob βb oc βc od βd}
{B : Precategory ob βb}
{C : Precategory oc βc}
{D : Precategory od βd}
(F : Functor C D) (G : Functor B C)
where
private
module D = Cat.Reasoning D
module F = Cat.Functor.Reasoning F
module G = Cat.Functor.Reasoning G

open IsoβΏ
open _=>_


Essentially constant functors are closed under pre and postcomposition by arbitrary functors.

  essentially-constant-βl
: is-essentially-constant F
β is-essentially-constant (F Fβ G)
essentially-constant-βl =
rec! Ξ» d f β
pure $d , isoβisoβΏ (Ξ» b β isoβΏβiso f (G.β b)) (Ξ» g β sym (f .to .is-natural _ _ (G.β g))) essentially-constant-βr : is-essentially-constant G β is-essentially-constant (F Fβ G) essentially-constant-βr = rec! Ξ» c f β pure$ F.β c ,
isoβisoβΏ
(Ξ» b β F-map-iso F (isoβΏβiso f b))
(Ξ» g β
apβ D._β_ (sym (F.F-id)) refl
β F.weave (sym (f .to .is-natural _ _ g)))