------------------------------------------------------------------------
-- 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  _<$>_ _<$_

  field
    _<$>_ : ∀ {P Q} → P ⊆ Q → F P ⊆ F Q

  _<$_ : ∀ {P Q} → (∀ {i} → P i) → F Q ⊆ F P
  x <$ y = const x <$> y