{-# OPTIONS --type-in-type #-}

open import NeilPrelude

module SubSet where

SubSet : Set → Set
SubSet A = A → Set

Image : {A B : Set} → (f : A → B) → SubSet B
Image {A} f b = Σ[ a ∶ A ] (f a ≡ b)

SubImage : {A B : Set} → (f : A → B) → SubSet A → SubSet B
SubImage {A} f P b = Σ[ a ∶ A ] (P a × f a ≡ b)

SubSetEq : {A : Set} → SubSet A → SubSet A → Set
SubSetEq {A} P Q = (a : A) → P a ↔ Q a