------------------------------------------------------------------------ -- The Agda standard library -- -- Bundles for types of functions ------------------------------------------------------------------------ -- The contents of this file should usually be accessed from `Function`. -- Note that these bundles differ from those found elsewhere in other -- library hierarchies as they take Setoids as parameters. This is -- because a function is of no use without knowing what its domain and -- codomain is, as well which equalities are being considered over them. -- One consequence of this is that they are not built from the -- definitions found in `Function.Structures` as is usually the case in -- other library hierarchies, as this would duplicate the equality -- axioms. {-# OPTIONS --cubical-compatible --safe #-} module Function.Dependent.Bundles where open import Level using (Level; _⊔_) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid) private variable a b ℓ₁ ℓ₂ : Level ------------------------------------------------------------------------ -- Setoid bundles ------------------------------------------------------------------------ module _ (From : Setoid a ℓ₁) (To : IndexedSetoid (Setoid.Carrier From) b ℓ₂) where open Setoid From using () renaming (Carrier to A; _≈_ to _≈₁_) open IndexedSetoid To using () renaming (Carrier to B; _≈_ to _≈₂_) ------------------------------------------------------------------------ -- Bundles with one element -- Called `Func` rather than `Function` in order to avoid clashing -- with the top-level module. record Func : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : (x : A) → B x cong : ∀ {x y} → x ≈₁ y → to x ≈₂ to y