{-# OPTIONS --without-K --safe #-}

open import Level

module Categories.Category.Instance.One where

open import Data.Unit using (⊤; tt)

open import Categories.Category
open import Categories.Functor
open import Categories.Category.Instance.Cats
import Categories.Object.Terminal as Term

module _ {o ℓ e : Level} where
  open Term (Cats o ℓ e)

  One : Category o ℓ e
  One = record
    { Obj       = Lift o ⊤
    ; _⇒_       = λ _ _ → Lift ℓ ⊤
    ; _≈_       = λ _ _ → Lift e ⊤
    }

  One-⊤ : Terminal
  One-⊤ = record { ⊤ = One ; ⊤-is-terminal = record { ! = record { F₀ = λ _ → lift tt } } }

-- not only is One terminal, it can be shifted anywhere else. Stronger version of !
shift : {o ℓ e : Level} (o′ ℓ′ e′ : Level) → Functor (One {o} {ℓ} {e}) (One {o′} {ℓ′} {e′})
shift o′ ℓ′ e′ = _ -- so obvious, Agda can fill it all in automatically!

One0 : Category 0ℓ 0ℓ 0ℓ
One0 = One {0ℓ} {0ℓ} {0ℓ}