{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core using (Category)

-- You can transform functions out of discrete
-- categories into functors.
module Categories.Functor.Construction.FromDiscrete {o β„“ e} (π’ž : Category o β„“ e) where

open import Relation.Binary.PropositionalEquality.Core as ≑

open import Categories.Category.Construction.StrictDiscrete using (Discrete)
open import Categories.Functor.Core using (Functor)

open Category π’ž
open Equiv

FromDiscrete : βˆ€ {o} {A : Set o} β†’ (A β†’ Obj) β†’ Functor (Discrete A) π’ž
FromDiscrete {o} {A = A} select = record
  { Fβ‚€ = select
  ; F₁ = Ξ» { ≑.refl β†’ id }
  ; identity = Equiv.refl
  ; homomorphism = Ξ» { {_} {_} {_} {≑.refl} {≑.refl} β†’ Equiv.sym identityΒ² }
  ; F-resp-β‰ˆ = Ξ» { ≑.refl β†’ Equiv.refl }
  }