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)))