Accessible elements with respect to relations

Content created by Daniel Gratzer, Egbert Rijke, Elisabeth Stenholm and Fredrik Bakke.

Created on 2023-11-27.
Last modified on 2024-04-11.

module order-theory.accessible-elements-relations where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.universe-levels

open import foundation-core.negation
open import foundation-core.propositions

Idea

Given a type X with a binary relation _<_ : X → X → Type we say that x : X is accessible if y is accessible for all y < x. Note that the predicate of being an accessible element is a recursive condition. The accessibility predicate is therefore implemented as an inductive type with one constructor:

  access : ((y : X) → y < x → is-accessible y) → is-accessible x

Definitions

The predicate of being an accessible element with respect to a relation

module _
  {l1 l2} {X : UU l1} (_<_ : Relation l2 X)
  where

  data is-accessible-element-Relation (x : X) : UU (l1 ⊔ l2)
    where
    access :
      ({y : X} → y < x → is-accessible-element-Relation y) →
      is-accessible-element-Relation x

Accessible elements with respect to relations

module _
  {l1 l2 : Level} {X : UU l1} (_<_ : Relation l2 X)
  where

  accessible-element-Relation : UU (l1 ⊔ l2)
  accessible-element-Relation = Σ X (is-accessible-element-Relation _<_)

Properties

Any element in relation to an accessible element is accessible

module _
  {l1 l2 : Level} {X : UU l1} (_<_ : Relation l2 X)
  where

  is-accessible-element-is-related-to-accessible-element-Relation :
    {x : X} → is-accessible-element-Relation _<_ x →
    {y : X} → y < x → is-accessible-element-Relation _<_ y
  is-accessible-element-is-related-to-accessible-element-Relation (access f) =
    f

An induction principle for accessible elements

module _
  {l1 l2 l3 : Level} {X : UU l1} (_<_ : Relation l2 X) (P : X → UU l3)
  where

  ind-accessible-element-Relation :
    ( {x : X} → is-accessible-element-Relation _<_ x →
      ({y : X} → y < x → P y) → P x) →
    {x : X} → is-accessible-element-Relation _<_ x → P x
  ind-accessible-element-Relation IH (access f) =
    IH (access f) (λ H → ind-accessible-element-Relation IH (f H))

Accessibility is a property

Proof: Consider an element x : X of a type X equipped with a binary relation _<_. We prove by double induction that any two elements of is-accessible-element-Relation _<_ x are equal. It therefore suffices to prove that access f ＝ access f' for any two elements

  f f' : {y : X} → y < x → is-accessible-element-Relation _<_ y

The induction hypotheses asserts that any two elements of type is-accessible-element-Relation _<_ y are equal for any y < x. The induction hypothesis therefore implies that any two elements in the type

  {y : X} → y < x → is-accessible-element-Relation _<_ y

are equal. Therefore it follows that f ＝ f', and we conclude that access f ＝ access f'.

module _ {l1 l2} {X : UU l1} (_<_ : Relation l2 X) where

  all-elements-equal-is-accessible-element-Relation :
    (x : X) → all-elements-equal (is-accessible-element-Relation _<_ x)
  all-elements-equal-is-accessible-element-Relation x (access f) (access f') =
    ap
      ( access)
      ( eq-htpy-implicit
        ( λ y →
          eq-htpy
            ( λ H →
              all-elements-equal-is-accessible-element-Relation y
                ( f H)
                ( f' H))))

  is-prop-is-accessible-element-Relation :
    (x : X) → is-prop (is-accessible-element-Relation _<_ x)
  is-prop-is-accessible-element-Relation x =
    is-prop-all-elements-equal
      ( all-elements-equal-is-accessible-element-Relation x)

  is-accessible-element-prop-Relation : (x : X) → Prop (l1 ⊔ l2)
  pr1 (is-accessible-element-prop-Relation x) =
    is-accessible-element-Relation _<_ x
  pr2 (is-accessible-element-prop-Relation x) =
    is-prop-is-accessible-element-Relation x

If x is an <-accessible element, then < is antisymmetric at x

module _
  {l1 l2 : Level} {X : UU l1} (_<_ : Relation l2 X)
  where

  is-asymmetric-is-accessible-element-Relation :
    {x : X} → is-accessible-element-Relation _<_ x →
    {y : X} → x < y → ¬ (y < x)
  is-asymmetric-is-accessible-element-Relation (access f) H K =
    is-asymmetric-is-accessible-element-Relation (f K) K H

If x is an <-accessible element, then < is irreflexive at x

module _
  {l1 l2 : Level} {X : UU l1} (_<_ : Relation l2 X)
  where

  is-irreflexive-is-accessible-element-Relation :
    {x : X} → is-accessible-element-Relation _<_ x → ¬ (x < x)
  is-irreflexive-is-accessible-element-Relation a H =
    is-asymmetric-is-accessible-element-Relation _<_ a H H

Recent changes