The elementhood relation on W-types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2023-01-26.
Last modified on 2023-09-11.

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.transport-along-identifications
open import foundation.universe-levels

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


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.


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

  infix 6 _∈-𝕎_ _∉-𝕎_

  _∈-𝕎_ : 𝕎 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)


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))

Recent changes