------------------------------------------------------------------------
-- The Agda standard library
--
-- Several kinds of "relatedness" for containers such as equivalences,
-- surjections and bijections
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Container.Related where
open import Data.Container.Core using (Container; ⟦_⟧)
open import Data.Container.Membership using (_∈_)
import Function.Related.Propositional as Related
open import Level using (_⊔_)
open import Relation.Binary.Bundles using (Preorder; Setoid)
open Related public
using (Kind; SymmetricKind)
renaming ( implication to subset
; reverseImplication to superset
; equivalence to set
; injection to subbag
; reverseInjection to superbag
; bijection to bag
)
[_]-Order : ∀ {s p ℓ} → Kind → Container s p → Set ℓ →
Preorder (s ⊔ p ⊔ ℓ) (s ⊔ p ⊔ ℓ) (p ⊔ ℓ)
[ k ]-Order C X = Related.InducedPreorder₂ k (_∈_ {C = C} {X = X})
[_]-Equality : ∀ {s p ℓ} → SymmetricKind → Container s p → Set ℓ →
Setoid (s ⊔ p ⊔ ℓ) (p ⊔ ℓ)
[ k ]-Equality C X = Related.InducedEquivalence₂ k (_∈_ {C = C} {X = X})
infix 4 _≲[_]_
_≲[_]_ : ∀ {s p x} {C : Container s p} {X : Set x} →
⟦ C ⟧ X → Kind → ⟦ C ⟧ X → Set (p ⊔ x)
_≲[_]_ {C = C} {X} xs k ys = Preorder._≲_ ([ k ]-Order C X) xs ys
------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.0
infix 4 _∼[_]_
_∼[_]_ = _≲[_]_
{-# WARNING_ON_USAGE _∼[_]_
"Warning: _∼[_]_ was deprecated in v2.0. Please use _≲[_]_ instead. "
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4