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.

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)

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)

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