The elementhood relation on W-types

module trees.elementhood-relation-w-types where

open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.identity-types
open import foundation.universe-levels

open import trees.elementhood-relation-coalgebras-polynomial-endofunctors
open import trees.w-types

Idea

We say that a tree S is an element of a tree tree-𝕎 x α if S can be equipped with an element y : B x such that α y = S.

Definition

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  where

  _∈-𝕎_ : 𝕎 A B → 𝕎 A B → UU (l1 ⊔ l2)
  x ∈-𝕎 y = x ∈ y in-coalgebra 𝕎-Coalg A B

  _∉-𝕎_ : 𝕎 A B → 𝕎 A B → UU (l1 ⊔ l2)
  x ∉-𝕎 y = is-empty (x ∈-𝕎 y)

Properties

irreflexive-∈-𝕎 :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (x : 𝕎 A B) → x ∉-𝕎 x
irreflexive-∈-𝕎 {A = A} {B = B} (tree-𝕎 x α) (pair y p) =
  irreflexive-∈-𝕎 (α y) (tr (λ z → (α y) ∈-𝕎 z) (inv p) (pair y refl))