1234567891011121314151617-------------------------------------------------------------------------- The Agda standard library---- Heterogeneously-indexed binary relations------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Relation.Binary.Indexed.Heterogeneous where -------------------------------------------------------------------------- Publicly export core definitions open import Relation.Binary.Indexed.Heterogeneous.Core publicopen import Relation.Binary.Indexed.Heterogeneous.Definitions publicopen import Relation.Binary.Indexed.Heterogeneous.Structures publicopen import Relation.Binary.Indexed.Heterogeneous.Bundles public