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

module Categories.Bicategory.Object.Terminal {o  e t} (𝒞 : Bicategory o  e t) where

open Bicategory 𝒞
open import Level
open import Categories.Category using (_[_,_])
open import Categories.Morphism.HeterogeneousEquality using (Along_,_[_≈_])
open import Categories.Morphism.Notation using (_[_≅_])
open import Categories.Morphism using (_≅_)

record IsTerminal ( : Obj) : Set (o    e  t) where
  field
    !₁ : {A : Obj}  (A ⇒₁ )
    !₂ : {A : Obj}  !₁ {A} ⇒₂ !₁

    η₁ :  {A} f  hom A  [ f  !₁ ]
    η₂ :  {A}{f g}(α : hom A  [ f , g ])
        Along η₁ _ , η₁ _ [ α  !₂ ]