------------------------------------------------------------------------
-- The Agda standard library
--
-- Functors on indexed sets (predicates)
------------------------------------------------------------------------
-- Note that currently the functor laws are not included here.
{-# OPTIONS --cubical-compatible --safe #-}
module Effect.Functor.Predicate where
open import Function.Base using (const)
open import Level using (Level; suc; _⊔_)
open import Relation.Unary using (_⊆_)
open import Relation.Unary.PredicateTransformer using (PT)
private
variable
i j ℓ₁ ℓ₂ : Level
record RawPFunctor {I : Set i} {J : Set j}
(F : PT I J ℓ₁ ℓ₂) : Set (i ⊔ j ⊔ suc ℓ₁ ⊔ suc ℓ₂)
where
infixl 4 _<$>_ _<$_
field
_<$>_ : ∀ {P Q} → P ⊆ Q → F P ⊆ F Q
_<$_ : ∀ {P Q} → (∀ {i} → P i) → F Q ⊆ F P
x <$ y = const x <$> y
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