------------------------------------------------------------------------
-- The Agda standard library
--
-- Order morphisms
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary.Core

module Relation.Binary.Morphism where

------------------------------------------------------------------------
-- Re-export contents of morphisms

open import Relation.Binary.Morphism.Definitions public
open import Relation.Binary.Morphism.Structures public