{-# OPTIONS --without-K --safe #-}
 
{-
  Useful notation for Epimorphisms, Mononmorphisms, and isomorphisms
-}
module Categories.Morphism.Notation where
 
open import Level
 
open import Categories.Category.Core
open import Categories.Morphism
 
private
  variable
    o ℓ e : Level
 
_[_↣_] : (𝒞 : Category o ℓ e) → (A B : Category.Obj 𝒞) → Set (o ⊔ ℓ ⊔ e)
𝒞 [ A ↣ B ] = _↣_ 𝒞 A B
 
_[_↠_] : (𝒞 : Category o ℓ e) → (A B : Category.Obj 𝒞) → Set (o ⊔ ℓ ⊔ e)
𝒞 [ A ↠ B ] = _↠_ 𝒞 A B
 
_[_≅_] : (𝒞 : Category o ℓ e) → (A B : Category.Obj 𝒞) → Set (ℓ ⊔ e)
𝒞 [ A ≅ B ] = _≅_ 𝒞 A B