{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Construction.Constant where

open import Level

open import Categories.Category
open import Categories.Category.Instance.One
open import Categories.Category.Product
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation using (NaturalTransformation)
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D : Category o ℓ e

const : (d : Category.Obj D) → Functor C D
const {D = D} d = record
  { F₀           = λ _ → d
  ; F₁           = λ _ → id
  ; identity     = refl
  ; homomorphism = sym identity²
  ; F-resp-≈     = λ _ → refl
  }
  where open Category D
        open Equiv

const! : (d : Category.Obj D) → Functor (One {0ℓ} {0ℓ} {0ℓ}) D
const! = const

constˡ : (c : Category.Obj C) → Functor D (Product C D)
constˡ c = const c ※ idF

constʳ : (c : Category.Obj C) → Functor D (Product D C)
constʳ c = idF ※ (const c)

constNat : ∀ {A B} → Category._⇒_ D A B → NaturalTransformation (const {D = D} {C = C} A) (const B)
constNat {D = D} f = record
  { η           = λ _ → f
  ; commute     = λ _ → MR.id-comm D
  ; sym-commute = λ _ → MR.id-comm-sym D
  }