module Cat.Bi.Instances.Terminal where

The terminal bicategory🔗

The terminal bicategory is the bicategory with a single object, and a trivial category of morphisms.

open Prebicategory

⊤Bicat : Prebicategory lzero lzero lzero
⊤Bicat .Ob = 
⊤Bicat .Hom _ _ = ⊤Cat
⊤Bicat .Prebicategory.id = tt
⊤Bicat .compose = !F
⊤Bicat .unitor-l = path→iso !F-unique₂
⊤Bicat .unitor-r = path→iso !F-unique₂
⊤Bicat .associator = path→iso !F-unique₂
⊤Bicat .triangle _ _ = refl
⊤Bicat .pentagon _ _ _ _ = refl