------------------------------------------------------------------------ -- The Agda standard library -- -- Definitions for types of functions that only require an equality -- relation over the domain. ------------------------------------------------------------------------ -- The contents of this file should usually be accessed from `Function`. {-# OPTIONS --without-K --safe #-} open import Relation.Binary module Function.Definitions.Core1 {a ℓ₁} {A : Set a} (_≈₁_ : Rel A ℓ₁) where open import Level using (_⊔_) ------------------------------------------------------------------------ -- Definitions -- (Note the name `RightInverse` is used for the bundle) Inverseʳ : {b} {B : Set b} (A B) (B A) Set (a ℓ₁) Inverseʳ f g = x g (f x) ≈₁ x