# Accessible elements with respect to relations

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

Created on 2023-11-27.

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