open import Cat.Instances.Discrete
open import Cat.Instances.Functor
open import Cat.Morphism
open import Cat.Bi.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Bi.Instances.Discrete {o β„“} (C : Precategory o β„“) where

Locally discrete bicategoriesπŸ”—

Let C\ca{C} be a precategory. We can define a prebicategory C\bf{C} by letting the hom-1-categories of C\bf{C} be the discrete categories on the Hom-sets of C\ca{C}.

{-# TERMINATING #-}
Locally-discrete : Prebicategory o β„“ β„“
Locally-discrete .Ob = C.Ob
Locally-discrete .Hom x y = Discβ€² (el (C.Hom x y) (C.Hom-set x y))
Locally-discrete .id = C.id
Locally-discrete .compose .Fβ‚€ (f , g) = f C.∘ g
Locally-discrete .compose .F₁ (p , q) = apβ‚‚ C._∘_ p q
Locally-discrete .compose .F-id = refl
Locally-discrete .compose .F-∘ f g = C.Hom-set _ _ _ _ _ _
Locally-discrete .unitor-l = to-natural-iso ni where
  ni : make-natural-iso _ _
  ni .make-natural-iso.eta x = sym (C.idl x)
  ni .make-natural-iso.inv x = C.idl x
  ni .make-natural-iso.eta∘inv x = βˆ™-inv-r (C.idl x)
  ni .make-natural-iso.inv∘eta x = βˆ™-inv-l (C.idl x)
  ni .make-natural-iso.natural x y f = C.Hom-set _ _ _ _ _ _
Locally-discrete .unitor-r = to-natural-iso ni where
  ni : make-natural-iso _ _
  ni .make-natural-iso.eta x = sym (C.idr x)
  ni .make-natural-iso.inv x = C.idr x
  ni .make-natural-iso.eta∘inv x = βˆ™-inv-r (C.idr x)
  ni .make-natural-iso.inv∘eta x = βˆ™-inv-l (C.idr x)
  ni .make-natural-iso.natural x y f = C.Hom-set _ _ _ _ _ _
Locally-discrete .associator = to-natural-iso ni where
  ni : make-natural-iso _ _
  ni .make-natural-iso.eta x = sym (C.assoc _ _ _)
  ni .make-natural-iso.inv x = C.assoc _ _ _
  ni .make-natural-iso.eta∘inv x = βˆ™-inv-r (C.assoc _ _ _)
  ni .make-natural-iso.inv∘eta x = βˆ™-inv-l (C.assoc _ _ _)
  ni .make-natural-iso.natural x y f = C.Hom-set _ _ _ _ _ _
Locally-discrete .triangle f g = C.Hom-set _ _ _ _ _ _
Locally-discrete .pentagon f g h i = C.Hom-set _ _ _ _ _ _