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