The elementhood relation on coalgebras of polynomial endofunctors

module trees.elementhood-relation-coalgebras-polynomial-endofunctors where
Imports 
open import foundation.dependent-pair-types
open import foundation.fibers-of-maps
open import foundation.universe-levels

open import graph-theory.directed-graphs
open import graph-theory.walks-directed-graphs

open import trees.coalgebras-polynomial-endofunctors

Idea

Given two elements x y : X in the underlying type of a coalgebra of a polynomial endofunctor, We say that x is an element of y, i.e., x ∈ y, if there is an element b : B (shape y) equipped with an identification component y b ＝ x. Note that this elementhood relation of an arbitrary coalgebra need not be irreflexive.

By the elementhood relation on coalgebras we obtain for each coalgebra a directed graph.

Definition

infixl 0 is-element-of-coalgebra-polynomial-endofunctor

is-element-of-coalgebra-polynomial-endofunctor :
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  (x y : type-coalgebra-polynomial-endofunctor X) → UU (l2 ⊔ l3)
is-element-of-coalgebra-polynomial-endofunctor X x y =
  fib (component-coalgebra-polynomial-endofunctor X y) x

syntax
  is-element-of-coalgebra-polynomial-endofunctor X x y = x ∈ y in-coalgebra X

The graph of a coalgebra for a polynomial endofunctor

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
  (X : coalgebra-polynomial-endofunctor l3 A B)
  where

  graph-coalgebra-polynomial-endofunctor :
    Directed-Graph l3 (l2 ⊔ l3)
  pr1 graph-coalgebra-polynomial-endofunctor =
    type-coalgebra-polynomial-endofunctor X
  pr2 graph-coalgebra-polynomial-endofunctor x y =
    x ∈ y in-coalgebra X

  walk-coalgebra-polynomial-endofunctor :
    (x y : type-coalgebra-polynomial-endofunctor X) → UU (l2 ⊔ l3)
  walk-coalgebra-polynomial-endofunctor =
    walk-Directed-Graph graph-coalgebra-polynomial-endofunctor

  concat-walk-coalgebra-polynomial-endofunctor :
    {x y z : type-coalgebra-polynomial-endofunctor X} →
    walk-coalgebra-polynomial-endofunctor x y →
    walk-coalgebra-polynomial-endofunctor y z →
    walk-coalgebra-polynomial-endofunctor x z
  concat-walk-coalgebra-polynomial-endofunctor =
    concat-walk-Directed-Graph graph-coalgebra-polynomial-endofunctor