open import 1Lab.Underlying
open import 1Lab.Type hiding (Σ-syntax)
module 1Lab.Membership where
record Membership {ℓ ℓe} (A : Type ℓe) (ℙA : Type ℓ) ℓm : Type (ℓ ⊔ ℓe ⊔ lsuc ℓm) where
field _∈_ : A → ℙA → Type ℓm
infix 30 _∈_
open Membership ⦃ ... ⦄ using (_∈_) public
{-# DISPLAY Membership._∈_ i a b = a ∈ b #-}
instance
Membership-pow
: ∀ {ℓ ℓ'} {A : Type ℓ} {P : Type ℓ'} ⦃ u : Underlying P ⦄
→ Membership A (A → P) _
Membership-pow = record { _∈_ = λ x S → ⌞ S x ⌟ }
_∉_ : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {ℙA : Type ℓ'} ⦃ m : Membership A ℙA ℓ'' ⦄
→ A → ℙA → Type ℓ''
x ∉ y = ¬ (x ∈ y)
infix 30 _∉_
∫ₚ
: ∀ {ℓ ℓ' ℓ''} {X : Type ℓ} {ℙX : Type ℓ'} ⦃ m : Membership X ℙX ℓ'' ⦄
→ ℙX → Type _
∫ₚ {X = X} P = Σ[ x ∈ X ] x ∈ P
record Inclusion {ℓ} (ℙA : Type ℓ) ℓi : Type (ℓ ⊔ lsuc (ℓi)) where
field _⊆_ : ℙA → ℙA → Type ℓi
infix 30 _⊆_
open Inclusion ⦃ ... ⦄ using (_⊆_) public
{-# DISPLAY Inclusion._⊆_ i a b = a ⊆ b #-}
instance
Inclusion-default
: ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {ℙA : Type ℓ'} ⦃ m : Membership A ℙA ℓ'' ⦄
→ Inclusion ℙA (ℓ ⊔ ℓ'')
Inclusion-default {A = A} = record { _⊆_ = λ S T → (a : A) → a ∈ S → a ∈ T }
{-# INCOHERENT Inclusion-default #-}