-- Discrete category over a type A
-- A must be an h-groupoid for the homs to be sets

module Cubical.Categories.Instances.Discrete where

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Functor.Base
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Transport

private
  variable
     ℓC ℓC' : Level

open Category

-- Discrete category
DiscreteCategory : hGroupoid   Category  
DiscreteCategory A .ob = A .fst
DiscreteCategory A .Hom[_,_] a a' = a  a'
DiscreteCategory A .id = refl
DiscreteCategory A ._⋆_ = _∙_
DiscreteCategory A .⋆IdL f = sym (lUnit f)
DiscreteCategory A .⋆IdR f = sym (rUnit f)
DiscreteCategory A .⋆Assoc f g h = sym (assoc f g h)
DiscreteCategory A .isSetHom {x} {y} = A .snd x y


module _ {A : hGroupoid }
         {C : Category ℓC ℓC'} where
  open Functor

  -- Functions f: A → ob C give functors F: DiscreteCategory A → C
  DiscFunc : (fst A  ob C)  Functor (DiscreteCategory A) C
  DiscFunc f .F-ob = f
  DiscFunc f .F-hom {x} p = subst  z  C [ f x , f z ]) p (id C)
  DiscFunc f .F-id {x} = substRefl {B = λ z  C [ f x , f z ]} (id C)

  -- Preserves composition
  DiscFunc f .F-seq {x} {y} p q =
      let open Category C using () renaming (_⋆_ to _●_) in

      let Hom[fx,f—] =  (w : A .fst)  C [ f x , f w ]) in
      let Hom[fy,f—] =  (w : A .fst)  C [ f y , f w ]) in
      let id-fx = id C {f x} in
      let id-fy = id C {f y} in
      let Fp = (subst Hom[fx,f—] (p) id-fx) in

      subst Hom[fx,f—] (p  q) id-fx            ≡⟨ substComposite Hom[fx,f—] _ _ _ 
      subst Hom[fx,f—] (q) (Fp)                 ≡⟨ cong (subst _ q) (sym (⋆IdR C _)) 
      subst Hom[fx,f—] (q) (Fp  id-fy)         ≡⟨ substCommSlice _ _  _  Fp ●_) q _ 
      Fp  (subst Hom[fy,f—] (q) id-fy)