123456789101112131415161718-------------------------------------------------------------------------- The Agda standard library---- Order morphisms------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Core module Relation.Binary.Morphism where -------------------------------------------------------------------------- Re-export contents of morphisms open import Relation.Binary.Morphism.Definitions publicopen import Relation.Binary.Morphism.Structures publicopen import Relation.Binary.Morphism.Bundles public